From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by yquem.inria.fr (Postfix) with ESMTP id 31A8FBB84
	for <caml-list@yquem.inria.fr>; Sat, 19 Jul 2008 04:23:34 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApoEAGvsgEiCNhAB/2dsb2JhbACvXA
X-IronPort-AV: E=Sophos;i="4.31,214,1215381600"; 
   d="scan'208";a="15261512"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Jul 2008 04:23:32 +0200
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m6J2NSbd005740;
	Sat, 19 Jul 2008 11:23:29 +0900 (JST)
Date: Sat, 19 Jul 2008 11:23:14 +0900 (JST)
Message-Id: <20080719.112314.52190643.garrigue@math.nagoya-u.ac.jp>
To: darioteixeira@yahoo.com
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Troublesome nodes
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <816005.53409.qm@web54606.mail.re2.yahoo.com>
References: <299457.46023.qm@web54602.mail.re2.yahoo.com>
	<816005.53409.qm@web54606.mail.re2.yahoo.com>
X-Mailer: Mew version 4.2 on Emacs 22.2 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; nodes:01 node:01 sig:01 node:01 struct:01 sig:01 struct:01 datatype:01 recursion:01 datatype:01 summarize:01 invariants:01 rec:01 rec:01 caml-list:01 

From: Dario Teixeira <darioteixeira@yahoo.com>

> I would like to add one extra, odd, tidbit.  On a simple example, 'private'
> will only work if a dummy constructor is added to the type.  Thus, this will
> not work:
> 
> module rec Node:
> sig
>         (* ... *)
>         type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t]
>         (* ... *)
> end =
> struct
>         (* ... *)
>         type (+'a, 'b) t = 'a constraint 'a = [< super_node_t]
>         (* ... *)
> end

I don't understand your counter-example. In typechecks without any
problem, even in older versions. May you did cut it down too much?

> But this will:
> 
> module rec Node:
> sig
>         (* ... *)
>         type (+'a, 'b) t = private Dummy of 'a constraint 'a = [< super_node_t]
>         (* ... *)
> end =
> struct
>         (* ... *)
>         type (+'a, 'b) t = Dummy of 'a constraint 'a = [< super_node_t]
>         (* ... *)
> end =

You Dummy creates a datatype, so this is a completely different story.
Recursion is freely allowed in datatype definitions, while there are
restrictions for abbreviations.

> Is this behaviour correct?  (I'm running 3.11+dev12)

I cannot tell you, since I couldn't reproduce your problem.

By the way, I somehow get the feeling that your solution is
over-engineered. You shouldn't need all that many constraints.
I you could find a way to use private rows rather than private
abbreviations, your code might be much simpler.
But I'm sorry I couldn't follow the whole discussion on your problem.
I you could summarize it shortly, with the basic code (without phantom
types) and the invariants you are trying to enforce, I might try to
look into it.

Jacques Garrigue