type families not advertised for 6.8

[Simon Peyton-Jones]

| But the problem in the HList example is that two equations apply where the
| most specific one should be taken.

There is no difficulty in principle with this.  You just need to state (and implement) the rule that the most specific equation applies.  That is, there's no reason in principle you should not be able to write
        type instance Eq t t = True
        type instance Eq a b = False

BUT, we need to take care here.  There is one way in which indexed type family instances differ in a fundamental way from type-class instances (and hence FDs).  Suppose we have
    module M where
        class C a where { foo :: ... }
        instance C [a] where ...
Now suppose you import this into module X
    module X where
        import M
        instance C [Int] where ...

Now, with type classes it's sort-of-OK that inside M we'll use one instance decl for (C [Int]), but a different one inside X.  OK, so the two implementations of method foo will be different, but the program won't crash.

Things are different with type families.  Suppose we have

    module M where
        type family F :: * -> *
        type instance F [a] = a
    module X where
        import M
        type instance F [Int] = Bool

Then you'll get a *seg fault* if you use the F [a] instance in one place, and the F [Int] instance in another place, when resolving a constraint involving F [Int]!  (Because Bool /= Int.)  That is why the current impl strictly rules out overlap for type families.

Our proposed solution is that you can only use overlapping type-family instances for "closed" type families; here "closed" means that you can't add "more" instance later.  Something like this:
        type family Eq :: * -> * -> * where
          Eq t t = True
          Eq t1 t2 = False

(The 'where' means it's a closed family.)  Which is fine for the application you mention.  Of course none of this is implemented!

Simon