From 3cd46888bf58dcaadbe4782819de090e7bb574f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 May 2022 06:49:14 -0700 Subject: [PATCH] fix: check types using default reducibility at `synthInstance?` closes #1131 --- src/Lean/Meta/SynthInstance.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 7287e38d5b..764033638e 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -659,7 +659,6 @@ private def preprocessOutParam (type : Expr) : MetaM Expr := def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do let opts ← getOptions let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts) - let inputConfig ← getConfig /- We disable eta for structures that are not classes during TC resolution because it allows us to find unintended solutions. See discussion at @@ -686,7 +685,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM ( let (_, _, result) ← openAbstractMVarsResult result trace[Meta.synthInstance] "result {result}" let resultType ← inferType result - if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then + if (← withDefault <| 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,