From 941282ea888fc2cdb47da4baf8ef74af6e9fefb1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Apr 2026 12:54:00 +0000 Subject: [PATCH 1/2] fix: record instances unfolded by `wrapInstance` as shake dependencies --- src/Lean/Meta/WrapInstance.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Lean/Meta/WrapInstance.lean b/src/Lean/Meta/WrapInstance.lean index bbbb45cdafc0..1597d2b604bf 100644 --- a/src/Lean/Meta/WrapInstance.lean +++ b/src/Lean/Meta/WrapInstance.lean @@ -11,6 +11,7 @@ public import Lean.Meta.SynthInstance public import Lean.Meta.CtorRecognizer public import Lean.Meta.AppBuilder import Lean.Structure +import Lean.ExtraModUses /-! # Instance Wrapping @@ -133,6 +134,10 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr else return inst + -- record inferred instance as elab dependency before `whnf` may remove it + if let .const n .. := inst.getAppFn then + recordExtraModUseFromDecl n isMeta + -- Try to reduce it to a constructor. (← whnf inst).withApp fun f args => do let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo From 4ddb8d9074f42b5c5b4e2cecda5b8fe6940b649d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 May 2026 16:22:25 +0000 Subject: [PATCH 2/2] add test --- tests/elab/extraModUses.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/elab/extraModUses.lean b/tests/elab/extraModUses.lean index 591d58c76a13..dbd617502f6a 100644 --- a/tests/elab/extraModUses.lean +++ b/tests/elab/extraModUses.lean @@ -326,3 +326,16 @@ info: Entries: [public import Init.Tactics] Is rev mod use: false -/ #guard_msgs in #eval showExtraModUses + +/-! `inferInstanceAs` inputs not included in output. -/ + +#eval resetExtraModUses + +def MyNat := Nat +instance : Max MyNat := inferInstanceAs (Max Nat) + +/-- +info: Entries: [import Init.Data.Nat.Basic] +Is rev mod use: false +-/ +#guard_msgs in #eval showExtraModUses