Thanks for the explanation Jacques!

To be honest I was expecting the difficulty to lie in comparing two constrained definitions (in my example, that would mean that type 'a format would already be constrained and I'd be trying to narrow it further with another constrained type). I thought the particular case where the original type is unconstrained would be easier, but yeah, this is certainly more difficult than it looks!

ph.


2013/7/27 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