Comment author: @garrigue

Indeed, the warning is here to avoid confusion over the scope of type variable in constraints.
But this doesn't mean that having a constraint on a GADT is strictly useless.
Maybe the warning could be disabled when

• some variables in the constraint are formal parameters of the type
• no variable of the constraints appear in GADT cases

Comment author: disteph

Thanks for the answer.
Yes, that would already be good! (otherwise I don't know how to avoid getting a warning).
Now I'm just curious: the constraint I've added in the struct triggers the verification that each of the GADT cases satisfies it. Why isn't this constructor-by-constructor analysis performed when the inferred signature is matched against the declared one (when I don't put the constraint in the struct)?

Comment author: @gasche

I had a discussion with Stéphane (disteph) about this issue today,
which I will summarize below.

Variables in the constraint that are not type parameters are
existentially quantified at the type declaration point
(existential constraint variables), while variables in GADT
constructor types that are not type parameters are existentially
quantified within each constructor
(existential constructor variables).

The intent of the warning is to warn users that, if an existential
constraint variable and an existential constructor variables are
given the same name, they will still be bound in different places
and independent. For example:

type 'a t = A : 'b -> (int * int) t
  constraint 'a = 'b * _

One may think that the parameter of A is constrained to be int,
it would if the two 'b were the same variable, but in fact it isn't.

This situation cannot occur in the original reported example,
where the constraint is only used to expose a type product constructor
to the outside (constraint 'a = _*_). If I understand Jacques'
second "disabling condition" correctly, it exactly means that
there never are existential constraint variable and constructor
variables of the same name.

(I asked Stéphane whether he would be interested in trying to write
a PR to relax the warning in this way, and he might give it
a try. I don't know how easy/hard that is.)

On the other hand, I would personally find it more natural if the
compiler did "the right thing" in this situation, rather than emitting
a warning to say that it may not be doing what the user want. In my
example above, it is quite clear to me that the two 'b should be the
same variable, scoped at the type-declaration point. Why don't we
implement this? (If we would like to implement this eventually, but
don't have time to do it now, maybe we should emit an error in the
case of name conflict instead of a warning, as the semantics is going to
change from the one currently accepted.)

Finally, here is an answer to Stéphane's question of why we cannot
write the constraint only in the signature, and have a check that it
is valid when compared to an unconstrained implementation:

1. For non-GADT type declarations, this is probably unsound
   (experts would know). In general if you could write:

     module M : sig
        type 'a t = 'a constraint 'a = _ * _
        ...
     end = struct
        type 'a t = 'a
        ...
     end

then it would be possible for other declarations in the module
(the ... in struct), which see an un-constrained definition, to use
'a t that do not satisfy the contraints. They may then export
code using these through the signature, and we both thought that it
might be possible to cause trouble in this way.

2. Even for GADT type declarations this may be unsound: even if the
   constraint is checked against the instances imposed by the
   constructors, it is still possible for the code to manipulate
   values at types that do not match any of the constructor type
   instantiations. A typical example is

     type (_, _) eq = Refl : ('c, 'c) eq

which still allows to abstract over values of type (int, bool) eq,
and do various things with them.

Remark: we had fun playing with the following declaration of eq:

  type ('a, 'b) eq = Refl : ('c, 'c) eq
    constraint 'a = 'b

This is valid OCaml code, and it does what you expect: it's a version
of eq that does not allow to express instances for which the two parameters
are not syntactically equal.
Yet, this type is completely useless as far as I can tell (the whole point
of eq being to expose equalities in contexts where they are not statically
evident, for example if one side is an abstract type).

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Since we all agree that currently the wording of the warning is wrong, I see 2 solutions:

• fix the wording only; something like
  Type constraints do not apply to type variables in GADT cases of variant types
• really try to detect whether there is an overlap in variable names between GADT cases and constraints
  Of course, the first one is easier.
  Note that if you know that the warning is spurious you can always disable it locally with an attribute.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.