Instance loop

Stream: mathlib4

[David Loeffler]

Am I correct in believing that instance loops are troublesome for the typeclass machinery?

I just noticed that, for a topological space X, we have instances showing that

"if X is TotallySeparated, then it is TotallyDisconnected" (here: docs#TotallySeparatedSpace.totallyDisconnectedSpace)

and also

"if X is TotallyDisconnected and also compact Hausdorff, then it is TotallySeparated" (here: docs#instTotallySeparatedSpace)

My understanding was that this sort of thing -- having two instances "A implies B" and "B and C imply A" -- was problematic, and usually the solution was that the second implication shouldn't be an instance. However, for this example, having both instances so far doesn't seem to be causing problems, and removing the second instance causes various proofs about profinite spaces to break.

[Ruben Van de Velde]

This didn't work in lean 3 but it's supposed to work in lean 4. There may still be rough edges, though, because it's not used all that much

[Yaël Dillies]

Lean 4 automatically handles instance loops so long as the looping typeclass searches are strictly identical. In practice this means that the same (but not strictly the same, eg because of the instance arguments being defeq but not synteq) typeclass search can be performed several times before the loop stabilizes

[Eric Wieser]

Is stabilization guaranteed?

[Yaël Dillies]

I am confident we could find a counter-example given some effort :smiling_devil:

[Yaël Dillies]

In fact, it might as easy as digging up one of the few PRs that tried adding those looping instances. Some went through, some didn't because of timeouts. I assume those timeouts were due to non-stabilization of the TC calls.

[Eric Wieser]

I guess I'm asking about the more abstract distinction between intractably long and actually non-terminating

[Daniel Weber]

This works, although this might not be exactly what you mean

class C (α : Type) where
class D (α : Type) where

instance i1 [C α] : D α := sorry
instance i2 [D (id α)] : C α := sorry

variable {α : Type}

#synth D α

[Eric Wieser]

Yeah, that's not really what I mean, since it reproduces as

class C (α : Type) where
instance i [C (id α)] : C α := sorry

[Daniel Weber]

I claim that all non-terminating loops are essentially this, with more complicated id functions and possible in implicit/instance variables of the class