fix: missing universe assignments made during TC resolution
closes #796
This commit is contained in:
Leonardo de Moura
parent
a91b861919
commit
a3361e7d86
4 changed files with 126 additions and 38 deletions
|
|
@ -712,6 +712,8 @@ where
|
|||
checkLetRecsToLiftTypes funFVars letRecsToLift
|
||||
withUsed vars headers values letRecsToLift fun vars => do
|
||||
let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
|
||||
for preDef in preDefs do
|
||||
trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
|
||||
let preDefs ← levelMVarToParamPreDecls preDefs
|
||||
let preDefs ← instantiateMVarsAtPreDecls preDefs
|
||||
let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ import Lean.Meta.Basic
|
|||
import Lean.Meta.Instances
|
||||
import Lean.Meta.AbstractMVars
|
||||
import Lean.Meta.WHNF
|
||||
import Lean.Meta.Check
|
||||
import Lean.Util.Profile
|
||||
|
||||
namespace Lean.Meta
|
||||
|
|
@ -682,6 +683,32 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
|
|||
let resultType ← inferType result
|
||||
if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
|
||||
let result ← instantiateMVars result
|
||||
/- We use `check` to propogate universe constraints implied by the `result`.
|
||||
Recall that we use `ignoreLevelMVarDepth := 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
|
||||
trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
|
||||
|
|
|
|||
|
|
@ -1,33 +1,3 @@
|
|||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
|
|
@ -62,8 +32,12 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
|
||||
@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
|
|
@ -77,12 +51,8 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
|
||||
@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
|
|
@ -131,3 +101,33 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
|
|
|
|||
59
tests/lean/run/796.lean
Normal file
59
tests/lean/run/796.lean
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
namespace Ex1
|
||||
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 a] (α : Sort u) [B a α] : D α := ⟨⟩
|
||||
end Ex1
|
||||
|
||||
namespace Ex2
|
||||
class C where f : Sort u → Nat
|
||||
class D extends C
|
||||
def a [C] := C.f Nat
|
||||
def b [D] := D.toC.f Nat
|
||||
def c [D] := C.f Nat
|
||||
end Ex2
|
||||
|
||||
namespace Ex3
|
||||
section
|
||||
variable (N : Type _)
|
||||
class Zero where
|
||||
zero : N
|
||||
export Zero (zero)
|
||||
class Succ where
|
||||
succ : N → N
|
||||
export Succ (succ)
|
||||
class Succ_Not_Zero [Zero N] [Succ N] where
|
||||
succ_not_zero {n : N} : succ n ≠ zero
|
||||
export Succ_Not_Zero (succ_not_zero)
|
||||
class Eq_Of_Succ_Eq_Succ [Succ N] where
|
||||
eq_of_succ_eq_succ {n m : N} (h : succ n = succ m) : n = m
|
||||
export Eq_Of_Succ_Eq_Succ (eq_of_succ_eq_succ)
|
||||
class Nat_Induction [Zero N] [Succ N] where
|
||||
nat_induction {P : N → Sort _}
|
||||
(P0 : P zero)
|
||||
(ih : (k : N) → P k → P (succ k))
|
||||
(n : N) : P n
|
||||
export Nat_Induction (nat_induction)
|
||||
end
|
||||
|
||||
section
|
||||
variable (N : Type _)
|
||||
class Natural
|
||||
extends Zero N, Succ N, Succ_Not_Zero N, Eq_Of_Succ_Eq_Succ N, Nat_Induction N
|
||||
end
|
||||
|
||||
section
|
||||
variable {ℕ} [Natural ℕ]
|
||||
def pred_with_proof (n : ℕ) (h : n ≠ zero) : Σ' m, n = succ m :=
|
||||
by
|
||||
revert h
|
||||
let P (k : ℕ) := k ≠ zero → Σ' m, k = succ m
|
||||
exact (nat_induction (by simp ; exact False.elim) (λ k _ _ => ⟨k, rfl⟩) n : P n)
|
||||
|
||||
def pred (n : ℕ) (h : n ≠ zero) : ℕ := (pred_with_proof n h).fst
|
||||
end
|
||||
end Ex3
|
||||
Loading…
Add table
Reference in a new issue