| 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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to