Isn't the issue a bit more complex? The way I see it, the difference between the type level and the value level is that at the type level we want to do reasoning rather than just evaluation.
That is an excellent point! I wish the design of Haskell type-level features has kept that in mind. For example, given the closed type families type family F1 a where F1 Int = True F1 a = False type family F2 a where F2 Int = Char F2 a = Bool wouldn't it be nice if (F1 a ~ True) were to simplify to (a ~ Int)? Then the following term t1 would not have been ambiguous data Proxy (a::Bool) = Proxy foo :: Proxy (F1 a) -> a -> String foo = undefined t1 = foo (Proxy :: Proxy True) 1 And wouldn't it be nice if (F1 a ~ False, F2 a ~ b) were to simplify to (b ~ Bool)? Alas, such considerations were explicitly out of scope when type families, open or closed, were designed. We wouldn't have had to wait so long for injective type families; with the proper design, the need for such feature would've been obvious from the beginning.