fix: cached results at synthInstance?

Synthesized type class instances may introduce new metavariables,
and we should actually cache `AbstractMVarsResult`.

closes #2283

src/Lean/Meta/AbstractMVars.lean

@@ -7,13 +7,6 @@ prelude
 import Lean.Meta.Basic
 
 namespace Lean.Meta
-
-structure AbstractMVarsResult where
-  paramNames : Array Name
-  numMVars   : Nat
-  expr       : Expr
-  deriving Inhabited, BEq
-
 namespace AbstractMVars
 
 structure State where

src/Lean/Meta/Basic.lean

@@ -222,7 +222,14 @@ structure SynthInstanceCacheKey where
   synthPendingDepth : Nat
   deriving Hashable, BEq
 
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
+/-- Resulting type for `abstractMVars` -/
+structure AbstractMVarsResult where
+  paramNames : Array Name
+  numMVars   : Nat
+  expr       : Expr
+  deriving Inhabited, BEq
+
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo

src/Lean/Meta/SynthInstance.lean

@@ -698,6 +698,83 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
+private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
+  let resultType ← inferType result
+  /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+      We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+      TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
+  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+  unless defEq do
+    trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
+  return defEq
+
+/--
+Auxiliary function for converting the `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
+-/
+private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+  let some abstResult := abstResult? | return none
+  let (_, _, result) ← openAbstractMVarsResult abstResult
+  unless (← assignOutParams type result) do return none
+  let result ← instantiateMVars result
+  /- We use `check` to propagate universe constraints implied by the `result`.
+      Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
+      but these assignments are discarded by `withNewMCtxDepth`.
+
+      TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
+            a universe metavariable from previous universe levels have been assigned or not during TC resolution.
+            We only need to perform the `check` if this kind of assignment have been performed.
+
+      The example in the issue #796 exposed this issue.
+      ```
+      structure A
+      class B (a : outParam A) (α : Sort u)
+      class C {a : A} (α : Sort u) [B a α]
+      class D {a : A} (α : Sort u) [B a α] [c : C α]
+      class E (a : A) where [c (α : Sort u) [B a α] : C α]
+      instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+      def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
+      ```
+      The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
+      resolution produces the result `@c.{u} a e α b`.
+      Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
+      but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
+      but this assignment is lost.
+  -/
+  check result
+  return some result
+
+/--
+Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
+This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
+-/
+private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+  let some abstResult := abstResult? | return none
+  if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
+    /-
+    Result does not instroduce new metavariables, thus we don't need to perform (again)
+    the `check` at `applyAbstractResult?`.
+    This is an optimization.
+    -/
+    unless (← assignOutParams type abstResult.expr) do
+      return none
+    return some abstResult.expr
+  else
+    applyAbstractResult? type abstResult?
+
+/-- Helper function for caching synthesized type class instances. -/
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+  match result? with
+  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
+  | some result =>
+    let some abstResult := abstResult? | return ()
+    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
+      -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
+      -- we don't need to perform extra checks again when reusing result.
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], numMVars := 0 }) }
+    else
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
+
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
@@ -709,66 +786,20 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
-    let s ← get
-    let rec assignOutParams (result : Expr) : MetaM Bool := do
-      let resultType ← inferType result
-      /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
-         We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
-         TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
-      let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
-      unless defEq do
-        trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
-      return defEq
     let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
-    match s.cache.synthInstance.find? cacheKey with
-    | some result =>
-      trace[Meta.synthInstance] "result {result} (cached)"
-      if let some inst := result then
-        unless (← assignOutParams inst) do
-          return none
-      pure result
-    | none        =>
-      let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    match (← get).cache.synthInstance.find? cacheKey with
+    | some abstResult? =>
+      let result? ← applyCachedAbstractResult? type abstResult?
+      trace[Meta.synthInstance] "result {result?} (cached)"
+      return result?
+    | none =>
+      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize
-      let result? ← match result? with
-        | none        => pure none
-        | some result => do
-          let (_, _, result) ← openAbstractMVarsResult result
-          trace[Meta.synthInstance] "result {result}"
-          if (← assignOutParams result) then
-            let result ← instantiateMVars result
-            /- We use `check` to propagate universe constraints implied by the `result`.
-               Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
-               but these assignments are discarded by `withNewMCtxDepth`.
-
-               TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
-                     a universe metavariable from previous universe levels have been assigned or not during TC resolution.
-                     We only need to perform the `check` if this kind of assignment have been performed.
-
-               The example in the issue #796 exposed this issue.
-               ```
-                structure A
-                class B (a : outParam A) (α : Sort u)
-                class C {a : A} (α : Sort u) [B a α]
-                class D {a : A} (α : Sort u) [B a α] [c : C α]
-                class E (a : A) where [c (α : Sort u) [B a α] : C α]
-                instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
-
-                def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
-               ```
-               The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
-               resolution produces the result `@c.{u} a e α b`.
-               Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
-               but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
-               but this assignment is lost.
-            -/
-            check result
-            pure (some result)
-          else
-            pure none
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
-      pure result?
+      let result? ← applyAbstractResult? type abstResult?
+      trace[Meta.synthInstance] "result {result?}"
+      cacheResult cacheKey abstResult? result?
+      return result?
 
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if

tests/lean/infoFromFailure.lean.expected.out

@@ -2,6 +2,8 @@ B.foo "hello" : String × String
 [Meta.synthInstance] ❌ Add String
   [Meta.synthInstance] no instances for Add String
     [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
 [Meta.synthInstance] ❌ Add Bool
   [Meta.synthInstance] no instances for Add Bool
     [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>

tests/lean/run/2283.lean

@@ -0,0 +1,45 @@
+-- This file produces:
+-- PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:839:14: unknown metavariable
+
+-- from Mathlib.CategoryTheory.Category.Basic
+class Category.{v, u} (obj : Type u) : Type max u (v + 1) where
+
+-- from Mathlib.CategoryTheory.Functor.Basic
+structure Functor' (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂ where
+
+-- from Mathlib.CategoryTheory.Types
+instance : Category (Type u) := sorry
+
+-- from Mathlib.CategoryTheory.Limits.HasLimits
+section
+
+variable {J : Type u₁} [Category.{v₁} J] {C : Type u} [Category.{v} C]
+
+class HasLimit (F : Functor' J C) : Prop where
+class HasLimitsOfSize (C : Type u) [Category.{v} C] : Prop where
+  has_limit : ∀ (J : Type u₁) [Category.{v₁} J] (F : Functor' J C), HasLimit F
+
+instance {J : Type u₁} [Category.{v₁} J] [HasLimitsOfSize.{v₁, u₁} C] (F : Functor' J C) : HasLimit F :=
+  sorry
+
+def limit (F : Functor' J C) [HasLimit F] : C := sorry
+def limit.π (F : Functor' J C) [HasLimit F] (j : J) : sorry := sorry
+
+end
+
+-- from Mathlib.CategoryTheory.Limits.Types
+instance hasLimitsOfSize : HasLimitsOfSize.{v} (Type max v u) := sorry
+
+set_option pp.mvars false
+/--
+error: type mismatch
+  limit.π (sorryAx (Functor' ?_ ?_)) (sorryAx ?_)
+has type
+  sorryAx (Sort _) : Sort _
+but is expected to have type
+  limit f → sorryAx (Sort _) : Sort (imax (max (u + 1) (v + 1)) _)
+-/
+#guard_msgs in
+theorem pi_lift_π_apply {C : Type v} [Category.{v} C] (f : Functor' C (Type max v u)) :
+    (limit.π sorry sorry : limit f → sorry) sorry = sorry :=
+  sorry