This is perfectly reasonable from a GHC Core (System FC) perspective, which makes no assumptions about type family termination. Unfortunately the tricky bit is the constraint solver, which has to solve a wide range of equality constraints involving type families.
The current design makes absolutely no attempt to give them any kind of sensible operational semantics, because it is coming from a logical rather than operational perspective. Type family reduction is neither strict nor lazy as such; instead, GHC reduces essentially arbitrary redexes (and exploits given equality constraints whenever it feels like it) to try to make the program typecheck. In addition, closed type families permit reduction steps that make sense if reading them as equations, but are difficult to interpret operationally (e.g. they don’t map nicely onto case-splitting trees).
All this is good for accepting lots of programs without too many type annotations or explicit appeals to equality constraints. But it is rather bad for performance of type family reduction, and makes it difficult to translate programs that rely on term-level laziness into their type-level equivalents.
Given backwards compatibility constraints, I suspect the most feasible way forward would be to introduce a new flavour of type families with a clearly defined operational semantics (ideally compatible with lazy evaluation in term-level Haskell) but potentially less automated equational reasoning in the constraint solver. It’s quite a technically tricky area, however, so I’m not sure we’re likely to see progress any time soon.
A couple of related links that might be of interest: