[ fix ] Fix pattern match issue with function application in Refl (#3027)

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

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

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/PiMatch.idr

@@ -0,0 +1,3 @@
+idMatch : Type -> Bool
+idMatch ((x : Type) -> x) = True
+idMatch _ = False

tests/idris2/casetree004/expected

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

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