Type-level programming is still programming

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.