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

[Simon Peyton-Jones]

| | -- f' :: forall d a. (Fun d) => Memo d a -> Memo d a
| | f' = abst . (id :: (d->a)->(d->a)) . appl
| |
| | There is a perfectly valid type signature for f', as given in
| | comment, but GHCi gives an incorrect one (the same as for f):
| |
| | *Main> :browse Main
| | class Fun d where
| |   abst :: (d -> a) -> Memo d a
| |   appl :: Memo d a -> d -> a
| | f :: (Fun d) => Memo d a -> Memo d a
| | f' :: (Fun d) => Memo d a -> Memo d a
|
| >I'm missing something here.  Those types are identical to the one given
| >in your type signature for f' above, save that the forall is suppressed
| >(because you are allowed to omit it, and GHC generally does when
| >printing types).
|
| Not with ScopedTypeVariables, though, where explicit foralls have
| been given an additional significance. Uncommenting the f' signature works, while
| dropping the
| 'forall d a' from it fails with
| the usual match failure due to ambiguity "Couldn't match expected
| type `Memo d1' against inferred type `Memo d'".

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.

S