Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] 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 0007618resolvedgarrigue Unexpected GADT error 

-  Notes
(0018224)
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.
(0018229)
garrigue (manager)
2017-09-06 09:34

Cf. https://github.com/ocaml/ocaml/pull/1318 [^]
(0018241)
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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker