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

constraint ignored on (existential) GADT #7261

Closed
vicuna opened this issue May 19, 2016 · 5 comments
Closed

constraint ignored on (existential) GADT #7261

vicuna opened this issue May 19, 2016 · 5 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented May 19, 2016

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

@vicuna
Copy link
Author

vicuna commented May 19, 2016

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.

@vicuna
Copy link
Author

vicuna commented May 19, 2016

Comment author: @lpw25

Constraints are on the whole type not a particular constructor. So the 'b in the constraint is unrelated to the existential 'b in the constructor's type.

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.

@vicuna
Copy link
Author

vicuna commented May 19, 2016

Comment author: lebotlan

type foo =
Foo: 'b * 'b -> foo constraint 'b = [> `Bla ]

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

@vicuna
Copy link
Author

vicuna commented Feb 22, 2017

Comment author: @xavierleroy

Rediscussed at the dev meeting. Consenss is to try to add a warning for this misleading notation.

@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

Commit 47eb55f adds the requested warning, i.e. as soon as a type constraint is added to a type containing GADT cases.
Note that in theory it can warn on valid code too, but I'm yet to see such code in the wide.

@vicuna vicuna closed this as completed Mar 14, 2017
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.06.0 milestone 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
Projects
None yet
Development

No branches or pull requests

2 participants