Type-checked non-empty strings

This is very cool! But it does seem like a hack. I wish dependent Haskell the best of luck.

Sidenote, I find it odd that Simon Peyton Jones (who seems to be the most famous of those involved in original Haskell development) quite often talks about languages with interesting type systems and never once mentions proof assistant languages like Agda, Idris, Lean, Rocq, …; I suppose he doesn’t consider them “programming languages”?