tentative fix for the instanceNormalFormExpose problem

Author: kim-em

src/Lean/Elab/BuiltinTerm.lean

@@ -322,6 +322,16 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType
   let type ← instantiateMVars type
+  -- Rebuild type with fresh synthetic mvars for instance-implicit args, so that
+  -- synthesis is not influenced by the expected type's instance choices.
+  let type ← do
+    let fn := type.getAppFn
+    let args := type.getAppArgs
+    let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
+    for i in [:args.size] do
+      unless bis[i]!.isInstImplicit do
+        mvars[i]!.mvarId!.assign args[i]!
+    instantiateMVars (mkAppN fn mvars)
   let inst ← synthInstance type
   -- Normalize to instance normal form.
   let compile := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))

tests/elab/instanceNormalFormExpose.lean

@@ -18,6 +18,8 @@ instance [MyMonad m] : MyMonad (MyStateRefT σ m) :=
 instance [MyMonad m] [MyLawful m] : MyLawful (MyReaderT ρ m) where
   law := trivial
 
---set_option backward.isDefEq.respectTransparency false in
+instance [MyMonad m] [MyLawful m] : MyLawful (MyStateRefT σ m) :=
+  inferInstanceAs (MyLawful (MyReaderT σ m))
+
 instance [MyMonad m] [MyLawful m] : MyLawful (MyStateRefT σ m) :=
   inferInstanceAs (MyLawful (MyReaderT _ _))