>>11Types of all terms have to be forced (strongly normalized) at typecheck time, that's the very point of type inference and typechecking. If you don't normalize 'em, then might as well skip typechecking altogether.
That's also the reason why in dependently typed languages you have to prove that all calculations at the type level terminate. That's why all the totality bullshit there.
>>12Keep telling yourself that, keep enclosing yourself in that cozy box where your low-level shitlanguages aren't being ousted by Haskell all over the place.