From bdd3b9e552d8064a503e6ba054d7cf18ddf03591 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 18 Dec 2024 16:34:35 -0800
Subject: [PATCH] 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 | 14 ++++++++-
 tests/lean/run/6354.lean   | 62 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/6354.lean

diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index ca169eaf96d2..444688a494ae 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/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 =>
diff --git a/tests/lean/run/6354.lean b/tests/lean/run/6354.lean
new file mode 100644
index 000000000000..9c06b0aba9d7
--- /dev/null
+++ b/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