-
Notifications
You must be signed in to change notification settings - Fork 369
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: cached results at
synthInstance?
(#4530)
Synthesized type class instances may introduce new metavariables, and we should actually cache `AbstractMVarsResult`. closes #2283
- Loading branch information
1 parent
5767a59
commit 74cdaa0
Showing
5 changed files
with
143 additions
and
65 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |