| | -- 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