I was commenting on what the effects would be from removing laziness. I'm not experienced enough in Haskell to know whether making strictness the default option

I was commenting on what the effects would be from removing laziness. I'm not experienced enough in Haskell to know whether making strictness the default option would make sense, although I've seen a quote from Simon Peyton Jones saying he'd do that if he could start over. Out of curiosity, would you know whether there exists sufficient strictness pragmas in Haskell to translate your example Idris (pseudo) code into Haskell? I often hear about performance/memory usage pitfalls with Haskell laziness, so it'd be really nice if Haskell were able to emulate Idris in this regards, by enabling enough LANGUAGE pragmas to require explicitly annotating types if laziness is desired.