Type constraints on all type family instances

Question

I suppose what I want is impossible without Template Haskell but I'll ask anyway.

I have an interface for types like Data.Set and Data.IntSet:

type family Elem s :: *
class SetLike s where
  insert :: Elem s -> s -> s
  member :: Elem s -> s -> Bool
  ...

type instance Elem (Set a) = a
instance Ord a => SetLike (Set a) where
  ...

And I have a type family which chooses optimal set implementation:

type family EfficientSet elem :: *
type instance EfficientSet Int = IntSet
type instance EfficientSet String = Set String -- or another implementation

Is there a way to guarantee that EfficientSet instances will be always SetLike and that Elem (EfficientSet a) is a ?

Without this guarantee all function signatures will be like this:

type LocationSet = EfficientSet Location
f :: (SetLike LocationSet, Elem LocationSet ~ Location) => ...

To write each time SetLike LocationSet is somewhat tolerable, but Elem LocationSet ~ Location makes code understanding only harder, as for me.

Answer 1

Using GHC 7.4's constraint kinds you could have something like

type EfficientSetLike a = (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a)

You can (with appropriate extensions) get constraints like this in earlier versions of GHC

class (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a) => EfficientSetLike a 
instance (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a) => EfficientSetLike a 

But, the new style type declaration is much nicer.

I'm not exactly sure what you are looking for, but it sounds like you just want easier to write/understand constraint signatures, in which case this will work.