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.