Re: [Caml-list] GADT: equal functions typechecks differently

[Leo White <lpw25@cam.ac.uk>]

>   type 'a pool = {
>     set : Set.t;
>     min : int;
>     max : int;
>   }
>   type 'a id = int
>

The difference between id and pool is that 'a id is equal to 'b id for
any types 'a and 'b, since they are both equal to int, while 'a pool
only equals 'b pool if 'a equals 'b. For example:

  # let f (x: int id) : float id = x;;
  val f : int id -> float id = <fun>

  # let f (x: int pool) : float pool = x;;
  Characters 35-36:
    let f (x: int pool) : float pool = x;;
                                       ^
  Error: This expression has type int pool
         but an expression was expected of type float pool
         Type int is not compatible with type float 

Interestingly, 'a pool is a subtype of 'b pool for any 'a and 'b, so the
following definition is allowed:

  # let f (x: int pool) : float pool = (x :> float pool);;
  val f : int pool -> float pool = <fun>

This is why:

>   # let of_tid: type t1 t2. t1 sys -> tid -> t2 id option =
>     fun sys1 (Id (sys2,id)) ->
>       match try_sys_equal (sys1,sys2) with
>       | Some Eq -> Some id
>       | None -> None;;
>   val of_tid : 't1 sys -> tid -> 't2 id option = <fun>

is accepted, but 

>   let of_tpool: type t1 t2. t1 sys -> tpool -> t2 pool option =
>     fun sys1 (Pool (sys2,pool)) ->
>       match try_sys_equal (sys1,sys2) with
>       | Some Eq -> Some pool
>       | None -> None;;
>           Characters 158-162:
>         | Some Eq -> Some pool

is disallowed. We could, however, write this function using subtyping:

  # let of_tpool: type t1 t2. t1 sys -> tpool -> t2 pool option =
    fun sys1 (Pool (sys2,pool)) ->
      match try_sys_equal (sys1,sys2) with
      | Some Eq -> Some (pool :> t2 pool)
      | None -> None;;
  val of_tpool : 't1 sys -> tpool -> 't2 pool option = <fun>

Note that these functions are not really using any of the GADT
constraints. They don't need to since any 'a id can be used as a t2 id
and any 'a pool can be subtyped into a t2 pool.

Regards,

Leo