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:

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

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.