[Haskell-cafe] Strange type error with associated type synonyms

[Claus Reinke]

|Oh now i see what you mean:  consider
|        f' = abst . (id :: (d->a)->(d->a)) . appl
|which GHC understands to mean
|        f' = abst . (id :: forall d a. (d->a)->(d->a)) . appl
|
|GHC infers the type
|        f' :: (Fun d) => Memo d a -> Memo d a
|Now you are saying that GHC *could* have figured out that if it added the signature
|        f' :: forall d a. (Fun d) => Memo d a -> Memo d a
|thereby *changing* the scoping of d,a in the buried signature for 'id', doing so would not change 
whether f' was |typeable or not.  Well maybe, but that is way beyond what I have any current plans 
to do.

Indeed!-) I didn't mean to suggest this as a course of action, it was
just a way of representing the internal type inference intermediates
at source level. Another aspect I would not like about this approach is
that renamings of bound type variables would no longer be meaning-
preserving (because the signature would be interpreted in the context
of the source-code it belongs to) - not good.

But the core part of my suggestion (which this example was meant
to help explain) remains attractive, at least to me: somewhere during
type inference, GHC *does* unify the *apparently free* 'd' with an
internal type variable (lets call it 'd1, as in the type error message)
that has no explicit counterpart in source code or type signature,
so the inferred type should not be

        f' :: forall d. (Fun d) => Memo d a -> Memo d a -- (1)

but rather

        f' :: forall d. (Fun d,d~d1) => Memo d a -> Memo d a -- (2)

That way, the internal dependency would be made explicit in
the printed representation of the inferred type signature, and
the unknown 'd1' would appear explicitly in the inferred type,
not just in the error message (the explicit foralls are needed
here to make it clear that 'd1' and by implication, 'd', *cannot*
be freely generalized - 'd' is qualified by the equation with the
unknown 'd1').

To me, (2) makes more sense as an inferred type for f' than (1),
especially as it represents an obviously unusable type signature
(we don't know what 'd1' is, and we can't just unify it with anything),
whereas (1) suggests a useable type signature, but one that will fail
when used:

    Couldn't match expected type `Memo d1' against inferred
    type `Memo d'.

All I'm suggesting is that the type *printed* by GHCi does not
really represent the type *inferred* by GHCi (or else there should
not be any attempt to match the *free* 'd' against some unknown
'd1', as the error message says), and that there might be ways to 
make the discrepancy explicit, by printing the inferred type differently.

Claus