Prior art for a strict language - it may be easier to reimplement default and prioritised instances in another strict or total language rather than Haskell. (Of course, there’s another option: bring laziness to the likes of Lean, Idris, and Agda - any expression not used by dependent types can still be lazy! :-)