From 4f45a514fc82f1565620cd9a71a809f66827dba4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Aug 2021 17:28:15 -0700
Subject: [PATCH] fix: TC issue introduced by recent bug fix

This commit fixes the issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20not.20synthesizing.20issue.3F
---
 src/Lean/Meta/SynthInstance.lean | 35 +++++++++++++++-----------------
 tests/lean/366.lean.expected.out |  1 -
 tests/lean/run/tcUnivIssue.lean  | 10 +++++++++
 3 files changed, 26 insertions(+), 20 deletions(-)
 create mode 100644 tests/lean/run/tcUnivIssue.lean

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 6942f2f37c..0138078d39 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -166,7 +166,7 @@ structure Context where
   `M` to `MetaM`.
 -/
 structure State where
-  result         : Option Expr                   := none
+  result?        : Option AbstractMVarsResult    := none
   generatorStack : Array GeneratorNode           := #[]
   resumeStack    : Array (ConsumerNode × Answer) := #[]
   tableEntries   : HashMap Expr TableEntry       := {}
@@ -372,8 +372,12 @@ def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : SynthM (
 /-- Move waiters that are waiting for the given answer to the resume stack. -/
 def wakeUp (answer : Answer) : Waiter → SynthM Unit
   | Waiter.root               => do
-    if answer.result.paramNames.isEmpty && answer.result.numMVars == 0 then
-      modify fun s => { s with result := answer.result.expr }
+    /- Recall that we now use `ignoreLevelMVarDepth := true`. Thus, we should allow solutions
+       containing universe metavariables, and not check `answer.result.paramNames.isEmpty`.
+       We use `openAbstractMVarsResult` to construct the universe metavariables
+       at the correct depth. -/
+    if answer.result.numMVars == 0 then
+      modify fun s => { s with result? := answer.result }
     else
       let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
       trace[Meta.synthInstance] "skip answer containing metavariables {answerExpr}"
@@ -487,10 +491,10 @@ def step : SynthM Bool := do
   else
     pure false
 
-def getResult : SynthM (Option Expr) := do
-  pure (← get).result
+def getResult : SynthM (Option AbstractMVarsResult) := do
+  pure (← get).result?
 
-partial def synth : SynthM (Option Expr) := do
+partial def synth : SynthM (Option AbstractMVarsResult) := do
   if (← step) then
     match (← getResult) with
     | none        => synth
@@ -499,13 +503,13 @@ partial def synth : SynthM (Option Expr) := do
     trace[Meta.synthInstance] "failed"
     pure none
 
-def main (type : Expr) (maxResultSize : Nat) : MetaM (Option Expr) :=
+def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult) :=
   withCurrHeartbeats <| traceCtx `Meta.synthInstance do
      trace[Meta.synthInstance] "main goal {type}"
      let mvar ← mkFreshExprMVar type
      let mctx ← getMCtx
      let key    := mkTableKey mctx type
-     let action : SynthM (Option Expr) := do
+     let action : SynthM (Option AbstractMVarsResult) := do
        newSubgoal mctx key mvar Waiter.root
        synth
      action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}
@@ -592,19 +596,12 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
       let result? ← withNewMCtxDepth do
         let normType ← preprocessOutParam type
         trace[Meta.synthInstance] "preprocess: {type} ==> {normType}"
-        match (← SynthInstance.main normType maxResultSize) with
-        | none        => pure none
-        | some result =>
-          trace[Meta.synthInstance] "FOUND result {result}"
-          let result ← instantiateMVars result
-          if (← hasAssignableMVar result) then
-            trace[Meta.synthInstance] "Failed has assignable mvar {result.setOption `pp.all true}"
-            pure none
-          else
-            pure (some result)
+        SynthInstance.main normType maxResultSize
+      let resultHasUnivMVars := if let some result := result? then !result.paramNames.isEmpty else false
       let result? ← match result? with
         | none        => pure none
         | some result => do
+          let (_, _, result) ← openAbstractMVarsResult result
           trace[Meta.synthInstance] "result {result}"
           let resultType ← inferType result
           if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
@@ -613,7 +610,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
           else
             trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
             pure none
-      if type.hasMVar then
+      if type.hasMVar || resultHasUnivMVars then
         pure result?
       else do
         modify fun s => { s with cache := { s.cache with synthInstance := s.cache.synthInstance.insert type result? } }
diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out
index 9f91443c1d..527ce50f29 100644
--- a/tests/lean/366.lean.expected.out
+++ b/tests/lean/366.lean.expected.out
@@ -9,5 +9,4 @@
       [Meta.synthInstance.tryResolve] success
     [Meta.synthInstance.newAnswer] size: 0, Inhabited Nat
     [Meta.synthInstance.newAnswer] val: instInhabitedNat
-  [Meta.synthInstance] FOUND result instInhabitedNat
   [Meta.synthInstance] result instInhabitedNat
diff --git a/tests/lean/run/tcUnivIssue.lean b/tests/lean/run/tcUnivIssue.lean
new file mode 100644
index 0000000000..5903cd770b
--- /dev/null
+++ b/tests/lean/run/tcUnivIssue.lean
@@ -0,0 +1,10 @@
+class L0  where f : Type _
+class A0  where a : Type _
+class B0  where b : Type _
+instance [A0] [B0] : L0 := ⟨A0.a × B0.b⟩
+class A1
+instance [A1] : A0 := ⟨Nat⟩
+class L1 extends A1, B0
+class C0 [L0]
+-- instance [L1] : L0 := inferInstance
+instance [L1] : C0 := ⟨⟩