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

[Claus Reinke]

| Here is a variation to make this point clearer:
|
| {-# LANGUAGE NoMonomorphismRestriction #-}
| {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
|
| class Fun d where
|     type Memo d :: * -> *
|     abst :: (d -> a) -> Memo d a
|     appl :: Memo d a -> (d -> a)
|
| f = abst . appl
|
| -- 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'".

>I must be missing the point.

The point was in the part you didn't quote:

|In other words, I'd expect :browse output more like this:
|
|f :: forall a d. (Fun d, d~_d) => Memo d a -> Memo d a
|f' :: forall a d. (Fun d) => Memo d a -> Memo d a
|
|making the first signature obviously ambiguous, and the
|second signature simply valid.

Again, the validity of the second signature depends on
ScopedTypeVariables - without that, both f and f' should
get a signature similar to the first one (or some other notation
that implies that 'd' isn't freely quantified, but must match a
non-accessible '_d').

Claus