Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007181OCamltypingpublic2016-03-14 22:312017-09-24 17:32
Reporterchambart 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0+dev / +beta1 
Target Version4.03.1+devFixed in Version4.03.0+dev / +beta1 
Summary0007181: Misleading error message with GADTs and polymorphic variants
DescriptionThe example is

type 'a tree =
  | Root : [>`Root] tree
  | Leaf : [`Root | `Leaf] tree -> [>`Leaf] tree

let rec root (type x) (tree : x tree) : [`Root] tree =
  match tree with
  | Root -> tree
  | Leaf parent -> root parent

which fails with

  | Root -> tree
            ^^^^
Error: This expression has type x tree but an expression was expected of type [ `Root ] tree
       Type x = [> `Root ] is not compatible with type [ `Root ]
       The first variant type does not allow tag(s)

Additional InformationBy the way, I'm not completely certain that this type should not be accepted
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0015498)
gasche (administrator)
2016-03-15 01:29
edited on: 2016-03-15 04:54

There is something fishy in trying to take an (exists 'r. [ `Root | 'r ]) and turn it into a [ `Root ]. In this case, you have no parameter to the Root constructor, so it seems harmless, but you could equally write the following which type-checks:

let rec root (type x) (tree : x tree) : [`Root] tree =
  match tree with
  | Root -> Root
  | Leaf parent -> root parent

if you added a parameter in the Root case, if this parameter does not depend on 'a then you can reuse the trick above, and if it does then your version seems unsound:

type 'a tree =
  | Root : ([> `Root] as 'a) -> 'a tree
  | Leaf : [`Root | `Leaf] tree -> [>`Leaf] tree

let rec root (type x) (tree : x tree) : [`Root] tree =
  match tree with
  | Root _ -> tree
  | Leaf parent -> root parent

if I could type-check that I could use it to coerce (Root `Leaf) into a ([`Root] tree).

(0015500)
garrigue (manager)
2016-03-15 04:42

Indeed, the error message is confusing.
I suppose you should get something like
       Type x = [> `Root ] is not compatible with type [ `Root ]
       The second variant type does not allow tag(s) `AnyOtherTag

Here type x has an existential row, which means that it could contain
anything, so you cannot coerce it to just [`Root].
(0015508)
chambart (developer)
2016-03-15 21:10

By the way this also cannot be coerced to [>`Root] for a different reason. The row variable will escape:

    | Root -> tree
              ^^^^
Error: This expression has type x tree but an expression was expected of type
         ([> `Root ] as 'a) tree
       Type x = [> `Root ] is not compatible with type [> `Root ] as 'a
       The type constructor $0 would escape its scope
(0015643)
garrigue (manager)
2016-03-30 03:49

Fixed in 4.03 by commit 56b337.
Just removed the incorrect last line in that case.

- Issue History
Date Modified Username Field Change
2016-03-14 22:31 chambart New Issue
2016-03-15 01:29 gasche Note Added: 0015498
2016-03-15 04:42 garrigue Note Added: 0015500
2016-03-15 04:42 garrigue Assigned To => garrigue
2016-03-15 04:42 garrigue Status new => confirmed
2016-03-15 04:54 gasche Note Edited: 0015498 View Revisions
2016-03-15 21:10 chambart Note Added: 0015508
2016-03-24 19:26 doligez Target Version => 4.03.1+dev
2016-03-30 03:49 garrigue Note Added: 0015643
2016-03-30 03:49 garrigue Status confirmed => resolved
2016-03-30 03:49 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-03-30 03:49 garrigue Resolution open => fixed
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker