Closed type families don’t work as expected

Question

A couple of hours ago I built GHC HEAD to experiment with new shiny closed type families.

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}

type family C a b where
  C  a [a] = [a]
  C  a  a  = [a]

Now I try to put C to use:

class Combine a b where
  combine :: a -> b -> C a b

instance Combine a [a] where
  combine a b = a : b

instance Combine a a where
  combine a b = [a, b]

Which results in this error:

Couldn't match expected type ‛C a a’ with actual type ‛[a]’
...
In the expression: [a, b]
In an equation for ‛combine’: combine a b = [a, b]
In the instance declaration for ‛Combine a a’

It seems to me that the second equation is apart from the first one ([a] a can’t be simplified to a a, no matter what a), so why doesn’t it compile?

Answer 1

I looked through the mail archives a little bit. Unfortunately, it seems that a ~ b does not preclude the possibility that a ~ [b], because this kind of nonsense is accepted:

type family G = [G]

As a result, in instance Combine a a, when we call C a a to find out what the return type ought to be, no reduction is possible: because we don't know anything about a, we don't know yet whether to choose the C a a or C a [a] branch of the C type family, and we can't do any reduction yet.

There's more details in this mailing list thread, which has a great deal of followups (that seem to be hard to find from the previous link) in the next month's by-thread archive. The whole situation actually seems a bit weird to me, though I'm not sure what a better solution would be.