[Caml-list] An inconsistency (possibly) in typing constraints with GADT

[Ivan Gotovchits <ivg@ieee.org>]

[-- Attachment #1: Type: text/plain, Size: 1121 bytes --]

Hi Everyone,

I'm wondering, is the following type definition rejected because there is
some fundamental reason, that I'm missing, or this is just a missed case in
the type checker?

    type ('a,'b) domain = Domain
    type 'd exp = Ret : 'a -> 'd exp constraint 'd = ('a,'b) domain

Fails with:

     Error: Constraints are not satisfied in this type.
       Type 'd exp should be an instance of ('a, 'b) domain exp

If we will express the same without GADT, it will be accepted, e.g.,

    type 'd exp = Ret of 'a constraint 'd = ('a,'b) domain


And, of course, we can make typechecker happy with

   type 'd exp = Ret : 'a -> ('a,'b) domain exp constraint 'd = ('a,'b)
domain

However, it will, somewhat, defeat the whole purpose of introducing the
constraint, as I'm using constraints as a sort of type abstraction to bind
type variables, and to my understanding the [constraint 'x =
<type-expression>] makes any occurrence of `'x` to be equivalent to the
<type-expression> in its scope.

Thanks,
Ivan

P.S. Of course, the provided example is a simplification of a real code,
where the constraint is really needed.

[-- Attachment #2: Type: text/html, Size: 4087 bytes --]