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.
> Mostly it's a usability nightmare for typeclasses
And also for Rust traits, C++ templates, etc (those are all nonterminating)
(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.)
This is the automatic resolution of some instance satisfying a typeclass constraint, and is not related to the termination of functions. This does not call a function. If you compare it to the relational definition I give at the end of the semantics section, the typechecker does not similarly infer satisfying constructers for the relation. Proof tactics can also diverge, but that's different.
It just gives up after running for too long as any Turing-complete type checkers are doing.