Ryan Ingram:

On 3/17/08, Hugo Pacheco wrote:

...

On the other side, it fails to compile when this signature is explicit: fff :: forall d x. (FunctorF d) => d -> F d x -> F d x fff a = fmapF a id

Interestingly, this works when you also give a type signature to "id":

fff :: forall d x. (FunctorF d) => d -> F d x -> F d x fff a = fmapF a (id :: x -> x)

compiles for me (ghc6.8.2). There's probably a bug in the type checker; inference is working with no type signatures, but checking fails.

The type checker is alright. It is an issue that we need to explain better in the documentation, though. As a simple example consider, class C a where type F a :: * foo :: F a The only occurrence of 'a' here is as an argument of the type family F. However, as discussed in this thread, decomposition does not hold for the type-indicies of a type family. In other words, from F a ~ F b, we can *not* deduce a ~ b. You have got the same situation for the 'x' in type type of fff. BTW, the same applies if you code the example with FDs. class C a ca | a -> ca where foo :: ca which means, we have foo :: C a ca => ca Here 'a' only appears in the context and as 'a' appears on the lhs of the FD arrow, that leads to ambiguities. In summary, a type variable in a signature that appears *only* as part of type-indicies of type families leads to the same sort of ambiguities as a type variable that appears only in the context of a type signature. Manuel

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 wrote:

On 3/17/08, Hugo Pacheco 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)