Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007261OCamltypingpublic2016-05-19 17:262017-03-14 05:04
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.03.0 
Target Version4.06.0 +dev/beta1/beta2/rc1Fixed in Version4.06.0 +dev/beta1/beta2/rc1 
Summary0007261: constraint ignored on (existential) GADT
DescriptionBug 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 ReproduceCompile the attached file

$ ocamlc -c
File "", 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, uncomment definition 2 instead of definition 1 :
that is
 Foo: ( [> `Bla ] as 'b ) * 'b -> foo

$ ocamlc -c

=> Definition 2 is ok.

TagsNo tags attached.
Attached Files? file icon [^] (552 bytes) 2016-05-19 17:26 [Show Content]

- Relationships

-  Notes
nojebar (developer)
2016-05-19 17:47

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.
lpw25 (developer)
2016-05-19 17:48

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.
lebotlan (reporter)
2016-05-19 22:35
edited on: 2016-05-19 22:36

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.

xleroy (administrator)
2017-02-22 15:25

Rediscussed at the dev meeting. Consenss is to try to add a warning for this misleading notation.
garrigue (manager)
2017-03-14 05:04

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.

- Issue History
Date Modified Username Field Change
2016-05-19 17:26 lebotlan New Issue
2016-05-19 17:26 lebotlan File Added:
2016-05-19 17:47 nojebar Note Added: 0015943
2016-05-19 17:48 lpw25 Note Added: 0015944
2016-05-19 22:35 lebotlan Note Added: 0015946
2016-05-19 22:36 lebotlan Note Edited: 0015946 View Revisions
2016-09-07 17:04 shinwell Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-02-22 15:25 xleroy Note Added: 0017394
2017-02-22 15:25 xleroy Assigned To => garrigue
2017-02-22 15:25 xleroy Status new => assigned
2017-02-22 15:25 xleroy Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => 4.06.0 +dev/beta1/beta2/rc1
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-14 05:04 garrigue Note Added: 0017634
2017-03-14 05:04 garrigue Status assigned => resolved
2017-03-14 05:04 garrigue Fixed in Version => 4.06.0 +dev/beta1/beta2/rc1
2017-03-14 05:04 garrigue Resolution open => fixed

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker