Zulip Chat Archive

Stream: mathlib4

Topic: instance search sees through type synonyms


Jireh Loreaux (Nov 29 2022 at 17:44):

on mathlib4#783 I ran into a very concerning issue. The declaration toLex_mono (and similarly toLex_strictMono) picks up the wrong Preorder instance on α ×ₗ β despite having the type annotation toLex : α × β → α ×ₗ β. It instead uses the non-lexicographic preorder (i.e., the prod preorder) on α ×ₗ β. This seems like a bug and an important one to fix (it took me a while to figure out this was the problem when the proof was just randomly broken). I don't think Lean should be blasting right through type synonyms on its type class search.

Scott Morrison (Nov 29 2022 at 17:52):

Hopefully this is covered by https://github.com/leanprover/lean4/issues/1891, for which we'll have a fix tomorrow.

Scott Morrison (Nov 29 2022 at 17:52):

It is at least a related error, but I haven't thought about whether it applies here.

Jireh Loreaux (Nov 29 2022 at 17:53):

That seems like the same issue, thanks.


Last updated: Dec 20 2023 at 11:08 UTC