3 Nov 12:07 2012

## forall disappear from type signature

<oleg <at> okmij.org>

2012-11-03 11:07:36 GMT

2012-11-03 11:07:36 GMT

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(Continue reading)