fix: process delayed assignment metavariables correctly in Lean.Meta.…

…Closure

This PR fixes a bug in `Lean.Meta.Closure` that would introduce under-applied delayed assignment metavariables, which would keep them from ever getting instantiated. This bug affected `match` elaboration when the expected type contains postponed elaboration problems, for example tactic blocks.

Closes #6354

src/Lean/Meta/Closure.lean

@@ -203,9 +203,21 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
     let type ← collect type
     let newFVarId ← mkFreshFVarId
     let userName ← mkNextUserName
+    /-
+    If the metavariable is a delayed assignment, it would be an error to push it onto `exprMVarArgs` directly,
+    since the assumption is that delayed assignment metavariables are always fully applied (for example `instantiateMVars` assumes this).
+    The need to handle delayed assignment metavariables was uncovered in issue https://github.com/leanprover/lean4/issues/6354
+    -/
+    let e' ←
+      if let some { fvars, .. } ← getDelayedMVarAssignment? mvarId then
+        -- Eta expand `e` for the requisite number of arguments.
+        forallBoundedTelescope mvarDecl.type fvars.size fun args _ => do
+          mkLambdaFVars args <| mkAppN e args
+      else
+        pure e
     modify fun s => { s with
       newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ .cdecl default newFVarId userName type .default .default,
-      exprMVarArgs          := s.exprMVarArgs.push e
+      exprMVarArgs          := s.exprMVarArgs.push e'
     }
     return mkFVar newFVarId
   | Expr.fvar fvarId =>

tests/lean/run/6354.lean

@@ -0,0 +1,62 @@
+/-!
+# Proper handling of delayed assignment metavariables in `match` elaboration
+
+https://github.com/leanprover/lean4/issues/6354
+-/
+
+namespace Test1
+/-!
+Simplified version of example from issue 6354.
+Previously, had error `(kernel) declaration has metavariables '_example'`
+-/
+
+structure A where
+  p: Prop
+  q: True
+
+example := (λ ⟨_,_⟩ ↦ True.intro : (A.mk (And True True) (by exact True.intro)).p → True)
+
+end Test1
+
+
+namespace Test2
+/-!
+Example from issue (by @roos-j)
+-/
+
+structure A where
+  p: Prop
+  q: True
+
+structure B extends A where
+  q': p → True
+
+example: B where
+  p := True ∧ True
+  q := by exact True.intro
+  q' := λ ⟨_,_⟩ ↦ True.intro
+
+end Test2
+
+
+namespace Test3
+/-!
+Example from issue comment (by @b-mehta)
+-/
+
+class Preorder (α : Type) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+
+class PartialOrder (α : Type) extends Preorder α where
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+inductive MyOrder : Nat × Nat → Nat × Nat → Prop
+  | within {x u m : Nat} : x ≤ u → MyOrder (x, m) (u, m)
+
+instance : PartialOrder (Nat × Nat) where
+  le := MyOrder
+  le_refl x := .within (Nat.le_refl _)
+  le_antisymm | _, _, .within _, .within _ => Prod.ext (Nat.le_antisymm ‹_› ‹_›) rfl
+
+end Test3