Unexpected GADT error

[vicuna]

Original bug ID: 7618
Reporter: @trefis
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-09-12T23:34:09Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Child of: #7617
Monitored by: @gasche

Bug description

Currently the following code is rejected by the typechecker:

# type _ t = I : int t
type _ t = I : int t
# let f (type a) (x : a t) (y : int) =
    match x, y with
    | I, (_:a) -> ()
  ;;
Error: This pattern matches values of type a t * a
       but a pattern was expected which matches values of type a t * int
       Type a is not compatible with type int

While this one is accepted:

# let g (type a) (x : a t) (y : a) =
    match x, y with
    | I, (0:int) -> ()
  ;;
val g : 'a t -> 'a -> unit

I believe that both of these function suffer from the issue raised in #7617,
i.e. the typechecker allows ambiguous types to escape, arbitrarily choosing one
of the instances as the type of the pattern (or rather, always choosing the
locally abstract type).

[f] later fails to typecheck because we try to unify the type of the pattern
with the type of the argument outside the scope of the equation introduced by
[I].
This happens on line 3887 of typecore.ml, with the call to
[unify_pats (instance env ty_arg)].

Once #7617 is fixed, everything else being unchanged, these functions should
both be rejected.
However Leo suggests they could be accepted that the typechecker if we decreased
the sharing between the type of the scrutiny and the expected type of each
pattern (eg. by using generalize_structure).

[vicuna]

Comment author: @garrigue

Leo is right. The fix should be the same as 7617.

[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.