fix: missing instantiateMVars

src/Init/Lean/Meta/SynthInstance.lean

@@ -173,6 +173,7 @@ forallTelescopeReducing type $ fun _ type => do
     `key` must be `mkTableKey mctx mvarType`. -/
 def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit :=
 withMCtx mctx $ do
+  trace `Meta.synthInstance.newSubgoal $ fun _ => key;
   mvarType  ← inferType mvar;
   instances ← getInstances mvarType;
   mctx      ← getMCtx;
@@ -204,6 +205,7 @@ do entry? ← findEntry key;
 def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr :=
 withMCtx mctx $ do
   mvarType ← inferType mvar;
+  mvarType ← instantiateMVars mvarType;
   pure $ mkTableKey mctx mvarType
 
 private partial def mkInstanceTelescopeAux
@@ -335,7 +337,6 @@ do (cNode, answer) ← getNextToResume;
      | none                  => pure ()
      | some (mctx, subgoals) => consume { key := cNode.key, mvar := cNode.mvar, subgoals := subgoals ++ rest, mctx := mctx }
 
-
 def step : SynthM Bool :=
 do s ← get;
    if !s.resumeStack.isEmpty then do resume; pure true

tests/lean/run/meta2.lean

@@ -5,6 +5,9 @@ open Lean.Meta
 def dbgOpt : Options :=
 let opt : Options := {};
 let opt := opt.setBool `trace.Meta true;
+let opt := opt.setBool `trace.Meta.isDefEq.step false;
+let opt := opt.setBool `trace.Meta.isDefEq.delta false;
+let opt := opt.setBool `trace.Meta.isDefEq.assign false;
 -- let opt := opt.setBool `trace.Meta.check false;
 opt
 
@@ -30,11 +33,12 @@ do env ← importModules $ mods.map $ fun m => {module := m};
      s.traceState.traces.forM $ fun m => IO.println $ format m;
      throw (IO.userError (toString err))
 
-def nat  := mkConst `Nat
-def succ := mkConst `Nat.succ
-def add  := mkConst `Nat.add
-def io   := mkConst `IO
-def type := mkSort levelOne
+def nat   := mkConst `Nat
+def boolE := mkConst `Bool
+def succ  := mkConst `Nat.succ
+def add   := mkConst `Nat.add
+def io    := mkConst `IO
+def type  := mkSort levelOne
 
 def tst1 : MetaM Unit :=
 do print "----- tst1 -----";
@@ -383,6 +387,18 @@ do print "----- tst16 -----";
 
 #eval run [`Init.Control.State] tst16
 
+def tst17 : MetaM Unit :=
+do print "----- tst17 -----";
+   prod ← mkProd nat nat;
+   prod ← mkProd boolE prod;
+   inst ← mkHasToString prod;
+   print inst;
+   (some r) ← synthInstance inst | throw $ Exception.other "failed `HasToString (Bool × (Nat × Nat))`";
+   print r;
+   pure ()
+
+#eval run [`Init.Control.State] tst17
+
 #exit
 
 def tst15 : MetaM Unit :=