|Anonymous | Login | Signup for a new account||2018-06-19 14:54 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-13 15:01|
|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)?
|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|
|Copyright © 2000 - 2011 MantisBT Group|