Fix #7154: Application: check for sufficient arity before checking ta…

…rget

Closes #7154

src/full/Agda/TypeChecking/Rules/Application.hs

@@ -679,6 +679,11 @@ checkArgumentsE'
                       then skip x
                       else skip 0
                 IsRigid -> do
+                  -- Andreas, 2024-03-01, issue #7154 reported by Amy.
+                  -- We need to check that the arity of the function type
+                  -- is sufficient before checking the target,
+                  -- otherwise the target is non-sensical.
+                  if visiblePis < sArgsLen then return s else do
 
                       -- Is any free variable in tgt less than
                       -- visiblePis?

test/Fail/Issue7154.agda

@@ -0,0 +1,34 @@
+-- Andreas, 2024-03-01, issue #7154
+-- reported and test case by Amy.
+--
+-- Regression in 2.5.4 concerning error message
+-- given when non-function is applied.
+
+-- {-# OPTIONS -v tc.term.args:30 #-}
+
+data Nat : Set where
+  zero : Nat
+  suc  : Nat → Nat
+
+record T : Set where
+  field
+    f : Nat → Nat
+
+foo : T
+foo .T.f = suc
+
+test : Nat
+test = foo zero
+
+-- Wrong error (since Agda 2.5.4)
+--
+-- T !=< Nat of type Set
+-- when checking that the inferred type of an application
+--   T
+-- matches the expected type
+--   Nat
+--
+-- Expected error (given until Agda 2.5.3):
+--
+-- T should be a function type, but it isn't
+-- when checking that zero is a valid argument to a function of type T

test/Fail/Issue7154.err

@@ -0,0 +1,3 @@
+Issue7154.agda:21,8-11
+T should be a function type, but it isn't
+when checking that zero is a valid argument to a function of type T