instance depth again

Stream: general

[Reid Barton]

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]

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]

@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).