Do GADTs break equational reasoning in Haskell

Question

I have the following interpreter using ProgramT from the operational package

{-# LANGUAGE GADTs #-}
import Control.Monad ((<=<))
import Control.Monad.Operational

data Motor' a where
  --Define GADT

serialNewportT :: (Monad m, MonadIO m) => ProgramT Motor' m a -> m a
serialNewportT = eval <=< viewT
  where
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v
    eval (Return x) = return x
    eval (x :>>= k) = f x >>= serialNewportT  . k

f :: (Monad m, MonadIO m) => Motor' a -> m a
f = undefined -- excluded for brevity

The code, as it stands, currently type checks just fine. However, I want to be able to switch out how the interpreter handles different motors, so I want to make f a parameter, instead of having it hard coded in. I've tried to make this switch with the following code

{-# LANGUAGE GADTs #-}
import Control.Monad ((<=<))
import Control.Monad.Operational

data Motor' a where
  --Define GADT

serialNewportT :: (Monad m, MonadIO m) => (Motor' a -> m a) -> ProgramT Motor' m a -> m a
serialNewportT f = eval <=< viewT
  where
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v
    eval (Return x) = return x
    eval (x :>>= k) = f x >>= serialNewportT f . k

However, this code fails with an error message

Couldn't match type ‘b’ with ‘c’
   ‘b’ is a rigid type variable bound by
       a pattern with constructor
         :>>= :: forall (instr :: * -> *) (m :: * -> *) a b.
                 instr b -> (b -> ProgramT instr m a) -> ProgramViewT instr m a,
       in an equation for ‘eval’
   ‘c’ is a rigid type variable bound by
       the type signature for
         serialNewportT :: (Monad m, MonadIO m) =>
                           (Motor' c -> m c) -> ProgramT Motor' m a -> m a
 Expected type: Motor' c
   Actual type: Motor' b

Since I'm just replacing the global name with a local one of the same type, I would have thought that it should have worked without a hitch. How can I get the types to unify with f as a parameter?

Answer 1

You have not correctly translated the type of f. In the original code, the type of f is forall a . (..) => Motor' a -> m a. It could be instantiated with a type Motor' a for any a, but in the non-working code you state that it's type is precisely the same a as in ProgramT Motor' m a, whereas in the function body you call f on a Motor' b for some other (existentially quantifed) type b.

You just need a higher rank type:

serialNewportT :: (Monad m, MonadIO m) => (forall x . Motor' x -> m x) -> ProgramT Motor' m a -> m a