But once you have purity you don't need strictness - Idris takes that approach.

Implicit, pervasive laziness makes performance non-compositional and more or less impossible to reason about. AIUI the largest industrial deployment of Haskell uses a strict variant for this reason.