From bde1a66075dbb2ec4fc08eac7e13f7ff0e32bdc4 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Fri, 4 Aug 2023 05:46:04 -0700
Subject: [PATCH] [ fix ] Fix pattern match issue with function application in
 Refl (#3027)

---
 CHANGELOG.md                           |  2 ++
 src/Core/Case/CaseBuilder.idr          |  8 +++++---
 tests/Main.idr                         |  2 +-
 tests/idris2/casetree004/LocalArgs.idr | 11 +++++++++++
 tests/idris2/casetree004/PiMatch.idr   |  3 +++
 tests/idris2/casetree004/expected      |  2 ++
 tests/idris2/casetree004/run           |  4 ++++
 7 files changed, 28 insertions(+), 4 deletions(-)
 create mode 100644 tests/idris2/casetree004/LocalArgs.idr
 create mode 100644 tests/idris2/casetree004/PiMatch.idr
 create mode 100644 tests/idris2/casetree004/expected
 create mode 100755 tests/idris2/casetree004/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ae2a37999..fc70675b4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -99,6 +99,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
diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr
index 257c1f1a0..46d5bd751 100644
--- a/src/Core/Case/CaseBuilder.idr
+++ b/src/Core/Case/CaseBuilder.idr
@@ -1089,7 +1089,7 @@ 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
+mkPat [] orig (Ref fc Bound n) = pure $ PLoc fc n
 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)
@@ -1107,8 +1107,10 @@ mkPat args orig (Ref fc Func n)
                 "Unmatchable function: " ++ show n
               pure $ PUnmatchable (getLoc orig) orig
 mkPat args orig (Bind fc x (Pi _ _ _ s) t)
-    = let t' = subst (Erased fc Placeholder) t in
-      pure $ PArrow fc x !(mkPat [] s s) !(mkPat [] t' t')
+    -- For (b:Nat) -> b, the codomain looks like b [__], but we want `b` as the pattern
+    = case subst (Erased fc Placeholder) t of
+        App _ t'@(Ref fc Bound n) (Erased _ _) =>  pure $ PArrow fc x !(mkPat [] s s) !(mkPat [] t' t')
+        t' =>  pure $ PArrow fc x !(mkPat [] s s) !(mkPat [] t' t')
 mkPat args orig (App fc fn arg)
     = do parg <- mkPat [] arg arg
          mkPat (parg :: args) orig fn
diff --git a/tests/Main.idr b/tests/Main.idr
index 8cfca5043..0944e6e61 100644
--- a/tests/Main.idr
+++ b/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
diff --git a/tests/idris2/casetree004/LocalArgs.idr b/tests/idris2/casetree004/LocalArgs.idr
new file mode 100644
index 000000000..0b48e56a3
--- /dev/null
+++ b/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) ()
diff --git a/tests/idris2/casetree004/PiMatch.idr b/tests/idris2/casetree004/PiMatch.idr
new file mode 100644
index 000000000..bb761b6db
--- /dev/null
+++ b/tests/idris2/casetree004/PiMatch.idr
@@ -0,0 +1,3 @@
+idMatch : Type -> Bool
+idMatch ((x : Type) -> x) = True
+idMatch _ = False
diff --git a/tests/idris2/casetree004/expected b/tests/idris2/casetree004/expected
new file mode 100644
index 000000000..72ab3a629
--- /dev/null
+++ b/tests/idris2/casetree004/expected
@@ -0,0 +1,2 @@
+1/1: Building LocalArgs (LocalArgs.idr)
+1/1: Building PiMatch (PiMatch.idr)
diff --git a/tests/idris2/casetree004/run b/tests/idris2/casetree004/run
new file mode 100755
index 000000000..bb13c37f3
--- /dev/null
+++ b/tests/idris2/casetree004/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner LocalArgs.idr --check
+$1 --no-color --console-width 0 --no-banner PiMatch.idr --check