Haskell: Counter-intuitive type checking going on

Question

So I have these type:

newtype StateT s m a = StateT {runStateT :: s -> m (a, s)}

data MTa a = FailTa Exception
        | DoneTa {unpackDoneTa :: (a, O)}
        deriving Show

type O = String
type Exception = String
type State = Int

I made (State s m) an instance of the Functor, Applicative, and Monad classes like so:

instance (Monad m) => Functor (StateT s m) where
    fmap f t = StateT $ \is -> do
                    ~(a, s) <- runStateT t is
                    return (f a, s)

instance (Monad m) => Applicative (StateT s m) where
    pure = return
    StateT f <*> StateT t = StateT $ \is -> do
        ~(ta, ts) <- t is
        ~(fa, fs) <- f ts
        return (fa ta, fs)

instance (Monad m) => Monad (StateT s m) where
    return a = StateT $ \s -> return (a, s)
    StateT m1 >>= k = StateT $ \s -> do
        ~(a, s1) <- m1 s
        let StateT m2 = k a
        m2 s1

I also made MTa an instance of the Functor, Applicative, and Monad classes:

instance Functor MTa where
    _ `fmap` (FailTa e) = FailTa e
    f `fmap` (DoneTa (a, o)) = DoneTa (f a, o)

instance Applicative MTa where
    pure = return
    _ <*> (FailTa e) = FailTa e
    FailTa e <*> _ = FailTa e
    DoneTa (f, x) <*> DoneTa (a, y) = DoneTa (f a, y ++ x)

instance Monad MTa where
    return a = DoneTa (a, "")
    m >>= f = case m of
        FailTa e -> FailTa e
        DoneTa (a, x) -> case (f a) of
            FailTa e1 -> FailTa e1
            DoneTa (b, y) -> DoneTa (b, x ++ y)

I then have this function:

incTaState :: StateT State MTa ()
incTaState = StateT $ \s -> return ((), s+1)

Am I right to think that return ((), s+1) will evaluate to DoneTa (((), s+1), ""). If so, doesn't that mean that its type is MTa ((), State). Why does incTaState typecheck to StateT State MTa ()? When I run this: :t DoneTa ((), "") in a console, it evaluates to DoneTa ((), "") :: MTa (). Am I not interpreting the return part of incTaState correctly?

The question can almost be summarized like so: if Done ((), "") typechecks to MTa (), how is it that incTaState typechecks to StateT State MTa ()? Doesn't DoneTa (((), s+1), ""), the resolution of return ((), s+1), typecheck to MTa (((), State), O) making incTaState a type of StateT State MTa ((), State) not what is specified?

Please fell free to be verbose (-vvv).

Your consideration is much appreciated. Peace.

Below is removed as I made a mistake by entering a 3-tuple. Thanks @HTNW.

I suspect I'm not because when I run :t (StateT $ \s -> DoneTa (((), s+1, ""))) I get the following error:

• Couldn't match expected type ‘((a, b), O)’
                  with actual type ‘((), b, [Char])’
• In the first argument of ‘DoneTa’, namely ‘(((), s + 1, ""))’
  In the expression: DoneTa (((), s + 1, ""))
  In the second argument of ‘($)’, namely
    ‘\ s -> DoneTa (((), s + 1, ""))’
• Relevant bindings include s :: b (bound at <interactive>:1:12)

Answer 1

incTaState :: StateT State MTa ()
incTaState = StateT $ \s -> return ((), s+1)
\s -> ((), s+1)          :: State -> ((), State)
-- You were correct
\s -> return ((), s + 1) :: State -> MTa ((), State)
-- The type of that function matches up with StateT
-- We can set s = State, m = MTa, and a = ()
StateT s     m   a  = s     -> m   (a , s    )
StateT State MTa () = State -> MTa ((), State)
-- So:
StateT $ \s -> return ((), s+1) :: StateT State MTa ()
-- QED

When you run StateT $ \s -> DoneTa ((), s+1, ""), the issue is that DoneTa :: (a, String) -> MTa a, with a 2-tuple, but you are passing it ((), s + 1, "") :: ((), State, String), a 3-tuple. Add more nesting: StateT $ \s -> DoneTa (((), s + 1), "") (where (((), s + 1), "") :: (((), State), String), a 2-tuple with a 2-tuple inside it).