[Haskell-cafe] Re: Type parameters in type families

[Manuel M T Chakravarty]

Ryan Ingram:
> On 3/17/08, Hugo Pacheco <hpacheco at gmail.com> 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