I'm under the impression that SPJ made that comment thinking of adoption (for a future "regrettably popular" Haskell), since the difficulty of reasoning about laziness does put people off. I might be wrong though: maybe he was arguing that laziness doesn't warrant the user and compiler-author cost it brings. I don't remember where I picked this up from.

Idris is strict too, but optional laziness is built into the compiler with the use of a special-cased Lazy wrapper of the form

  data Lazy a = Delay a

This is kind of the opposite of strictness annotations (bang-patterns) from Haskell, except one doesn't need to pattern-match on Delay or use it to wrap arguments to functions expecting Lazy values. The Idris compiler can do something like "laziness analysis" (admittedly trivial in comparison to GHC's strictness analyser) to introduce and eliminate Delay constructors automatically. The laziness information is carried around in the types:

  force : Lazy a -> a
  force a = a

https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ#...

(purescript-lazy is also a thing, but I think it's not as seamless because of the "no compiler magic" position.)

In any case, what about -XStrict? I've never used it (or -XStrictData either), but isn't it a solution to the laziness problem, albeit a nuke-ish one at that?

And while we're thinking ahead, let's talk about the project to get linear types (something similar to Rust lifetimes, but weaker) into GHC :)

https://ghc.haskell.org/trac/ghc/wiki/LinearTypes