From 789c7073dc901788fd40863bd7d51161a5e75104 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Aug 2021 12:09:22 -0700 Subject: [PATCH] fix: avoid eager TC synthesis at `isDefEq` --- src/Lean/Meta/ExprDefEq.lean | 15 ++++++++------ tests/lean/343.lean | 4 ++-- tests/lean/infoTree.lean.expected.out | 28 +++++++++++++-------------- 3 files changed, 25 insertions(+), 22 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index eaa03b4bb6..e325a406ca 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -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 diff --git a/tests/lean/343.lean b/tests/lean/343.lean index e3cfa3c8c3..b90367f30e 100644 --- a/tests/lean/343.lean +++ b/tests/lean/343.lean @@ -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 diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 4d36f53312..264103da1c 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -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