Rank-2 polymorphism woes in module signatures

Rank-2 polymorphism woes in module signatures

[Jacques Carette]

[Simplified problem]:
module type Symantics = sig
  type ('c,'sv,'dv) repr
  type ('c, 'sv, 'dv) pack = {
   _lam : 'sa 'sb 'da 'db . (('c,'sa,'da) repr -> ('c,'sb,'db) repr)
    -> ('c,(('c,'sa,'da) repr -> ('c,'sb,'db) repr),'da->'db) repr;
   }
end

(* concrete *)
module R = struct
  type ('c,'sv,'dv) repr = 'dv
  type ('c, 'sv, 'dv) pack = {
   _lam : 'sa 'sb 'da 'db . (('c,'sa,'da) repr -> ('c,'sb,'db) repr)
    -> ('c,(('c,'sa,'da) repr -> ('c,'sb,'db) repr),'da->'db) repr;
   }
end;;

module XX(S:Symantics) = struct end;;
module XXR = XX(R);;

and I get
Signature mismatch:
Modules do not match:
[...]
is not included in
  Symantics
Type declarations do not match:
  type ('a, 'b, 'c) pack =
    ('a, 'b, 'c) R.pack = {
    _lam :
      'd 'e 'f 'g.
        (('a, 'd, 'f) repr -> ('a, 'e, 'g) repr) ->
        ('a, ('a, 'd, 'f) repr -> ('a, 'e, 'g) repr, 'f -> 'g) repr;
  }
is not included in
  type ('a, 'b, 'c) pack = {
    _lam :
      'd 'e 'f 'g.
        (('a, 'd, 'f) repr -> ('a, 'e, 'g) repr) ->
        ('a, ('a, 'd, 'f) repr -> ('a, 'e, 'g) repr, 'f -> 'g) repr;
  }

Those look absolutely identical to me - especially since the definitions 
were done via copy & paste.
The rank-1 parts of the same record work fine [not shown], but none of 
the rank-2 parts do.  The above is a minimal extraction from a real program.
Can anyone help?  [This is in 3.09.01]

Jacques

Re: [Caml-list] Rank-2 polymorphism woes in module signatures

[Jacques Garrigue]

From: Jacques Carette <carette@mcmaster.ca>

> Those look absolutely identical to me - especially since the definitions 
> were done via copy & paste.
> The rank-1 parts of the same record work fine [not shown], but none of 
> the rank-2 parts do.  The above is a minimal extraction from a real program.
> Can anyone help?  [This is in 3.09.01]

Thanks for finding a (very stupid) bug, triggered by your use of a
phantom type. This is now fixed in CVS for 3.10.
Here is a patch that should work on any version of ocaml.

Jacques Garrigue

Index: typing/ctype.ml
===================================================================
RCS file: /net/yquem/devel/caml/repository/csl/typing/ctype.ml,v
retrieving revision 1.204
retrieving revision 1.205
diff -u -r1.204 -r1.205
--- typing/ctype.ml	16 Feb 2007 11:18:36 -0000	1.204
+++ typing/ctype.ml	19 Feb 2007 00:49:16 -0000	1.205
@@ -2264,7 +2264,7 @@
               enter_poly env univar_pairs t1 tl1 t2 tl2
                 (eqtype rename type_pairs subst env)
           | (Tunivar, Tunivar) ->
-              unify_univar t1 t2 !univar_pairs
+              unify_univar t1' t2' !univar_pairs
           | (_, _) ->
               raise (Unify [])
         end