Re: [Caml-list] Constrain module type to reuse a sum type

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2011/06/05, at 0:42, Dawid Toton wrote:

> I have a functor F which itself applies its own arguments to some other functors. Results R of these applications contain sum types. These R are exposed in the outcome of F in two ways: as types carried by the functions defined by F and all R packed into a wrapper module. I'd like to tell the compiler that each sum type is equal in both contexts.
> 
> The problem boils down to the following:
> 
> B.ml:
> 
> module type A = sig type a = A end
> module A = struct type a = A end
> 
> module E = A
> 
> type want_equal = A.a as 'a constraint 'a = E.a
> 
> B.mli:
> 
> module type A = sig type a = A end
> module A : A
> 
> module type E = A (*with type a = A.a*)
> module E : E
> 
> type want_equal = A.a as 'a constraint 'a = E.a
> 
> 
> There are no problems with the module implementation. I can see right types in the output of ocamlc -i .
> But the interface is wrong, since it is forgotten that the sum types in E and A are the same.
> 
> I have put a constraint in a comment - this is what I'm trying to achieve.

Your constraint (in comment) is the right one.
Unfortunately,  it was not allowed up to 3.12.0 (a full definition, including constructors, was required).
The upcoming 3.12.1 will allow it.

Jacques Garrigue