| 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
