Re: [Caml-list] Troublesome nodes

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Jeremy Yallop <jeremy.yallop@ed.ac.uk>

> Jacques Garrigue wrote:
> > From: Jeremy Yallop <jeremy.yallop@ed.ac.uk>
> >> Dario Teixeira wrote:
> >>>     type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
> >> I don't think this is quite what you want yet, although it's getting
> >> close!
> >>
> >> The first problem is that phantom types must be implemented in terms
> >> of abstract (or at least generative) types.
> > 
> > This is actually the other way round: abstract and private types allow
> > phantom types, but abbreviations and normal datatypes (generative
> > ones) don't.
> 
> Thanks for the correction!  I haven't yet properly internalized private 
> rows.  It seems that private rows allow phantom types because there is 
> abstraction (and hence generativity) involved.
> 
> However, it seems to me that normal (generative) datatypes also allow 
> phantom types.  If `t' is a unary generative datatype constructor  then 
> `int t' and `unit t' are not unifiable, even if the type parameter does 
> not occur on the rhs of the definition of `t'.  For example:
> 
>     type 'a t = T
>     let f ((_ : int t) : unit t) = ()  (* Wrong. *)

However

      let f x = (x : int t :> unit t)  (* Ok *)

For datatypes, variance is inferred automatically, and if a variable
does not occur in the type you are allowed to change it arbitrarily
through subtyping.

> On a related note, does Dario's declaration above become ambiguous with 
> the introduction of private type abbreviations?  The following program
> passes typechecking in 3.10.2, but not in 3.11+dev12, perhaps because 
> `t' is interpreted as a private type abbreviation rather than as a 
> private row type.

I detailed the change in my answer to his mail. In 3.11 the
distinction is syntactic: only explicit variant or object types give
rise to private rows.
By the way, I forgot to mention that aliases (as keyword) of those
were not allowed until now, so I have to fix it to make the syntax for
private rows work. (There are useful examples using this syntax.)

  type ('a, 'b) t = private [< super_node_t ] as 'a

Cheers,

Jacques Garrigue