From 02b6fb3f41880209052bd024560b10f4122647ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 May 2024 20:13:41 +0200 Subject: [PATCH] fix: `canonInstances := true` issue (#4216) closes #4213 --- src/Lean/Meta/SynthInstance.lean | 12 +++++++++--- tests/lean/run/4213.lean | 4 ++++ 2 files changed, 13 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/4213.lean diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 84e36f784d..bae085dae9 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -561,11 +561,17 @@ def generate : SynthM Unit := do if backward.synthInstance.canonInstances.get (← getOptions) then unless gNode.typeHasMVars do if let some entry := (← get).tableEntries.find? key then - unless entry.answers.isEmpty do + if entry.answers.any fun answer => answer.result.numMVars == 0 then /- - We already have an answer for this node, and since its type does not have metavariables, - we can skip other solutions because we assume instances are "morally canonical". + We already have an answer that: + 1. its result does not have metavariables. + 2. its types do not have metavariables. + + Thus, we can skip other solutions because we assume instances are "morally canonical". We have added this optimization to address issue #3996. + + Remark: Condition 1 is important since root nodes only take into account results + that do **not** contain metavariables. This extra check was added to address issue #4213. -/ modify fun s => { s with generatorStack := s.generatorStack.pop } return diff --git a/tests/lean/run/4213.lean b/tests/lean/run/4213.lean new file mode 100644 index 0000000000..f7eddcde9b --- /dev/null +++ b/tests/lean/run/4213.lean @@ -0,0 +1,4 @@ +class FooClass (α : Type _) : Prop where + +theorem bar (α ι : Type _) [FooClass α] (f : ι → FooClass α) : FooClass α := by + infer_instance