Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"Warning 62: Type constraints do not apply to GADT cases of variant types." Yes they do, you little liar :-) #7803

vicuna opened this issue Jun 9, 2018 · 3 comments


None yet
2 participants
Copy link

commented Jun 9, 2018

Original bug ID: 7803
Reporter: disteph
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2018-06-11T04:12:38Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.06.1
Category: typing

Bug description

module Test : sig
type 'a t constraint 'a = *
end = struct
type 'a t =
| Int : (intint) t
| Bool: (bool
bool) t
constraint 'a = *

The code above triggers "Warning 62: Type constraints do not apply to GADT cases of variant types."
about the "constraint 'a = *" in the struct.

However, if I remove "constraint 'a = *" in the struct, I get a real error message:
"Type declarations do not match:
type 'a t = Int : (int * int) t | Bool : (bool * bool) t
is not included in
type 'a t constraint 'a = 'b * 'c

Ideally, I would like to agree with the warning, and disagree with the error, expecting the type-checker to go through each constructor's type and verify that the output type does satisfy the constraint, which is the case in my example.
But if for some reason the type-checker cannot do that when it matches the inferred type from the signature's type, then at least I would like to help him with my constraint inside the struct and not get the warning.


This comment has been minimized.

Copy link

commented Jun 11, 2018

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

This comment has been minimized.

Copy link

commented Jun 13, 2018

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)?


This comment has been minimized.

Copy link

commented Jun 20, 2018

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" correclty, 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 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

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

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.