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.