4 ms·

But Coq is strongly normalizing… it always halts. What gives?

• thaliaarchi 3y ago
  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.
• tlringer 3y ago
  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 3y ago
    > Mostly it's a usability nightmare for typeclasses And also for Rust traits, C++ templates, etc (those are all nonterminating)
  • tlringer 3y ago
    (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.)
• _0w8t 3y ago
  It just gives up after running for too long as any Turing-complete type checkers are doing.