Ryan Ingram:
On 3/17/08, Hugo Pacheco <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
