Ambiguous type escaping the scope of its equation

[vicuna]

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.

[vicuna]

Comment author: @garrigue

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.

[vicuna]

Comment author: @garrigue

Cf. #1318

[vicuna]

Comment author: @garrigue

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.