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 fu

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.