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

fix: check types using default reducibility at synthInstance?

Browse source 
closes #1131
This commit is contained in:
Leonardo de Moura 2022-05-08 06:49:14 -07:00
parent 0fd47fd817
commit 3cd46888bf
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Meta/SynthInstance.lean
View file

@ -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,