That's demonstrably false (Coq will do this for you handily), but furthermore you're missing the point entirely!
Any worthwhile type-checking algorithm (like Haskell's) would have to Scoop the Loop Snooper to accept every valid formula and deny all invalid or undecidable ones. Of course they don't actually do that, instead accepting incompleteness -- that there will be valid code that they reject.
I agree, but that's not too practical. I mean, give me a system that will show [] to satisfy monad laws. You won't, because the definition of >>= for [] involves concat and map... both functions are recursive, and you know your system is going to reject that because it's not part of your strongly normalizing language, consequently rejecting [] as a monad.
Yes, it will work if you redefine the list constructors as functions...
(:) x xs = \f z -> f x (xs f z)
[] = \f z -> z
... and then we can define fold in a non-recursive way... but can this work in Haskell?
