Re: [Caml-list] Narrowing a signature with a constrained type

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

On 2013/07/26, at 22:32, Philippe Veber <philippe.veber@gmail.com> wrote:

> Dear camlers,
> 
> Out of curiosity, I'd be happy to understand why the following definition is rejected:
> 
> # module type T = sig type 'a format end;;
> module type T = sig type 'a format end
> # module F(X : T with type 'a format = 'a list constraint 'a = < .. >) = struct end;;
> File "", line 1, characters 13-67:                                                                                           Error: In this `with' constraint, the new definition of format does not match its original definition in the constrained signature:                                  
> Type declarations do not match: type 'a format = 'a0 list is not included in type 'a format                                                            
>        Their constraints differ.
> 
> Would it be unsound to allow it?

Well, to ensure the coherence of the with constraints, we require that
the new signature be a subtype of the original one (as a module, not as an object).
This is where your code gets rejected.

Now why is it deemed unsafe to allow a constrained type definition to be a subtype of 
an unconstrained one?
Actually, I don't know.
The unconstrained type does not enforce the invariants of the constrained one,
but they will be checked as soon as you try to unify the two.
So it may be possible to lift this restriction.

However, there are technical difficulties in comparing a constrained definition
with an unconstrained one, so this might just be the main reason.
This would also have an impact on the invariants of types through abstraction.

Jacques