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
constraint ignored on (existential) GADT #7261
Comments
Comment author: @nojb Are you sure this is a bug ? The constraint is applied to the whole type definition, and it would seem that the existential type type foo = Foo: 'b * 'b -> foo does not have any type parameters so the constraint does not (rightly) have any effect. |
Comment author: @lpw25 Constraints are on the whole type not a particular constructor. So the Unfortunately, constraints are just equations between arbitrary types. There is nothing to check that they actually add any useful information. For example: type t constraint 'a = 'b;;type t It would be good to have a warning when neither side of the equation relates to anything useful, but it may be quite awkward to implement. |
Comment author: lebotlan type foo = 'b is implicitly quantified and its scope is implicit, as well as the scope of the type constraint. As a consequence, it is not immediately obvious that 'b is not bound in the constraint scope. I understand that there is no quick fix. This is unfortunate, because this pattern implies a GADT, which are already hard to understand. (The original example had two type parameters, and was used in a many-polymorphic function). At first, I thought that the ocaml type system was unable to typecheck what I was doing (I was not able to check the typing by hand). Fortunately, I was wrong. |
Comment author: @xavierleroy Rediscussed at the dev meeting. Consenss is to try to add a warning for this misleading notation. |
Original bug ID: 7261
Reporter: lebotlan
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-14T04:04:54Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0
Target version: 4.06.0 +dev/beta1/beta2/rc1
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Monitored by: @gasche
Bug description
Bug summary:
When defining a GADT,
type foo =
Foo: [> `Bla ] as 'b ) * 'b -> foo
is not equivalent to
type foo =
Foo: 'b * 'b -> foo constraint 'b = [> `Bla ]
I had expected both definitions to be equivalent.
Steps to reproduce
Compile the attached file foo.ml:
$ ocamlc -c foo.ml
File "foo.ml", line 22, characters 6-10:
Error: This expression has type [> `Bla ]
but an expression was expected of type $Foo_'b
=> Definition 1 is broken.
Then, in foo.ml, uncomment definition 2 instead of definition 1 :
that is
Foo: ( [> `Bla ] as 'b ) * 'b -> foo
$ ocamlc -c foo.ml
=> Definition 2 is ok.
File attachments
The text was updated successfully, but these errors were encountered: