# Zulip Chat Archive

## Stream: general

### Topic: instance depth again

#### Reid Barton (Sep 28 2019 at 00:53):

This seems kind of ridiculous:

import algebra.module universes u v variables {α : Type u} [discrete_field α] {β : Type v} [add_comm_group β] [vector_space α β] set_option class.instance_max_depth 36 -- 35 is not enough def is_proportional (v w : β) : Prop := ∃ r : α, w = r • v

In fact, now I see that `algebra.module`

itself also uses depth 36 shortly after defining `vector_space`

#### Sebastien Gouezel (Sep 28 2019 at 01:48):

Could you prepare a stand-alone file (independent of mathlib) that contains just the relevant definitions, and that we could show to the Lean 4 team? They want examples showing the current shortcomings of instance search, and I think this one is pretty convincing!

#### Daniel Selsam (Sep 28 2019 at 03:09):

@Reid Barton I am guessing that the only reason for such a small `max_depth`

is to prevent expensive failures elsewhere caused by diamonds. If so, the new typeclass resolution procedure in lean4 should fix this and allow a much greater default `max_depth`

. The new procedure is prototyped at:

https://github.com/dselsam/lean4/blob/tabled_typeclasses/library/init/lean/typeclass/synth.lean

Here are some tests that show it can handle diamonds and loops:

https://github.com/dselsam/lean4/blob/tabled_typeclasses/tests/lean/run/typeclass_diamond.lean

https://github.com/dselsam/lean4/blob/tabled_typeclasses/tests/lean/run/typeclass_coerce.lean

As @Sebastien Gouezel said, it would be great to find out about typeclass problems encountered in mathlib that this new procedure does not solve (as well as desired uses of typeclasses that are impossible with the current resolution procedure).

Last updated: May 14 2021 at 22:15 UTC