[tlringer]

Typeclass resolution is implemented as a layer of automation that is above the type-checking kernel, so much like with nonterminating tactics, if it doesn't halt you mostly just end up with confusing automation that doesn't help you prove something, but you shouldn't be able to prove false. Mostly it's a usability nightmare for typeclasses, and in the case of this post also a way for hilarity to ensue.

[nextaccountic]

> Mostly it's a usability nightmare for typeclasses

And also for Rust traits, C++ templates, etc (those are all nonterminating)

[tlringer]

(Conflating a few things here, and only noticing now; there are also languages with undecidable type checking in which one cannot prove false, mostly because of fancy equality checking, though that's undesirable in some ways. But it's not accurate to think of typeclass resolution as part of the type checker IMO. It is in a layer similar to tactics.)