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. *)

> So the above code really defines a phantom type.

Yes.

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.

type super_node_t = [`S]

module M :
sig
   type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
end =
struct
   type super_node_t = [`S]
   type ('a, 'b) t = 'a constraint 'a = [< super_node_t ]
end

let f x = (x : [<super_node_t] :> ([< super_node_t], _) M.t)

Jeremy.