On 27 February 2013 12:01, Raphael Gaschignard
I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a.
It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already). But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap. -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq instance TypeEq a a True instance eq ~ False => TypeEq a b eq Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique. data k :> v infix 6 :> -- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -> v where class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq -> v where instance ( TypeEq k k' eq , TyLookupCase (k :> v ': xs) k' v' eq ) => TyLookup (k :> v ': xs) k' v' where instance TyLookupCase (k :> v ': xs) k v True where instance TyLookup xs k v => TyLookupCase (k' :> v' ': xs) k v False where