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

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

[Dawid Toton]

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.

In my real case, the module type A is a big signature that comes from 
somewhere else. The mentioned functor F should require as little changes 
as possible for each change of the module type that corresponds to the 
module type A in the above example.

This is why I'm looking for a way to constrain A to obtain E. How to do 
this?
I would be grateful for any comments.
If the code is simplified too much, I can post something more similar to 
my real code.

Dawid

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

[Jacques Garrigue]

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