[Haskell-cafe] Functional dependency failure

[Bertram Felgenhauer]

Alexander Pakhomov wrote:
> I have following code:
> 
> import Control.Monad.Reader
> import Control.Monad.ST
> import qualified Data.Vector.Mutable as MV
> import qualified Data.Vector as V
> 
> type ReadVecMonad s = ReaderT (MV.MVector s Int) (ST s)
> 
> freezeV :: ReadVecMonad s (V.Vector Int)
> freezeV = ask >>= lift V.freeze

You are asking to lift a function of type

    MV.MVector s Int -> ST s (V.Vector Int)

to another one of type

    MV.MVector s Int -> ReaderT (MV.MVector s Int) (ST s) (V.Vector Int)

However, `lift` works on monad actions. This works:

    freezeV :: ReadVecMonad s (V.Vector Int)
    freezeV = ask >>= lift . V.freeze

> Trying to compile this I have "Couldn't match type ... When using functional dependencies to combine" error
> following with kind mismatch and type with literaly the same type mismatch.

Ghc's error message is wonderfully convoluted. Let's try to follow.

We know that freezeV :: ReadVecMonad s (V.Vector Int) and
(>>=) :: Monad m => m a -> (a -> m b) -> m b, so that

  ask :: ReadVecMonad s r
  lift V.freeze :: r -> ReadVecMonad s (V.Vector Int)

ghc infers the following type for `lift V.freeze`:

  lift V.freeze
    :: (Control.Monad.Primitive.PrimMonad m, MonadTrans t) =>
     t ((->) (V.MVector (Control.Monad.Primitive.PrimState m) a))
       (m (V.Vector a))

To unify the two types for `lift V.freeze`, we let

  t = (->)
  r = (->) (V.MVector (Control.Monad.Primitive.PrimState m) a)
  m = ReadVecMonad s
  a = Int

Therefore, we must have

  ask :: ReadVecMonad s
    ((->) (V.MVector (Control.Monad.Primitive.PrimState (ReadVecMonad s)) Int))
  ask :: ReaderT (MV.MVector s Int) (ST s)
    ((->) (V.MVector (Control.Monad.Primitive.PrimState (ReadVecMonad s)) Int))

We also know that ask :: MonadReader m r => m r. In our case,
m = ReaderT (MV.MVector s Int) (ST s). From the instance
MonadReader r (ReaderT r m) and the functional dependency m -> r, we
conclude that

  r = MV.MVector s Int.

This, of course, is in contradiction with the already established

  r = (->) (V.MVector (Control.Monad.Primitive.PrimState (ReadVecMonad s)) Int)

Phew.

The kind errors later on arise from the fact that we have replaced
t :: (* -> *) -> * -> * (t is supposed to be a monad transformer)
by (->) :: * -> * -> *, and r :: * by something of kind * -> *.

Newer ghc versions seem to arrive at r = MV.MVector s Int before
r = (->) (V.MVector (Control.Monad.Primitive.PrimState (ReadVecMonad s)) Int)
and do not mention functional dependencies as a result.

Hope that helps,

Bertram

> There's full error message:
> 
> STRead.hs:9:11:
>     Couldn't match type `V.MVector s Int'
>                   with `(->)
>                           (V.MVector
>                              (Control.Monad.Primitive.PrimState
>                                 (ReaderT (V.MVector s Int) (ST s)))
>                              Int)'
>     When using functional dependencies to combine
>       MonadReader r (ReaderT r m),
>         arising from the dependency `m -> r'
>         in the instance declaration in `Control.Monad.Reader.Class'
>       MonadReader
>         ((->)
>            (V.MVector
>               (Control.Monad.Primitive.PrimState
>                  (ReaderT (V.MVector s Int) (ST s)))
>               Int))
>         (ReaderT (V.MVector s Int) (ST s)),
>         arising from a use of `ask' at STRead.hs:9:11-13
>     In the first argument of `(>>=)', namely `ask'
>     In the expression: ask >>= lift V.freeze
> 
> 
> STRead.hs:9:19:
>     Couldn't match kind `* -> *' with `*'
>     Expected type: (->)
>                      (V.MVector
>                         (Control.Monad.Primitive.PrimState
>                            (ReaderT (V.MVector s Int) (ST s)))
>                         Int)
>                    -> ReaderT (V.MVector s Int) (ST s) (V.Vector Int)
>       Actual type: (->)
>                      (V.MVector
>                         (Control.Monad.Primitive.PrimState
>                            (ReaderT (V.MVector s Int) (ST s)))
>                         Int)
>                    -> ReaderT (V.MVector s Int) (ST s) (V.Vector Int)
>     Kind incompatibility when matching types:
>       (->)
>         (V.MVector
>            (Control.Monad.Primitive.PrimState
>               (ReaderT (V.MVector s Int) (ST s)))
>            Int) :: * -> *
>       (->)
>         (V.MVector
>            (Control.Monad.Primitive.PrimState
>               (ReaderT (V.MVector s Int) (ST s)))
>            Int) :: *
>     In the return type of a call of `lift'
>     In the second argument of `(>>=)', namely `lift V.freeze'
> 
> STRead.hs:9:24:
>     Couldn't match kind `*' with `* -> *'
>     Expected type: V.MVector
>                      (Control.Monad.Primitive.PrimState
>                         (ReaderT (V.MVector s Int) (ST s)))
>                      Int
>                    -> ReaderT (V.MVector s Int) (ST s) (V.Vector Int)
>       Actual type: V.MVector
>                      (Control.Monad.Primitive.PrimState
>                         (ReaderT (V.MVector s Int) (ST s)))
>                      Int
>                    -> ReaderT (V.MVector s Int) (ST s) (V.Vector Int)
>     Kind incompatibility when matching types:
>       (->)
>         (V.MVector
>            (Control.Monad.Primitive.PrimState
>               (ReaderT (V.MVector s Int) (ST s)))
>            Int) :: *
>       (->)
>         (V.MVector
>            (Control.Monad.Primitive.PrimState
>               (ReaderT (V.MVector s Int) (ST s)))
>            Int) :: * -> *
>     In the first argument of `lift', namely `V.freeze'
>     In the second argument of `(>>=)', namely `lift V.freeze'