priority of typeclass inferences

Stream: general

[Kenny Lau]

If I proved A.to_B and A.to_C and B.to_D and C.to_D, when I want to coerce A to D, how does Lean judge which path to use?

[Mario Carneiro]

Unless you explicitly set priorities using @[priority n], the highest priority goes to the last declared instance. So if it's looking for a D and C.to_D was declared second, it uses that and looks for a C, finding A.to_C.

That said, it is possible to end up with the other path if you perform a typeclass search before the second instance is declared, or if you compose typeclass proofs, so this is why I recommend B.to_D (A.to_B inst) be defeq to C.to_D (A.to_C inst) in this circumstance.

[Kenny Lau]

is it even possible to make them defeq?

[Mario Carneiro]

sure... most "forgetful functor" type instances will have this property

[Kenny Lau]

aha, my functors are usually free functors though

[Kenny Lau]

I'm making a free group ^^

[Mario Carneiro]

do you have a particular diamond in mind?

[Kenny Lau]

aha, I had one when I analyzed onote.repr wrongly

[Kenny Lau]

i.e. providing a constructive path that nat.lt is computably well-founded

[Mario Carneiro]

By the way if you are on a quest to remove noncomputable you should start with the ordinal file which contains tons of noncomputable things

[Kenny Lau]

you're right

[Mario Carneiro]

I think you will hit your head against some hard problems and realize it's impossible eventually, but feel free to try :)

[Kevin Buzzard]

Kenny, did you follow the metric space / topological space story a couple of months ago?

[Kevin Buzzard]

Patrick was horrified to find that the _definition_ of metric space was a structure which included the metric _and_ the topology!

[Kevin Buzzard]

It turned out that it was because the mathlib people wanted the coercion from a metric space to a top space to be a forgetful functor!

[Kevin Buzzard]

Now they have the clever solution of putting the topology as part of the structure, but auto-generating it from the metric :-)

[Kevin Buzzard]

https://github.com/kbuzzard/mathlib/blob/WIP_docs/docs/WIPs/type_class_inference.md

[Kevin Buzzard]

Unfinished notes

[Kevin Buzzard]

Maybe I should add something from this thread