Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007803OCamltypingpublic2018-06-09 12:382018-06-13 15:01
Reporterdisteph 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product Version4.06.1 
Target VersionFixed in Version 
Summary0007803: "Warning 62: Type constraints do not apply to GADT cases of variant types." Yes they do, you little liar :-)
Descriptionmodule Test : sig
  type 'a t constraint 'a = _*_
end = struct
  type 'a t =
    | Int : (int*int) t
    | Bool: (bool*bool) t
    constraint 'a = _*_
end

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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019179)
garrigue (manager)
2018-06-11 06:12

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
(0019187)
disteph (reporter)
2018-06-13 15:01

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

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker