Editing GHC/Type families (section)

==== Closed family simplification ====

Included in ghc starting 7.8.1.

When dealing with closed families, simplifying the type is harder than just finding a left-hand side that matches and replacing that with a right-hand side. GHC will select an equation to use in a given type family application (the "target") if and only if the following 2 conditions hold:

# There is a substitution from the variables in the equation's LHS that makes the left-hand side of the branch coincide with the target.
# For each previous equation in the family: either the LHS of that equation is ''apart'' from the type family application, '''or''' the equation is ''compatible'' with the chosen equation.

Now, we define ''apart'' and ''compatible'':
# Two types are ''apart'' when one cannot simplify to the other, even after arbitrary type-family simplifications
# Two equations are ''compatible'' if, either, their LHSs are apart or their LHSs unify and their RHSs are the same under the substitution induced by the unification.

Some examples are in order:
<haskell>
type family F a where
  F Int  = Bool
  F Bool = Char
  F a    = Bool

type family And (a :: Bool) (b :: Bool) :: Bool where
  And False c     = False
  And True  d     = d
  And e     False = False
  And f     True  = f
  And g     g     = g
</haskell>

In <hask>F</hask>, all pairs of equations are compatible except the second and third. The first two are compatible because their LHSs are apart. The first and third are compatible because the unifying substitution leads the RHSs to be the same. But, the second and third are not compatible because neither of these conditions holds. As a result, GHC will not use the third equation to simplify a target unless that target is apart from <hask>Bool</hask>.

In <hask>And</hask>, ''every'' pair of equations is compatible, meaning GHC never has to make the extra apartness check during simplification.

Why do all of this? It's a matter of type safety. Consider this example:

<haskell>
type family J a b where
  J a a = Int
  J a b = Bool
</haskell>

Say GHC selected the second branch just because the first doesn't apply at the moment, because two type variables are distinct. The problem is that those variables might later be instantiated at the same value, and then the first branch would have applied. You can convince this sort of inconsistency to produce <hask>unsafeCoerce</hask>.

It gets worse. GHC has no internal notion of inequality, so it can't use previous, failed term-level GADT pattern matches to refine its type assumptions. For example:

<haskell>
data G :: * -> * where
 GInt  :: G Int
 GBool :: G Bool

type family Foo (a :: *) :: * where
 Foo Int = Char
 Foo a   = Double

bar :: G a -> Foo a
bar GInt  = 'x'
bar _     = 3.14
</haskell>

The last line will fail to typecheck, because GHC doesn't know that the type variable <hask>a</hask> can't be <hask>Int</hask> here, even though it's obvious. The only general way to fix this is to have inequality evidence introduced into GHC, and that's a big deal and we don't know if we have the motivation for such a change yet.