|Anonymous | Login | Signup for a new account||2018-08-16 20:12 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007803||OCaml||typing||public||2018-06-09 12:38||2018-06-20 18:37|
|Target Version||Fixed in Version|
|Summary||0007803: "Warning 62: Type constraints do not apply to GADT cases of variant types." Yes they do, you little liar :-)|
|Description||module Test : sig|
type 'a t constraint 'a = _*_
end = struct
type 'a t =
| Int : (int*int) 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.
|Tags||No tags attached.|
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
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)?
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).
|2018-06-09 12:38||disteph||New Issue|
|2018-06-11 06:12||garrigue||Note Added: 0019179|
|2018-06-11 06:12||garrigue||Assigned To||=> garrigue|
|2018-06-11 06:12||garrigue||Status||new => confirmed|
|2018-06-13 15:01||disteph||Note Added: 0019187|
|2018-06-20 18:37||gasche||Note Added: 0019200|
|Copyright © 2000 - 2011 MantisBT Group|