Implement recursive compatibility check for closed type families.

Now, on a closed type family, two branches are considered compatible
if their RHSs **normalize** to the same type. Previously, the RHSs
had to be identical (under the unifying substitution). This allows
more reductions -- yay.

CAVEAT: This is probably not type-safe with UndecidableInstances.
Someone (er... me) has to Think Hard about this before merging.
It might be unsafe even with imported non-terminating instances
(so, without UndecidableInstances in the same module).
There's a change this isn't type-safe even without UndecidableInstances,
but I'm not too worried about that possibility.