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

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

[Ivan Gotovchits]

[-- 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 --]

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

[Jacques Garrigue]

Sorry for the slow answer,


On 2017/07/14 10:00, Ivan Gotovchits wrote:
> 
> 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

The problem is the scope of ‘d in the definition of exp above.
It is actually equivalent to
   type ‘d exp = Ret : ‘a -> ‘e exp constraint ‘d = (‘a,’ b) domain

I.e. type variables in GADT clauses use a completely different scope, which ignores constraint clauses.
This makes combining GADTs and constraint very awkward.
On the other hand, a different semantics would be cumbersome too.

Jacques Garrigue

> 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.