Incorrect interaction of nested with blocks and nested dependent pattern matching

[edwinb]

Issue by ohad
Saturday Oct 26, 2019 at 22:51 GMT
Originally opened as edwinb/Idris2-boot#141

---

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

[ohad]

I think this is another instance of this problem (with gratitude to Jonathan Tanner):

import Decidable.Equality

[EqDPair] ((x : a) -> Eq (f x), DecEq a) => Eq (DPair a f) where
  (==)  (x1 ** y1) (x2 ** y2) with (decEq x1 x2)
   (==) (x  ** y1) (x  ** y2) | Yes Refl = y1 == y2
   (==) (x1 ** y1) (x2 ** y2) | No prf = False

gives:

     With clause does not match parent at:
     4	  (==)  (x1 ** y1) (x2 ** y2) with (decEq x1 x2)

while:

[EqDPair] ((x : a) -> Eq (f x), DecEq a) => Eq (DPair a f) where
  (==)  (MkDPair x1 y1) (MkDPair x2 y2) with (decEq x1 x2)
   (==) (MkDPair x  y1) (MkDPair x  y2) | Yes Refl = y1 == y2
   (==) (MkDPair x1 y1) (MkDPair x2 y2) | No prf = False

type-checks fine.