Idris is strict by default and has a stronger type system than Haskell that supports dependent typing and in effect forced the hand of the GHC developers and the wider Haskell community by showing laziness, one of the most unpopular aspects of Haskell, to be completely unnecessary for a modern, purely-functional language.<p>The strict pragma is a tacit admission that default non-strict evaluation was a mistake, and all of those who defended it here and on proggit for years should come clean and apologize for having done so, especially those who dishonestly tried to pass it off as an optimization while knowing full well that "spaceleaks" are one of the biggest performance concerns with deploying non-trivial Haskell code in production. I wrote off Haskell entirely for that very reason, and I'm not alone in having done so (search HN comments).<p>In fact, I would wager that if Haskell had not adopted such an unusual evaluation strategy, GHC would have required only a tenth of the manhours that have presently gone into it. Yes, you CS PhDs who secretly wish you were math PhDs wouldn't be able to write toy programs with infinite lists, but that's a small price to pay for lowering the language's skyscraper-steep learning curve and giving it predictable, easily reasoned-about performance characteristics.