Matching on an expression (when it's appropriate) fails when the expression is complex

[buzden]

Context

One can match an argument to a whole expression, if it matches with one:

ff : (n, k : Nat) -> k = n + 1 -> Nat
ff n (n + 1) Refl = 4

The order does not matter:

ff' : (k, n : Nat) -> k = n + 1 -> Nat
ff' (n + 1) n Refl = 4

This all works with a dot pattern too:

ff : (n, k : Nat) -> k = n + 1 -> Nat
ff n .(n + 1) Refl = 4

ff' : (k, n : Nat) -> k = n + 1 -> Nat
ff' .(n + 1) n Refl = 4

It also works if matching happens inside a with clause:

ff_ : (n, k : Nat) -> k = n + 1 -> Nat
ff_ n k r with (())
  ff_ n (n + 1) Refl | () = 4

ff'_ : (k, n : Nat) -> k = n + 1 -> Nat
ff'_ k n r with (())
  ff'_ (n + 1) n Refl | () = 4

Steps to Reproduce

Consider two following declarations matching one of their arguments on a non-trivial expression:

ffg : (f : Nat -> Nat) -> (k, n : Nat) -> (if k > 5 then n = f 5 else n = 5) -> Nat
ffg f k n prf with (k > 5)
  ffg f k (f 5) Refl | True = ?foo_t
  ffg f k n prf | False = ?foo_f

fff : (f : Nat -> Nat) -> (k, n : Nat) -> (if k > 5 then n = (if f k < 8 then 1 else 0) else n = 5) -> Nat
fff f k n prf with (k > 5)
  fff f k (if f k < 8 then 1 else 0) Refl | True = ?foo_t
  fff f k n prf | False = ?foo_f

Expected Behavior

Typechecks, as simpler expressions above.

Observed Behavior

Error: While processing left hand side of with block in ffg. Unknown type for pattern variable {P:f:2849}

DepInWith:21:12--21:13
 17 | --
 18 | 
 19 | ffg : (f : Nat -> Nat) -> (k, n : Nat) -> (if k > 5 then n = f 5 else n = 5) -> Nat
 20 | ffg f k n prf with (k > 5)
 21 |   ffg f k (f 5) Refl | True = ?foo_t
                 ^

Error: While processing left hand side of with block in fff. Undefined name f. 

DepInWith:26:15--26:16
 22 |   ffg f k n prf | False = ?foo_f
 23 | 
 24 | fff : (f : Nat -> Nat) -> (k, n : Nat) -> (if k > 5 then n = (if f k < 8 then 1 else 0) else n = 5) -> Nat
 25 | fff f k n prf with (k > 5)
 26 |   fff f k (if f k < 8 then 1 else 0) Refl | True = ?foo_t
                    ^

Dot pattern on the expression does not help either.

[dunhamsteve]

I was poking at this issue trying to understand it, and this seems to get further:

 ffg : (f : Nat -> Nat) -> (k, n : Nat) -> (if k > 5 then n = f 5 else n = 5) -> Nat
 ffg f k n prf with  (k > 5) | (prf)
   ffg f k (f 5) Refl | True | _ = ?foo_t
   ffg f k .(5) Refl | False | _ = ?foo_f

The with (prf) seems to get it past the (f 5). I don't know the implementation of with enough to understand why though. The 5 has to be dotted, the (f 5) works either way.

One more edit - the order of (prf) and (k > 5) don't seem to matter in this case.