Anonymous | Login | Signup for a new account 2019-02-20 03:09 CET
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007617OCamltypingpublic2017-09-01 18:572017-09-13 01:34
Reportertrefis
Assigned Togarrigue
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed
PlatformOSOS Version
Product Version
Target VersionFixed in Version4.06.0 +dev/beta1/beta2/rc1
Summary0007617: Ambiguous type escaping the scope of its equation
DescriptionThe following example typechecks properly:

# type ('a, 'b) eq = Refl : ('a, 'a) eq;;
type ('a, 'b) eq = Refl : ('a, 'a) eq
# let ok (type a b) (x : (a, b) eq) =
match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
;;
val ok : ('a, 'b) eq -> 'c list

But I claim it shouldn't as the typechecker will have chosen an arbitrary rigid
type for the ambivalent pattern [(_ : a) | (_ : b)].

This is made more apparent with the following examples:

# let oks (type a b) (x : (a, b) eq) =
match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
| Refl, [(_ : a) | (_ : b)] -> []
;;
val oks : ('a, 'b) eq -> 'c list
# let fails (type a b) (x : (a, b) eq) =
match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
| Refl, [(_ : b) | (_ : a)] -> []
;;
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type
(a, b) eq * a list
Type b is not compatible with type a

N.B. this happens both with and without -principal.
TagsNo tags attached.
Attached Files

Relationships
 parent of 0007618 resolved garrigue Unexpected GADT error

 Notes garrigue (manager) 2017-09-05 16:24 Actually, the first example is fine: since [] has type forall 'a. 'a list, the type is not escaping. But the fails example should not fail. We should use a different instance of the scrutinee for each case. garrigue (manager) 2017-09-06 09:34 Cf. https://github.com/ocaml/ocaml/pull/1318 [^] garrigue (manager) 2017-09-13 01:34 Fixed in trunk by commits 19b37dc5 and 5c174df4. Do not lower the level when unifying branches of pattern-matching together, and use local environment for unification.

 Issue History Date Modified Username Field Change 2017-09-01 18:57 trefis New Issue 2017-09-05 16:24 garrigue Note Added: 0018224 2017-09-05 16:24 garrigue Assigned To => garrigue 2017-09-05 16:24 garrigue Status new => confirmed 2017-09-05 16:27 garrigue Relationship added parent of 0007618 2017-09-06 09:34 garrigue Note Added: 0018229 2017-09-13 01:34 garrigue Note Added: 0018241 2017-09-13 01:34 garrigue Status confirmed => resolved 2017-09-13 01:34 garrigue Fixed in Version => 4.06.0 +dev/beta1/beta2/rc1 2017-09-13 01:34 garrigue Resolution open => fixed