Can the type of this function be declared in standard Haskell

Question

The following program compiles under GHC 8.0.2 with no language extensions, and produces the expected two lines of output.

However, it does not compile if the (non-top-level) type declaration for the value write' is removed.

Also, I cannot find any (top-level) type declaration for the function write.

I find this rather odd. If this is acceptable standard Haskell, surely it should be possible to create a type declaration for the function write.

So my question is: is there such a type declaration?

import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)
import Control.Monad.Writer (MonadTrans, Writer, lift, runWriter, tell, when)
import ListT (ListT, toList) -- Volkov's list-t package

logging = True

write x = when logging write' where
    write' :: MonadTrans m => m (Writer [String]) ()
    write' = lift $ tell [x]

f :: ListT (Writer [String]) String
f = do
    write "Hello from f"
    return "ABC"

g :: MaybeT (Writer [String]) Int
g = do
    write "Hello from g"
    return 123

main :: IO ()
main = do
    print $ runWriter $ toList f
    print $ runWriter $ runMaybeT g

Answer 1

Using GHCi (remember to put this into a separate file and load it on GHCi's command line lest you get confused by GHCi's altered typing rules):

> :t write
write :: (Applicative (m (Writer [String])), MonadTrans m) => 
         String -> m (Writer [String]) ()

Why? Well,

write' :: MonadTrans m => m (Writer [String]) ()
when :: Applicative f => Bool -> f () -> f ()
when logging :: Applicative f => f () -> f ()

so, when logging write' must unify write''s m (Writer [String]) with when loggings's f, causing the combined constraint (Applicative (m (Writer [String])), MonadTrans m). But wait, let's remove the type signatures and see what the most general type is:

-- equivalent but slightly easier to talk about
write = when logging . lift . tell . (:[])

(:[]) :: a -> [a]
tell :: MonadWriter w m -> w -> m ()
lift :: (Monad m, MonadTrans t) => m a -> t m a
tell . (:[]) :: MonadWriter [a] m => a -> m ()
lift . tell . (:[]) :: (MonadWriter [a] m, MonadTrans t) => a -> t m ()
when logging . lift . tell . (:[]) = write
  :: (Applicative (t m), MonadWriter [a] m, MonadTrans t) => a -> t m ()
-- GHCi agrees

Per se, there's nothing wrong with this type. However, standard Haskell does not allow this. In standard Haskell, a constraint must be of the form C v or C (v t1 t2 ...) where v is a type variable. In the compiling case, this holds: the Applicative constraint has the type variable m on the outside, and the MonadTrans is just m. This is true in the non-compiling version, too, but we also have the constraint MonadWriter ([] a) m. [] is no type variable, so the type here is rejected. This constraint arises in the compiling version, too, but the type signatures nail the variables down to produce MonadWriter [String] (Writer [String]), which is immediately satisfied and does not need to appear in the context of write.

The restriction is lifted by enabling FlexibleContexts (preferably via a {-# LANGUAGE FlexibleContexts #-} pragma, but also maybe by -XFlexibleContexts). It originally existed to prevent things such as the following:

class C a where c :: a -> a
-- no instance C Int

foo :: C Int => Int
foo = c (5 :: Int)
-- with NoFlexibleContexts: foo's definition is in error
-- with FlexibleContexts: foo is fine; all usages of foo are in error for
-- not providing C Int. This might obscure the source of the problem.

-- slightly more insiduous
data Odd a = Odd a
-- no Eq (Odd a)

oddly (Odd 0) (Odd 0) = False
oddly l r = l == r
-- oddly :: (Num a, Eq (Odd a), Eq a) => Odd a -> Odd a -> Bool
-- Now the weird type is inferred! With FlexibleContexts,
-- the weird constraint can propagate quite far, causing errors in distant
-- places. This is confusing. NoFlexibleContexts places oddly in the spotlight.

But it happens to get in the way a lot when you have MultiParamTypeClasses on.