[Caml-list] GADT: equal functions typechecks differently

[Caml-list] GADT: equal functions typechecks differently

[Ivan Gotovchits]

I've found a case when two function, that differs very slightly (almost
identical), causes different reactions of a typechecker. For me, this
looks like a bug, but may be there is something (well of course there
is) that I do not understand:

I have two types, an id and a pool of id. Both are protected with
phantom type. The definitions is very small, so I will provide them:

  module Set =
    Set.Make(struct type t = int let compare = compare end)

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

  type our
  type ads
  type ows
  type ext


I define two GADT's and two injections:

  type _ sys =
    | Our : our sys
    | Ows : ows sys
    | Ads : ads sys
    | Ext : ext sys

  type tid   = Id : 'a sys * 'a id -> tid
  type tpool = Pool : 'a sys * 'a pool -> tpool

  let to_tid sys id = Id (sys,id)
  let to_tpool sys pool = Pool (sys,pool)

Using common idiom (it is common, isn't?) I can typesafely compare my
systems.

  type (_,_) eq = Eq : ('a,'a) eq

  let try_sys_equal: type a b. (a sys * b sys) -> (a,b) eq option =
   function
   | Our,Our -> Some Eq
   | Ows,Ows -> Some Eq
   | Ads,Ads -> Some Eq
   | Ext,Ext -> Some Eq
   | _       -> None


Next, I provide two injections:

  # let of_tid: type t1. t1 sys -> tid -> t1 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 -> 't1 id option = <fun>

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

  val of_tpool : 't1 sys -> tpool -> 't1 pool option = <fun>

As you can see, they typechecks. But here is the strange behavior - if I
write the first function in a slightly different manner, it typechecks:

  # 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>

But if I add the same t2 type to the second function it fails:

  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
                          ^^^^
  Error: This expression has type ex#7 pool
       but an expression was expected of type t2 pool
       Type ex#7 = t1 is not compatible with type t2 


Thank in advance for any clues
Ivan

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

[Leo White]

>   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