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
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