Incorrect interaction of nested with blocks and nested dependent pattern matching

[ohad]

Sorry this is not minimal. If I have a better idea on what's happening under the hood, I'll try to minimize.

Steps to Reproduce

Foo.idr

infix 10 @@
-- DIY "with (...) proof p" construct
(@@) : (f : a -> b) -> (x : a) -> (u : b ** f x = u)
(@@) f x = ( f x ** Refl)

bar : a -> b -> (a,b)
bar x y = (x,y)

gnat : Nat -> Nat -> Nat
gnat     m n with (S @@ n, m)
  gnat   m n | ((l ** pf), k) with (plus k l) 
    gnat m n | ((l ** pf), k) | z  = ?help

Expected Behavior

$ idris2 Foo.idr
Foo> :t help
   l : Nat
   n : Nat
   pf : (S n) = l
   k : Nat
   m : Nat
   z : Nat
-------------------------------------
help : Nat

Observed Behavior

1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data/List/Foo.idr:13:18--13:20:With clause does not match parent

There's nothing wrong with the top two lines in the with block:

gnat : Nat -> Nat -> Nat
gnat     m n with (S @@ n, m)
  gnat   m n | ((l ** pf), k) {--with (plus k l) 
    gnat m n | ((l ** pf), k) | z--}  = ?help

1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data.List.Foo> :t help
   l : Nat
   n : Nat
   pf : (S n) = l
   k : Nat
   m : Nat
-------------------------------------
help : Nat

and dropping the dependent pair is also fine:

gnat : Nat -> Nat -> Nat
gnat     m n with (S n, m)
  gnat   m n | ((l ), k) with (plus k l) 
    gnat m n | ((l ), k) | z  = ?help

1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data.List.Foo> :t help
   n : Nat
   m : Nat
   z : Nat
   l : Nat
   k : Nat
-------------------------------------
help : Nat