[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.)