It isn’t just DT:
New type of ($) operator in GHC 8.0 is problematic
…Haskell: now the world’s finest imperative intermediate language?
Some time ago, there was an expression of interest in “embedding Elm in Haskell”. My final remark on that topic was to suggest adding laziness to Elm instead - to me, it seemed a simpler task.
Since the likes of Agda, Idris et al already support [the complexity of] DT, that same suggestion would also seem to apply - it would be easier to implement laziness in Agda or Idris, instead of retrofitting DT into Haskell, as the extra complexity of supporting nonstrict semantics would largely be confined to the implementation.
But perhaps the “dependenting of Haskell” may be a “rip-roaring success” that inspires the embedding of Elm into Haskell: anyone for elm-notation…?