Excellent write up! Cheers!
As I understand, this could alternatively be solved if there were some kind of laziness in the types. There’s no need to evaluate all the arguments to a type family before they’re matched on, right? Of course, it’s very easy for me to assert this in absence of GHC doing it, since there must be a reason it hasn’t been worked on.
Not only did I learn something valuable, but your writing style is really great! Hope to read many more articles on your blog.
The type level evaluation order is unspecified in GHC (last I checked). It has even varied between releases. That makes it hard to write robust code.
always a pleasure to read one of your articles, i always learn something … if Haskell truly is a ‘impractical academic obsession’ than at least it’s a great ‘impractical academic obsession’ and i can still love it the way i love anything else (it’s my favorite child actually)
some day perhaps we’ll see type-level thinking become the norm, even if there’s a couple hiccups like a O(2^n) If class 
; typed dataframes prove how cool and useful it can be!