From 74cdaa0f8a1ae0f7d1801a89a6c00c07aed21e84 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 21 Jun 2024 22:20:00 +0200 Subject: [PATCH] fix: cached results at `synthInstance?` (#4530) Synthesized type class instances may introduce new metavariables, and we should actually cache `AbstractMVarsResult`. closes #2283 --- src/Lean/Meta/AbstractMVars.lean | 7 - src/Lean/Meta/Basic.lean | 9 +- src/Lean/Meta/SynthInstance.lean | 145 +++++++++++-------- tests/lean/infoFromFailure.lean.expected.out | 2 + tests/lean/run/2283.lean | 45 ++++++ 5 files changed, 143 insertions(+), 65 deletions(-) create mode 100644 tests/lean/run/2283.lean diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index 678824eadd8e..627c4cf35c6b 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 1aadbc64b78e..79a1ca247c61 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 90016949162d..afd5129422ee 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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 diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out index 04f965edf389..ca2ea71f6f29 100644 --- a/tests/lean/infoFromFailure.lean.expected.out +++ b/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 [Meta.synthInstance] ❌ Add Bool [Meta.synthInstance] no instances for Add Bool [Meta.synthInstance.instances] #[] + [Meta.synthInstance] result diff --git a/tests/lean/run/2283.lean b/tests/lean/run/2283.lean new file mode 100644 index 000000000000..9a9b7e4ba834 --- /dev/null +++ b/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