You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 7617 Reporter:@trefis Assigned to:@garrigue Status: resolved (set by @garrigue on 2017-09-12T23:34:27Z) Resolution: fixed Priority: normal Severity: minor Fixed in version: 4.06.0 +dev/beta1/beta2/rc1 Category: typing Parent of:#7618 Monitored by:@gasche@yallop
Bug description
The 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.
The text was updated successfully, but these errors were encountered:
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.
Fixed in trunk by commits 19b37dc and 5c174df.
Do not lower the level when unifying branches of pattern-matching together, and use local environment for unification.
Original bug ID: 7617
Reporter: @trefis
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-09-12T23:34:27Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Parent of: #7618
Monitored by: @gasche @yallop
Bug description
The following example typechecks properly:
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:
N.B. this happens both with and without -principal.
The text was updated successfully, but these errors were encountered: