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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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.