| 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