Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.Sign up
GitHub is where the world builds software
Millions of developers and companies build, ship, and maintain their software on GitHub — the largest and most advanced development platform in the world.
constraint ignored on (existential) GADT #7261
Original bug ID: 7261
When defining a GADT,
is not equivalent to
I had expected both definitions to be equivalent.
Steps to reproduce
Compile the attached file foo.ml:
$ ocamlc -c foo.ml
=> Definition 1 is broken.
Then, in foo.ml, uncomment definition 2 instead of definition 1 :
$ ocamlc -c foo.ml
=> Definition 2 is ok.
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;;
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.