[ fix ] Fix pattern match issue with function application in Refl

CHANGELOG.md

@@ -94,6 +94,8 @@
 
 * Fixed a bug that caused holes to appear unexpectedly during quotation of dependent pairs.
 
+* Fixed a bug that caused `f` to sometimes be replaced by `fx` after matching `fx = f x`.
+
 ### Library changes
 
 #### Prelude

src/Core/Case/CaseBuilder.idr

@@ -1089,7 +1089,16 @@ mutual
 
 export
 mkPat : {auto c : Ref Ctxt Defs} -> List Pat -> ClosedTerm -> ClosedTerm -> Core Pat
-mkPat args orig (Ref fc Bound n) = pure $ PLoc fc n
+-- Only match Bound if it is applied to an empty or unmatchable spine
+-- The latter is needed for matching (x : Nat) -> b
+mkPat args orig (Ref fc Bound n) =
+  if all unmatchable args
+     then pure $ PLoc fc n
+     else pure $ PUnmatchable (getLoc orig) orig
+  where
+    unmatchable : Pat -> Bool
+    unmatchable (PUnmatchable _ _) = True
+    unmatchable _ = False
 mkPat args orig (Ref fc (DataCon t a) n) = pure $ PCon fc n t a args
 mkPat args orig (Ref fc (TyCon t a) n) = pure $ PTyCon fc n a args
 mkPat args orig (Ref fc Func n)

tests/Main.idr

@@ -70,7 +70,7 @@ idrisTestsTermination = MkTestPool "Termination checking" [] Nothing
 idrisTestsCasetree : TestPool
 idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
        -- Case tree building
-      ["casetree001", "casetree002", "casetree003"]
+      ["casetree001", "casetree002", "casetree003", "casetree004"]
 
 idrisTestsWarning : TestPool
 idrisTestsWarning = MkTestPool "Warnings" [] Nothing

tests/idris2/casetree004/LocalArgs.idr

@@ -0,0 +1,11 @@
+import Data.Vect
+
+bar : (f : List a -> Nat) -> (xs : List a) -> Nat
+bar f xs = f xs
+
+-- Idris was putting fx@f for the first implicit (instead of fx@(f xs))
+foo : (f : List a -> Nat) -> (xs : List a) -> (0 _ : fx = f xs) -> Nat
+foo f xs Refl = bar f xs
+
+blah : (xs : List a) -> Vect (foo List.length xs Refl) ()
+blah xs = replicate (length xs) ()

tests/idris2/casetree004/expected

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

tests/idris2/casetree004/run

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