Re: [Caml-list] Troublesome nodes

[Jeremy Yallop <jeremy.yallop@ed.ac.uk>]

Jacques Garrigue wrote:
> From: Jeremy Yallop <jeremy.yallop@ed.ac.uk>
>> 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.

Thanks for the explanation.  I agree that this means that datatypes are 
not useful for phantom types.

I don't yet understand exactly how private abbreviations are supposed to 
work.  The currently implemented behaviour doesn't accomplish what I 
understand to be the intention.  For example, given

    module Nat :
    sig
      type t = private int
      val z : t
      val s : t -> t
    end =
    struct
      type t = int
      let z = 0
      let s = (+) 1
    end

we can write

    # (((Nat.z : Nat.t :> int) - 1) :> Nat.t);;
    - : Nat.t = -1

Similarly, I'm surprised by the behaviour of coercions at parameterised 
types.  Given a private type

      type 'a t = private 'a

should we be able to coerce a value of type 'a t to type 'a?

Jeremy.