[Haskell-cafe] Type-level lazy bool operations

[Oleg]

> 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.