From bcfc927799d264a7973099995adff9d31a0b908b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Aug 2021 16:14:04 -0700
Subject: [PATCH] fix: fixes #602

---
 src/Lean/Meta/Basic.lean         | 15 ++++++++----
 src/Lean/Meta/ExprDefEq.lean     |  3 ++-
 src/Lean/Meta/SynthInstance.lean | 39 +++++++++++++++++++++-----------
 tests/lean/run/602.lean          | 32 ++++++++++++++++++++++++++
 4 files changed, 71 insertions(+), 18 deletions(-)
 create mode 100644 tests/lean/run/602.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 619d69c015..5dc60f7770 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -157,11 +157,18 @@ structure SavedState where
   deriving Inhabited
 
 structure Context where
-  config         : Config               := {}
-  lctx           : LocalContext         := {}
-  localInstances : LocalInstances       := #[]
+  config            : Config               := {}
+  lctx              : LocalContext         := {}
+  localInstances    : LocalInstances       := #[]
   /-- Not `none` when inside of an `isDefEq` test. See `PostponedEntry`. -/
-  defEqCtx?      : Option DefEqContext  := none
+  defEqCtx?         : Option DefEqContext  := none
+  /--
+    Track the number of nested `synthPending` invocations. Nested invocations can happen
+    when the type class resolution invokes `synthPending`.
+
+    Remark: in the current implementation, `synthPending` fails if `synthPendingDepth > 0`.
+    We will add a configuration option if necessary. -/
+  synthPendingDepth : Nat                  := 0
 
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index e325a406ca..43f5557e43 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1365,7 +1365,8 @@ end
       failK
   | none   => failK
 
-private def isDefEqOnFailure (t s : Expr) : MetaM Bool :=
+private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
+  trace[Meta.isDefEq.onFailure] "{t} =?= {s}"
   unstuckMVar t (fun t => Meta.isExprDefEqAux t s) <|
   unstuckMVar s (fun s => Meta.isExprDefEqAux t s) <|
   tryUnificationHints t s <||> tryUnificationHints s t
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index c090d430af..c2a20250ff 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -647,20 +647,32 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| withMVarContext mvarId do
   let mvarDecl ← getMVarDecl mvarId
   match mvarDecl.kind with
-  | MetavarKind.synthetic =>
+  | MetavarKind.syntheticOpaque =>
+    return false
+  | _ =>
+    /- Check whether the type of the given metavariable is a class or not. If yes, then try to synthesize
+       it using type class resolution. We only do it for `synthetic` and `natural` metavariables. -/
     match (← isClass? mvarDecl.type) with
-    | none   => pure false
-    | some _ => do
-      let val? ← catchInternalId isDefEqStuckExceptionId (synthInstance? mvarDecl.type (maxResultSize? := none)) (fun _ => pure none)
-      match val? with
-      | none     => pure false
-      | some val =>
-        if (← isExprMVarAssigned mvarId) then
-          pure false
-        else
-          assignExprMVar mvarId val
-          pure true
-  | _ => pure false
+    | none   =>
+      return false
+    | some _ =>
+      /- TODO: use a configuration option instead of the hard-coded limit `1`. -/
+      if (← read).synthPendingDepth > 1 then
+        trace[Meta.synthPending] "too many nested synthPending invocations"
+        return false
+      else
+        withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
+          trace[Meta.synthPending] "synthPending {mkMVar mvarId}"
+          let val? ← catchInternalId isDefEqStuckExceptionId (synthInstance? mvarDecl.type (maxResultSize? := none)) (fun _ => pure none)
+          match val? with
+          | none     =>
+            return false
+          | some val =>
+            if (← isExprMVarAssigned mvarId) then
+              return false
+            else
+              assignExprMVar mvarId val
+              return true
 
 builtin_initialize
   registerTraceClass `Meta.synthInstance
@@ -669,5 +681,6 @@ builtin_initialize
   registerTraceClass `Meta.synthInstance.tryResolve
   registerTraceClass `Meta.synthInstance.resume
   registerTraceClass `Meta.synthInstance.generate
+  registerTraceClass `Meta.synthPending
 
 end Lean.Meta
diff --git a/tests/lean/run/602.lean b/tests/lean/run/602.lean
new file mode 100644
index 0000000000..2a564734a3
--- /dev/null
+++ b/tests/lean/run/602.lean
@@ -0,0 +1,32 @@
+class Semiring (α : Type) where add : α → α → α
+class Ring (α : Type) where add : α → α → α
+
+class AddCommMonoid (α : Type) where
+class AddCommGroup (α : Type) where
+
+class Module (α β : Type) [Semiring α] [AddCommMonoid β] where
+
+class NormedField (α : Type) where
+  add : α → α → α
+  add_comm  : ∀ (x y : α), @Add.add _ ⟨add⟩ x y = @Add.add _ ⟨add⟩ y x
+
+class SemiNormedGroup (α : Type) where
+class SemiNormedSpace (α β : Type) [NormedField α] [SemiNormedGroup β] where
+
+instance SemiNormedGroup.toAddCommMonoid [SemiNormedGroup α] : AddCommMonoid α := {}
+instance Ring.toSemiring [instR : Ring α] : Semiring α := { add := instR.add }
+instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := instNF.add }
+
+
+-- @[inferTCGoalsRL]
+instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {}
+
+constant R : Type := Unit
+constant foo (a b : R) : R := a
+
+instance R.NormedField : NormedField R := { add := foo, add_comm := sorry }
+instance R.Ring : Ring R := { add := foo }
+
+variable {E : Type} [instSNG : SemiNormedGroup E] [instSNS : SemiNormedSpace R E]
+
+#synth Module R E