max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: avoid eager TC synthesis at isDefEq

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-05 12:09:22 -07:00
parent ddbd10f610
commit 789c7073dc
3 changed files with 25 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Meta/ExprDefEq.lean
View file

@ -1293,12 +1293,15 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
else if (← isDelayedAssignedHead sFn s) then
let s ← instantiateMVars s
isDefEqQuick t s
else if (← isSynthetic tFn <&&> trySynthPending tFn) then
let t ← instantiateMVars t
isDefEqQuick t s
else if (← isSynthetic sFn <&&> trySynthPending sFn) then
let s ← instantiateMVars s
isDefEqQuick t s
/- Remark: we do not eagerly synthesize synthetic metavariables when the constraint is not stuck.
Reason: we may fail to solve a constraint of the form `?x =?= A` when the synthesized instance
is not definitionally equal to `A`. We left the code here as a remainder of this issue. -/
-- else if (← isSynthetic tFn <&&> trySynthPending tFn) then
-- let t ← instantiateMVars t
-- isDefEqQuick t s
-- else if (← isSynthetic sFn <&&> trySynthPending sFn) then
-- let s ← instantiateMVars s
-- isDefEqQuick t s
else if tFn.isMVar && sFn.isMVar && tFn == sFn then
Bool.toLBool <$> isDefEqMVarSelf tFn t.getAppArgs s.getAppArgs
else

4
tests/lean/343.lean
View file

@ -8,7 +8,7 @@ structure FunctorIsh (C D : CatIsh) where
onObj : C.Obj → D.Obj
onHom : ∀ {s d : C.Obj}, (s ~> d) → (onObj s ~> onObj d)
def Catish : CatIsh :=
abbrev Catish : CatIsh :=
{
Obj := CatIsh
Hom := FunctorIsh
@ -16,7 +16,7 @@ def Catish : CatIsh :=
universe m o
unif_hint (mvar : CatIsh) where
Catish.{m,o} =?= mvar |- mvar.Obj =?= CatIsh.{m,o}
Catish.{o,m} =?= mvar |- mvar.Obj =?= CatIsh.{m,o}
structure CtxSyntaxLayerParamsObj where
Ct : CatIsh

28
tests/lean/infoTree.lean.expected.out
View file

@ -115,20 +115,20 @@
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.865} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.818} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.867} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.820} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
y : Nat @ ⟨21, 12⟩-⟨21, 13⟩
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent
[.] `Bool : some Sort.{?_uniq.870} @ ⟨21, 28⟩-⟨21, 32⟩
[.] `Bool : some Sort.{?_uniq.823} @ ⟨21, 28⟩-⟨21, 32⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.872} @ ⟨21, 36⟩-⟨21, 39⟩
[.] `Nat : some Sort.{?_uniq.825} @ ⟨21, 36⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
fun x y b =>
let x := (x + y, x - y);
@ -239,10 +239,10 @@
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.1827} @ ⟨27, 12⟩-⟨27, 15⟩
[.] `Nat : some Type.{?_uniq.1520} @ ⟨27, 12⟩-⟨27, 15⟩
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Type.{?_uniq.1826} @ ⟨27, 18⟩-⟨27, 23⟩
[.] `Array : some Type.{?_uniq.1519} @ ⟨27, 18⟩-⟨27, 23⟩
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
Macro expansion
@ -250,17 +250,17 @@
===>
Array Nat
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Type.{?_uniq.1828} @ ⟨27, 25⟩-⟨27, 30⟩
[.] `Array : some Type.{?_uniq.1521} @ ⟨27, 25⟩-⟨27, 30⟩
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.1829} @ ⟨27, 31⟩-⟨27, 34⟩
[.] `Nat : some Type.{?_uniq.1522} @ ⟨27, 31⟩-⟨27, 34⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Sort.{?_uniq.1831} @ ⟨27, 39⟩-⟨27, 44⟩
[.] `Array : some Sort.{?_uniq.1524} @ ⟨27, 39⟩-⟨27, 44⟩
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.1832} @ ⟨27, 45⟩-⟨27, 48⟩
[.] `Nat : some Type.{?_uniq.1525} @ ⟨27, 45⟩-⟨27, 48⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@ -274,11 +274,11 @@
Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.1872} @ ⟨30, 14⟩-⟨30, 15⟩
[.] `B : some Sort.{?_uniq.1568} @ ⟨30, 14⟩-⟨30, 15⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
arg : B @ ⟨30, 8⟩-⟨30, 11⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1874} @ ⟨30, 19⟩-⟨30, 22⟩
[.] `Nat : some Sort.{?_uniq.1570} @ ⟨30, 19⟩-⟨30, 22⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
@ -291,11 +291,11 @@
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1894} @ ⟨33, 12⟩-⟨33, 15⟩
[.] `Nat : some Sort.{?_uniq.1592} @ ⟨33, 12⟩-⟨33, 15⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.1896} @ ⟨33, 19⟩-⟨33, 20⟩
[.] `B : some Sort.{?_uniq.1594} @ ⟨33, 19⟩-⟨33, 20⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen