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