[Haskell-cafe] forall disappear from type signature

[oleg at okmij.org]

Takayuki Muranushi wrote:
> Today, I encountered a strange trouble with higher-rank polymorphism. It
> was finally solved by nominal typing. Was it a bug in type checker? lack of
> power in type inference? 

> runDB :: Lens NetworkState RIB
> runDB = lens (f::NetworkState -> RIB) (\x s -> s { _runDB = x })
>  where f :: NetworkState -> RIB

As it becomes apparent (eventually), RIB is a polymorhic type,
something like

type RIB = forall a. DB.DBMT (Maybe Int) IO a0
		           -> IO (StM (DB.DBMT (Maybe Int) IO) a0)

The field _runDB has this polymorphic type. Hence the argument x 
in (\x s -> s { _runDB = x }) is supposed to have a polymorphic type.
But that can't be: absent a type signature, all arguments of a
function are monomorphic. One solution is to give lens explicit,
higher-ranked signature (with explicit forall, that is). A better
approach is to wrap polymorphic types like your did

> newtype RIB = RIB (RunInBase (DB.DBMT (Maybe Int) IO) IO)

The newtype RIB is monomorphic and hence first-class, it can be freely
passed around. In contrast, polymorphic values are not first-class,
in Haskell. There are many restrictions on their use. That is not a
bug in the type checker. You may call it lack of power in type
inference: in calculi with first-class polymorphism (such as System F
and System Fw), type inference is not decidable. Even type checking is
not decidable.