RankNTypes does not match return type

Question

Using RankNTypes , I define a type that is independent of the type variable. Is this the right way to get around the case below?

I need to define several functions that will be used inside ST s , which, of course, does not depend on s . However, this leads to the fact that the Exp statement with two Int applied to it does not result in Block . Why?

Here is the reproducer:

 import Control.Monad.ST import Data.Vector.Unboxed (Vector) import qualified Data.Vector.Unboxed as U import Data.Vector.Unboxed.Mutable (STVector) import qualified Data.Vector.Unboxed.Mutable as UM type Exp = Int -> Int -> Block type Block = forall s . STVector s Int -> ST s Int block :: [Block] -> Block block [] _ = return 0 -- mapM doesn't work, either - ok, I kinda see why block (e:es) a = do x <- ea xs <- block es a return $ x+xs copy :: Exp copy ija = do aj <- a `UM.unsafeRead` j UM.unsafeWrite ai aj return 1 f :: Block -> Vector Int -> Int f blk ua = runST $ U.thaw ua >>= blk g :: Block -> Int g blk = f blk $ U.fromListN 12 [1..] main = print . g $ block [copy 10 1] 

The error I get in the last line is:

 Couldn't match type `STVector s0 Int -> ST s0 Int' with `forall s. STVector s Int -> ST s Int' Expected type: Block Actual type: STVector s0 Int -> ST s0 Int In the return type of a call of `block' Probable cause: `block' is applied to too few arguments In the second argument of `($)', namely `block [copy 10 1]' In the expression: print . g $ block [copy 10 1] 

The difference between the expected and the actual type is the forall s. bit forall s. as far as I can judge.

Answer 1

Although I would have preferred @Oleg's solution to be published, I would like to share an alternative.

Replace

 main = print . g $ block [copy 10 1] 

from

 main = print (g (block [copy 10 1])) 

Reason: improvised types make it difficult for the compiler to guess the types (.) And ($) above.

Another option would be to annotate (.) And ($) with your instantiated type - this would be rather cumbersome.

Answer 2

Using newtype for Block will support s existential. Otherwise, it leaks out

---

With original definition:

 type Block = forall s . STVector s Int -> ST s Int type Exp = Int -> Int -> Block 

You can simplify the failure example ( main ):

 g . block 

You would like it to be as follows:

 g . block :: [Block] -> Int 

But since the written types of components are:

 block :: forall s. [forall s0. STVector s0 Int -> ST s0 Int] -> (STVector s Int -> ST s Int) g :: (forall s1. STVector s1 Int -> ST s1 Int) -> Int 

Then, when compiled with (.) , The GHC saves s general:

 g . block :: forall s . [forall s0. STVector s0 Int -> ST s0 Int] -> Int 

and trying to combine:

 forall s1. STVector s1 Int -> ST s1 Int -- and (STVector s Int -> ST s Int) 

---

With newtype everything works fine (and ImpredicativeTypes not needed):

 {-# LANGUAGE RankNTypes #-} import Control.Monad.ST import Data.Vector.Unboxed (Vector) import qualified Data.Vector.Unboxed as U import Data.Vector.Unboxed.Mutable (STVector) import qualified Data.Vector.Unboxed.Mutable as UM type Exp = Int -> Int -> Block newtype Block = Block { unBlock :: forall s . STVector s Int -> ST s Int } block :: [Block] -> Block block [] = Block $ \_ -> return 0 -- mapM doesn't work, either - ok, I kinda see why block (e:es) = Block $ \a -> do x <- unBlock ea xs <- unBlock (block es) a return $ x + xs copy :: Exp copy ij = Block $ \a -> do aj <- a `UM.unsafeRead` j UM.unsafeWrite ai aj return 1 f :: Block -> Vector Int -> Int f (Block blk) ua = runST $ U.thaw ua >>= blk g :: Block -> Int g blk = f blk $ U.fromListN 12 [1..] main = print . g $ block [copy 10 1]