Currently, we have (in Data.Type.Bool):
-- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@ type family If cond tru fls where If 'True tru fls = tru If 'False tru fls = fls
I propose adding a new equation, thus:
-- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@ type family If cond tru fls where If b same same = same If 'True tru fls = tru If 'False tru fls = fls
This new equation would allow If to reduce when we don't know the condition but we do know that both branches are the same. All three equations are *compatible* (a technical term defined in the closed type families paper), meaning that GHC ignores the ordering between them and will just choose whichever equation matches. Any objections? Thanks, Richard