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

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,124 @@
+import Lean
+/-!
+# Proper handling of delayed assignment metavariables in `match` elaboration
+
+https://github.com/leanprover/lean4/issues/5925
+https://github.com/leanprover/lean4/issues/6354
+
+These all had the error `(kernel) declaration has metavariables '_example'`
+due to underapplied delayed assignment metavariables never being instantiated.
+-/
+
+namespace Test1
+/-!
+Simplified version of example from issue 6354.
+-/
+
+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 6354 (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 6354 (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
+
+
+namespace Test4
+/-!
+Example from issue 5925 (by @Komyyy)
+-/
+
+def Injective (f : α → β) : Prop :=
+  ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+
+axiom my_mul_right_injective {M₀ : Type} [Mul M₀] [Zero M₀] {a : M₀} (ha : a ≠ 0) :
+  Injective fun (x : M₀) ↦ a * x
+
+def mul2 : { f : Nat → Nat // Injective f } := ⟨fun x : Nat ↦ 2 * x, my_mul_right_injective nofun⟩
+
+end Test4
+
+
+namespace Test5
+/-!
+Example from issue 5925 (by @mik-jozef)
+-/
+
+structure ValVar (D: Type) where
+  d: D
+  x: Nat
+
+def Set (T : Type) := T → Prop
+
+structure Salg where
+  D: Type
+  I: Nat
+
+def natSalg: Salg := { D := Nat, I := 42 }
+
+inductive HasMem (salg: Salg): Set (Set (ValVar salg.D))
+| hasMem
+  (set: Set (ValVar salg.D))
+  (isElem: set ⟨d, x⟩)
+:
+  HasMem salg set
+
+def valVarSet: Set (ValVar Nat) :=
+  fun ⟨d, x⟩ => x = 0 ∧ d = 0 ∧ d ∉ []
+
+-- Needed to add a unification hint to this test
+-- because of https://github.com/leanprover/lean4/pull/6024
+unif_hint (s : Salg) where
+  s =?= natSalg
+  |-
+  Salg.D s =?= Nat
+
+def valVarSetHasMem: HasMem natSalg valVarSet :=
+  HasMem.hasMem
+    valVarSet
+    (show valVarSet _ from ⟨rfl, rfl, nofun⟩)
+
+end Test5