Fix at-pattern leak in recursive with blocks (#2834)

src/TTImp/WithClause.idr

@@ -84,9 +84,9 @@ mutual
       = matchAll True [(f, f'), (a, a)]
   -- On RHS: Rely on unification to fill in the implicit
   getMatch False (INamedApp fc f n a) f'
-      = getMatch False f f
+      = getMatch False f f'
   getMatch False (IAutoApp fc f a) f'
-      = getMatch False f f
+      = getMatch False f f'
   -- Can't have an implicit in the clause if there wasn't a matching
   -- implicit in the parent
   getMatch lhs f (INamedApp fc f' n a)

tests/Main.idr

@@ -246,7 +246,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
 idrisTestsWith : TestPool
 idrisTestsWith = MkTestPool "With abstraction" [] Nothing
       [ "with001", "with002", "with004", "with005", "with006", "with007",
-        "with008", "with009", "with010"
+        "with008", "with009", "with010", "with011"
       ]
 
 idrisTestsIPKG : TestPool

tests/idris2/with011/WithImplicits.idr

@@ -0,0 +1,9 @@
+import Data.Vect
+import Data.Vect.Views.Extra
+
+mergeSort : Ord a => {n : _} -> Vect n a -> Vect n a
+mergeSort input with (splitRec input)
+  mergeSort [] | SplitRecNil = []
+  mergeSort [x] | SplitRecOne = [x]
+  mergeSort (xs ++ ys) | (SplitRecPair {xs} {ys} xs_rec ys_rec) =
+    merge (mergeSort xs | xs_rec) (mergeSort ys | ys_rec)

tests/idris2/with011/expected

@@ -0,0 +1 @@
+1/1: Building WithImplicits (WithImplicits.idr)

tests/idris2/with011/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner -p contrib --check WithImplicits.idr