Fix #6783: error for @TactiC in a lambda.

Previously, it was silently dropped.

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

@@ -441,10 +441,23 @@ checkLambda' cmp r tac xps typ body target = do
     , "possiblePath   =" <+> prettyTCM possiblePath
     , "numbinds       =" <+> prettyTCM numbinds
     , "typ            =" <+> prettyA   (unScope typ)
+    , "tactic         =" <+> prettyA (tbTacticAttr tac)
     ]
   reportSDoc "tc.term.lambda" 60 $ vcat
     [ "info           =" <+> (text . show) info
     ]
+
+  -- Consume @tac@:
+  case tac of
+    A.TypedBindingInfo Nothing False -> pure ()
+    A.TypedBindingInfo{ tbFinite = True } -> __IMPOSSIBLE__
+    A.TypedBindingInfo{ tbTacticAttr = Just tactic } -> do
+      -- Andreas, 2024-02-22, issue #6783
+      -- Error out if user supplied a tactic (rather than dropping it silently).
+      _tactic <- checkTacticAttribute LamNotPi tactic
+      -- We should not survive this check...
+      __IMPOSSIBLE__
+
   TelV tel btyp <- telViewUpTo numbinds target
   if numbinds == 1 && not (null tel) then useTargetType tel btyp
   else if possiblePath then trySeeingIfPath

test/Fail/Issue6783.agda

@@ -0,0 +1,23 @@
+-- Andreas, 2024-20-22, issue #6783
+-- Error for @tactic in lambda, rather than silently dropping it.
+
+-- {-# OPTIONS -v tc.term.lambda:30 #-}
+
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Unit
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Equality
+
+super-tac : Term → TC ⊤
+super-tac hole = unify hole (lit (nat 101))
+
+bar = λ {@(tactic super-tac) n : Nat} → n + n
+
+_ : bar ≡ 202
+_ = refl
+
+-- Expected error:
+
+-- The @tactic attribute is not allowed here
+-- when checking that the expression
+-- λ {@(tactic super-tac) n : Nat} → n + n has type _4

test/Fail/Issue6783.err

@@ -0,0 +1,4 @@
+Issue6783.agda:14,11-29
+The @tactic attribute is not allowed here
+when checking that the expression
+λ {@(tactic super-tac) n : Nat} → n + n has type _4