Version française
Home     About     Download     Resources     Contact us    
Browse thread
Rank-2 polymorphism woes in module signatures
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jacques Carette <carette@m...>
Subject: Rank-2 polymorphism woes in module signatures
[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