Normaliser doesn't detect reducible patterns across arguments

[ohad]

Sorry about the title, I'm not sure how to best title this bug

Steps to Reproduce

Foo.idr:

foo1 : List a -> List a -> List a
foo1 []      right   = []
foo1 left    []      = []
foo1 (x::xs) (y::ys) = []

empty1 : (left, right : List a) -> foo1 left right = []
empty1 []      right   = Refl
empty1 left    []      = ?hole1
empty1 (x::xs) (y::ys) = Refl

foo2 : List a -> List a -> List a
foo2 left    []      = []
foo2 []      right   = []
foo2 (x::xs) (y::ys) = []

empty2 : (left, right : List a) -> foo2 left right = []
empty2 []      right   = ?hole2
empty2 left    []      = Refl
empty2 (x::xs) (y::ys) = Refl

The difference between foo1 and foo2 is the order of the top two clauses.

Expected Behavior

$ idris2 Foo.idr
Foo> :t hole1
 0 a : Type
   left : List a
-------------------------------------
hole1 : [] = []
Foo> :t hole2
 0 a : Type
   right : List a
-------------------------------------
hole2 : [] = []

Observed Behavior

Foo> :t hole1
 0 a : Type
   left : List a
-------------------------------------
hole1 : (foo1 left []) = []
Foo> :t hole2
 0 a : Type
   right : List a
-------------------------------------
hole2 : (foo2 [] right) = []

Idris1 exhibits the same behaviour.

[edwinb]

The first two patterns are overlapping - foo [] [] matches both. If there's overlapping patterns, the clauses aren't definitional equalities, but instead the computational behaviour depends on the case trees that come out. It's certainly the case that foo1 left [] = [] for all left, but in general the normaliser isn't going to be able to spot this. So I probably can't do anything about this, I'm afraid.