From 6d5ec050f4d2a4ced5727930d5b69707377c3c3d Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 19 May 2026 01:52:13 +1000
Subject: [PATCH] fix: instantiate metavariables when collecting a goal's
 constants (#13748)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes premise selection silently dropping relevant premises when
the goal was reached via `induction`.

`MVarId.getRelevantConstants` and `MVarId.getConstants` walked the raw
goal type returned by `getType`, which after `induction` is `?motive
arg` with `?motive` an assigned-but-unsubstituted metavariable. The
constant fold treats the metavariable as an opaque leaf, so every
constant in the goal predicate is lost. Instantiating metavariables
first recovers them.

Thanks to Xavier Généreux for the report.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 src/Lean/LibrarySuggestions/Basic.lean        | 18 ++++++++++---
 ...ibrary_suggestions_relevant_constants.lean | 27 +++++++++++++++++++
 ...tions_relevant_constants.lean.out.expected |  1 +
 3 files changed, 42 insertions(+), 4 deletions(-)
 create mode 100644 tests/elab/library_suggestions_relevant_constants.lean
 create mode 100644 tests/elab/library_suggestions_relevant_constants.lean.out.expected

diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
index 761b8324f7..ccc956c72b 100644
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -101,16 +101,26 @@ end Lean.Expr
 
 open Lean Meta MVarId in
 public def Lean.MVarId.getConstants (g : MVarId) : MetaM NameSet := withContext g do
-  let mut c := (← g.getType).getUsedConstantsAsSet
+  -- `instantiateMVars` is needed so that constants are not lost behind assigned
+  -- metavariables, e.g. the `?motive` left in a goal reached via `induction`.
+  -- Note: this does not recover constants behind non-ground delayed-assigned
+  -- metavariables. Without evidence this matters for premise selection,
+  -- for now we avoid the extra complexity of walking the metavariable graph.
+  let mut c := (← instantiateMVars (← g.getType)).getUsedConstantsAsSet
   for t in (← getLocalHyps) do
-    c := c ∪ (← inferType t).getUsedConstantsAsSet
+    c := c ∪ (← instantiateMVars (← inferType t)).getUsedConstantsAsSet
   return c
 
 open Lean Meta MVarId in
 public def Lean.MVarId.getRelevantConstants (g : MVarId) : MetaM NameSet := withContext g do
-  let mut c ← (← g.getType).relevantConstantsAsSet
+  -- `instantiateMVars` is needed so that constants are not lost behind assigned
+  -- metavariables, e.g. the `?motive` left in a goal reached via `induction`.
+  -- Note: this does not recover constants behind non-ground delayed-assigned
+  -- metavariables. Without evidence this matters for premise selection,
+  -- for now we avoid the extra complexity of walking the metavariable graph.
+  let mut c ← (← instantiateMVars (← g.getType)).relevantConstantsAsSet
   for t in (← getLocalHyps) do
-    c := c ∪ (← (← inferType t).relevantConstantsAsSet)
+    c := c ∪ (← (← instantiateMVars (← inferType t)).relevantConstantsAsSet)
   return c
 
 @[expose] public section
diff --git a/tests/elab/library_suggestions_relevant_constants.lean b/tests/elab/library_suggestions_relevant_constants.lean
new file mode 100644
index 0000000000..8b67799679
--- /dev/null
+++ b/tests/elab/library_suggestions_relevant_constants.lean
@@ -0,0 +1,27 @@
+import Lean.LibrarySuggestions.Basic
+
+/-!
+Regression test: `MVarId.getRelevantConstants` must instantiate metavariables
+in the goal type before collecting constants.
+
+A goal reached via `induction` has type `?motive arg`, where `?motive` is an
+assigned-but-unsubstituted metavariable. Without `instantiateMVars`, the
+constant fold treats `?motive` as an opaque leaf, so every constant occurring
+in the goal predicate is lost.
+-/
+
+open Lean Lean.Elab.Tactic
+
+axiom MyP : Nat → Prop
+
+example : ∀ n : Nat, MyP n := by
+  intro n
+  induction n with
+  | zero =>
+    run_tac do
+      let c ← (← getMainGoal).getRelevantConstants
+      unless c.contains ``MyP do
+        throwError "getRelevantConstants missed `MyP` hidden behind the \
+          induction motive metavariable"
+    sorry
+  | succ k ih => sorry
diff --git a/tests/elab/library_suggestions_relevant_constants.lean.out.expected b/tests/elab/library_suggestions_relevant_constants.lean.out.expected
new file mode 100644
index 0000000000..18bdd608fa
--- /dev/null
+++ b/tests/elab/library_suggestions_relevant_constants.lean.out.expected
@@ -0,0 +1 @@
+library_suggestions_relevant_constants.lean:17:0-17:7: warning: declaration uses `sorry`