Zulip Chat Archive

Stream: general

Topic: instance depth again


view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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