But by doing so I am changing type equality to the same as having "type family F a :: * -> *"

F' a x ~ F' b y <=> F' a ~ F' b /\ x ~ y (equality for ADTs)

 and I would like this "decomposition rule not to apply" so.

Thanks though,
hugo

On Tue, Mar 18, 2008 at 1:12 AM, Ryan Ingram <ryani.spam@gmail.com> wrote:
On 3/17/08, Hugo Pacheco <hpacheco@gmail.com> wrote:
> type family G a :: * -> *
> type instance G Int = Either () -- you forgot this line
>
> instance Functor (G Int) where
>    fmap f (Left ()) = Left ()
>    fmap f (Right x) = Right (f x)

One thing that you don't seem to be clear about is that there is
something slightly magic going on in this Functor definition; you are
not declaring Functor (G Int) but rather Functor (whatever (G Int)
turns into).  This is using a GHC extension "TypeSynonymInstances".
The extension allows you to use type synonyms when declaring
instances, but only if they are fully applied, and the compiler is
simply applying the substitution for you.

That is to say, this code is no different than the following:

type family G a :: * -> *
type instance G Int = Either ()
instance Functor (Either ()) where
   fmap f (Left ()) = Left ()
   fmap f (Right x) = Right (f x)

Once you declare a more complicated type function, such as
  type family F a x :: *
this extension can no longer come into play.

You can get around this restriction with a newtype:

type family F a x :: *
type instance F Int x = Either () x

newtype F' a b = F' (F a b)

instance Functor (F' Int) where
  fmap f (F' (Left ())) = F' (Left ())
  fmap f (F' (Right x)) = F' (Right $ f x)