# Zulip Chat Archive

## Stream: general

### Topic: typeclass resolution

#### Bhavik Mehta (Mar 16 2020 at 22:31):

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 (Mar 16 2020 at 22:33):

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

#### Mario Carneiro (Mar 16 2020 at 22:33):

it is sensible to do, it is like prolog

#### Bhavik Mehta (Mar 16 2020 at 22:35):

Okay great, thanks!

#### Gabriel Ebner (Mar 17 2020 at 09:27):

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 (Mar 17 2020 at 09:44):

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.

Last updated: May 10 2021 at 00:31 UTC