Typeclass propagation loop?

Stream: lean4

[Anne Baanen]

Here's a fascinating failure I came across while implementing the concrete category refactor for MonCat:

class Bottom (X : Type)
class Left (X : Type) extends Bottom X
class Right (X : Type) extends Bottom X
class Middle₁ (X : Type) extends Left X, Right X
class Middle₂ (X : Type) extends Middle₁ X
class Top (X : Type) extends Middle₂ X

structure Bundled where
  (X : Type)
  [inst : Left X]

instance loopy [i : Middle₂ X] : Middle₂ (Bundled.mk X).X := i

set_option trace.Meta.synthInstance true in
example (X : Type) [Top X] : Right X := inferInstance
-- Fails after 256 lines of "[resume] propagating Middle₂ (Bundled.mk X).X to subgoal Middle₂ X of Middle₂ X"

I think this is because in the loopy instance, (Bundled.mk X).X can be reduced to X so somehow this gets Lean confused and makes it think has solved the wrong subgoal?

[Anne Baanen]

If we collapse Middle₁ and Middle₂ into one Middle class, we only get 128 passes through the [resume] propagating loop before we exit, which makes Lean happy to apply the instance.

[Yaël Dillies]

Yes, fascinating! Maybe that should be in #lean4 ?

[Notification Bot]

This topic was moved here from #mathlib4 > Typeclass propagation loop? by Anne Baanen.

[Jovan Gerbscheid]

using set_option pp.explicit true, we can see that each next type (of the 256) contains an extra application of loopy. The part of the code that checks whether a new instance is different from the previous ones uses ==, and it has a comment:

Remark: isDefEq here is too expensive. TODO: if == is too imprecise, add some light normalization to resultType at addAnswer