fix: cached results at synthInstance? (#4530)
Synthesized type class instances may introduce new metavariables, and we should actually cache `AbstractMVarsResult`. closes #2283
This commit is contained in:
Leonardo de Moura
GitHub
parent
968aff403b
commit
33f7865bbb
5 changed files with 143 additions and 65 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
45
tests/lean/run/2283.lean
Normal file
45
tests/lean/run/2283.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue