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

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