Pattern matching inside closed type families

Question

I'm incompetently trying to play with the new closed type family feature of GHC 7.8 and I would like to find a nice way to branch on type level constructs.

I have something like

data (:::) :: Symbol -> * -> * where

data Result = Pre | Post | Match

type family Cmp a b :: Result where
    Cmp (s ::: t) (s ::: t) = Match
    Cmp (s1 ::: t1) (s2 ::: t2) = ???

where I would like to return different types depending on the result of CmpSymbol in GHC.TypeLits. It feels like something like

Cmp (s1 ::: t1) (s2 ::: t2) = (CmpSymbol s1 s2 ~ LT) => Pre
Cmp (s1 ::: t1) (s2 ::: t2) = (CmpSymbol s1 s2 ~ GT) => Post

should work, but it does not. Interestingly it's not a syntax error but instead a complaint that it is ill kinded.

I can somehow get it to work by using undecidable instances and a helper function:

type family Cmp a b :: Result where
    Cmp (s ::: t) (s ::: t) = Match
    Cmp (s1 ::: t1) (s2 ::: t2) = Fun (CmpSymbol s1 s2)

type family Fun r :: Result where
    Fun LT = Pre
    Fun GT = Post

But this feels rather clunky, surely there is a nicer way? Also ghci says something like :kind! Cmp ("a" ::: Int) ("a" ::: String) has type Fun 'EQ even though Fun is closed. Why is that? I also can't see an easy way to work with ordinary classes here? What if the definition of Fun was something like

class Fun2 o r
instance Fun2 LT Pre
instance Fun2 GT Post

Is there any way to talk to type classes in a nice way or am I restricted to just using other type families like Fun?

Answer 1

That really is the only way, although I like to define some reusable type functions (== and If), in your case it would become If (CmpSymbol s1 s2 == LT) Pre Post.

Unfortunately, there is no way to get a type function of kind LT -> Pre from a class like Fun2.

Your example has kind Fun EQ because CmpSymbol "a" "a" is EQ and you pass this to Fun. The reason it doesn't just give an error is type families are evaluated as late as possible - here you don't ask for the "value" of Fun EQ so it isn't necessary to evaluate it yet.