[Caml-list] GADT: equal functions typechecks differently

[Ivan Gotovchits <ivg@ieee.org>]

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