Using a monadic rank-2 type

Question

Here's the code: ``` {-# LANGUAGE RankNTypes, FlexibleContexts, ScopedTypeVariables #-} module Foo where import Data.Vector.Generic.Mutable as M import Data.Vector.Generic as V import Control.Monad.ST import Control.Monad.Primitive import Control.Monad data DimFun v s r = DimFun {dim::Int, func :: v (PrimState s) r -> s ()} runFun :: (Vector v r) => (forall s . (PrimMonad s) => DimFun (Mutable v) s r) -> v r -> v r runFun t x = runST $ do y <- thaw x evalFun t y unsafeFreeze y evalFun :: (PrimMonad s, MVector v r) => DimFun v s r -> v (PrimState s) r -> s () evalFun (DimFun dim f) y | dim == M.length y = f y fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r) fm = error "" f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r) f = liftM runFun $ (fm :: forall s . (PrimMonad s) => m (DimFun (Mutable v) s r)) ``` This results in errors: ``` Couldn't match type ‘DimFun (Mutable v) s0 r’ with ‘forall (s :: * -> *). PrimMonad s => DimFun (Mutable v) s r’ Expect…

Accepted Answer

One solution is to move the `PrimMonad` constraint inside the `DimFun` datatype.

```
data DimFun v r = DimFun 
   { dim  :: Int
   , func :: forall s . PrimMonad s => v (PrimState s) r -> s ()
   }
```

The rest of your code compiles as-is, removing the `s` parameter from `DimFun`:

```
runFun :: Vector v r => DimFun (Mutable v) r -> v r -> v r
runFun = ...

evalFun :: (PrimMonad s, MVector v r) => DimFun v r -> v (PrimState s) r -> s () 
evalFun = ...

fm :: (MVector v r, Num r, Monad m) => m (DimFun v r)
fm = ...

f :: (Vector v r, Num r, Monad m) => m (v r -> v r)
f = liftM runFun fm
```

Moving the class constraint into the datatype may seem scary to you, but in reality, you already had the class constraint there anyways. `PrimState` is an associated type family of `PrimMonad`, so in order to produce or consume a `v (PrimState s) r`, you need the `PrimMonad` constraint.

If you want to avoid it nevertheless, you will have to change the type of something. To see why the function you have is illtyped, consider the following (which requires `ImpredictiveTypes`):

```
fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r)
fm = error ""

g :: (Vector v r, Monad m) 
  => m (forall s . PrimMonad s => DimFun (Mutable v) s r) -> m (v r -> v r)
g = liftM runFun 
```

It should be cleared why `g fm` is illtyped: `g` expects something where the `forall s . PrimMonad s =>` is inside the `m`, which is not the case for `fm`. You will have to write a function of type:

```
fm' :: (MVector v r, Monad m, Num r) => m (forall s . PrimMonad s => DimFun v s r)
fm' = error ""

f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r)
f = g fm'
```

Using a monadic rank-2 type

Solution

Problem

Related problems