typeclass resolution

Stream: general

[Bhavik Mehta]

Out of interest, how does typeclass resolution happen in lean? For example, is it acceptable and/or sensible to write both of the following:

instance mono_prod_of_left {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [mono f] : mono (limits.prod.lift f g) :=
instance mono_prod_of_right {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [mono g] : mono (limits.prod.lift f g) :=

In Haskell for instance, I'd get complained at because of overlapping instances - do we get similar problems in lean?

[Mario Carneiro]

No, you have a different problem in lean, exponential blowup, because lean tries all the paths if you do this

[Mario Carneiro]

it is sensible to do, it is like prolog

[Bhavik Mehta]

Okay great, thanks!

[Gabriel Ebner]

Mario Carneiro said:

No, you have a different problem in lean, exponential blowup, because lean tries all the paths if you do this

Where does exponential blow-up happen here? Is there some other mono instance I'm missing? With these two instances, Lean will only search mono h for all subterms h, so this should be linear. Following me, Bhavik's instances are perfectly fine (or at least just as bad as every instance we have in mathlib).

[Mario Carneiro]

ah that's true, I shouldn't have suggested that that instance setup is exponential. I meant in general it can lead to exponential blowup, but with just those instances it is linear.