Scoping for temporary type variables

Question

I have a large number of in place vector functions of the type

f :: (M.MVector v r, PrimMonad m) => 
     v (PrimState m) r -> v (PrimState m) r -> m ()

These functions mostly work in-place, so it is convenient to have their argument be a mutable vector so that I can compose, iterate, etc. However, at the top level, I only want to work with immutable "Haskell"/pure vectors.

Here is an example of the problem:

{-# LANGUAGE TypeFamilies, 
             ScopedTypeVariables, 
             MultiParamTypeClasses, 
             FlexibleInstances #-}

import Data.Vector.Generic as V hiding (eq)
import Data.Vector.Generic.Mutable as M
import Control.Monad.ST
import Control.Monad.Primitive

f :: (M.MVector v r, PrimMonad m) => 
     v (PrimState m) r -> v (PrimState m) r -> m ()
f vIn vOut = do val <- M.read vIn 0
                M.write vOut 0 val

applyFunc :: (M.MVector v r, PrimMonad m, V.Vector v' r, v ~ Mutable v') => 
             (v (PrimState m) r -> v (PrimState m) r -> m ()) -> v' r -> v' r
applyFunc g x = runST $ do
                    y <- V.thaw x
                    g y y -- LINE 1
                    V.unsafeFreeze y

topLevelFun :: (V.Vector v r) => r -> v r
topLevelFun a =
    let x = V.replicate 10 a
    in applyFunc f x -- LINE 2

The code as written results in an error on LINE 1:

Could not deduce (m ~ ST s)
   Expected type: ST s ()
   Actual type: m ()
   in the return type of g, LINE 1

Commenting out LINE 1 results in the error on LINE 2:

Ambiguous type variable `m0' in the constraint:
    (PrimMonad m0) arising from a use of `applyFun'

I've tried a variety of explicit typing (using ScopedTypeVariables, explicit foralls, etc) but haven't found a way to fix the first error. For the LINE 1 error, it seems that m should simply be inferred to be ST s since I'm in a runST.

For the LINE 2 error (with LINE 1 commented out), the only thing I've come up with that works is

class Fake m v where
    kindSig :: m a -> v b c

instance Fake m v

topLevelFun :: forall m v v' r . (V.Vector v' r, M.MVector v r, PrimMonad m, Fake m v, v ~ Mutable v') => r -> v' r
topLevelFun a =
    let x = V.replicate 10 a
    in applyFunc (f::Transform m v r)  x -- LINE 2

which is obviously unsatisfactory: I have to create a fake class, with an even more pointless method whose only job is to demonstrate the kinds of the class arguments. Then I create a generic instance for everything so that I can have m in scope in topLevelFun, so that I can add a constraint and cast f. There has GOT to be a better way.

I could be doing a wide variety of things wrong here, so any suggestions would be helpful.

Answer 1

Does the following type for applyFunc work for you?

applyFunc :: (Vector v a) => 
  (forall s. Mutable v s a -> Mutable v s a -> ST s ()) 
  -> v a -> v a

That should compile with out problem so long as you have the Rank2Types extension, which you need because you work with a function that has to work on all ST monads. The reason for this is the type of runST is (forall s. ST s a) -> a, so the body of the code after runST needs to work for all s, hence g needs to work for all s.

(You could instead take a function that work with all PrimMonads but there are strictly fewer of those).

GHC can not infer higher rank types. There are very good reasons to not infer RankNTypes (it is undecidable), and although Rank2 is in theory inferable, the GHC people decided for the rule "infer if and only if the principle type is a Hindley-Milner type" which for people like me is very easy to reason about, and makes the compiler writers job not so hard.

In the comments you ask about taking a tuple. Tuples with polymorphic types require ImpredicativeTypes and can be done like

applyFuncInt :: (Vector v a) => 
   ((forall s. Mutable v s a -> Mutable v s a -> ST s ()),Int)
   -> v a -> v a
applyFuncInt (g,_) x = runST $ do
                            y <- V.thaw x
                            g y y
                            V.unsafeFreeze y

although, usually it would be better to simply pass the number as a separate argument.