#85: New (0.6.0) qualified superclass constraint on `MonadTrans` breaks Agda

concrete functor and monad transformers

#85New (0.6.0) qualified superclass constraint on `MonadTrans` breaks Agda

transformers-0.6 came with an extra constraint on MonadTrans:

class (forall m. Monad m => Monad (t m)) => MonadTrans t where

This breaks compilation of Agda, see: https://github.com/agda/agda/issues/5659#issuecomment-1027367167 In our case t = TCMT is only a monad if m is a MonadIO. This is because the fail method (which still exists in some GHC versions we support---we support GHC 8.0 - 9.2) is implemented using IO.

To help me understand what this new constraint's purpose is: Why can some t satisfying only (forall m. MonadIO m => Monad (t m)) not be a monad transformer? It can still provide access to the monad m, can't it? Why is it a hinderance that m has additional services, like IO access?

Andreas Abel Tue Feb 1 23:55:41 UTC 2022
This regression has been introduced by the "fix" of (non-)issue https://hub.darcs.net/ross/transformers/issue/71.

Andreas Abel Wed Feb 2 10:30:09 UTC 2022

Here is a MWE:

{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module CrashOnFail where

import           Control.Monad.IO.Class
import           Control.Monad.Trans.Class
import           Control.Monad.Fail         (MonadFail)
import qualified Control.Monad.Fail         as Fail
import           System.Exit                (die)

-- A monad transformer that implements &#39;fail&#39; as &#39;die&#39;.

newtype CrashOnFailT m a = CrashOnFailT (m a)
  deriving (Functor, Applicative)

instance MonadIO m => MonadFail (CrashOnFailT m) where
  fail = CrashOnFailT . liftIO . die

instance MonadIO m => Monad (CrashOnFailT m) where
  CrashOnFailT ma >>= k = CrashOnFailT $ do
    a <- ma
    let CrashOnFailT mb = k a
    mb
  return = pure
#if  __GLASGOW_HASKELL__ < 808
  fail   = Fail.fail
#endif

-- This breaks with transformers-0.6 starting with GHC 8.6:

instance MonadTrans CrashOnFailT where
  lift = CrashOnFailT

Cabal file for completeness:

cabal-version:      >= 1.10
name:               MonadTrans-fail
version:            0.1.0.0
build-type:         Simple

library
  hs-source-dirs:   .
  default-language: Haskell2010
  exposed-modules:  CrashOnFail
  build-depends:    base
                  , transformers == 0.6.*

Ross Paterson Wed Feb 2 11:18:20 UTC 2022
I think you said somewhere (that I can't find now) that limiting the constraint to GHC >= 8.8 (instead of 8.6) would fix things for you. Is that still true? (In the above example the Monad (CrashOnFailT m) instance could be defined to only require (Monad m) for GHC >= 8.8.)

Ross Paterson Wed Feb 2 12:19:18 UTC 2022

So the suggestion for Agda.TypeChecking.Monad.Base is

returnTCMT :: Monad m => a -> TCMT m a
returnTCMT = \x -> TCM $ \_ _ -> return x
{-# INLINE returnTCMT #-}

bindTCMT :: Monad m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e
{-# INLINE bindTCMT #-}

thenTCMT :: Monad m => TCMT m a -> TCMT m b -> TCMT m b
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
{-# INLINE thenTCMT #-}

instance Monad m => Functor (TCMT m) where
  fmap = fmapTCMT

fmapTCMT :: Monad m => (a -> b) -> TCMT m a -> TCMT m b
fmapTCMT = \f (TCM m) -> TCM $ \r e -> fmap f (m r e)
{-# INLINE fmapTCMT #-}

#if __GLASGOW_HASKELL__ < 808
instance MonadIO m => Applicative (TCMT m) where
#else
instance Monad m => Applicative (TCMT m) where
#endif
  pure  = returnTCMT
  (<*>) = apTCMT

#if __GLASGOW_HASKELL__ < 808
apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
#else
apTCMT :: Monad m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
#endif
apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
{-# INLINE apTCMT #-}

instance MonadTrans TCMT where
    lift m = TCM $ \_ _ -> m

-- We want a special monad implementation of fail.
#if __GLASGOW_HASKELL__ < 808
instance MonadIO m => Monad (TCMT m) where
#else
instance Monad m => Monad (TCMT m) where
#endif
    return = pure
    (>>=)  = bindTCMT
    (>>)   = (*>)
#if __GLASGOW_HASKELL__ < 808
    fail   = Fail.fail
#endif

instance MonadIO m => Fail.MonadFail (TCMT m) where
  fail = internalError

Ross Paterson Wed Feb 2 14:02:43 UTC 2022
The constraint is now limited to GHC >= 8.8. It seems unreasonable to require a polymorphic instance of Monad for earlier versions, when the class included the fail method.
Ross Paterson Wed Feb 2 18:33:03 UTC 2022
- status set to closed
It seems this fixes the Agda issue.

Andreas Abel Wed Nov 23 21:30:34 UTC 2022

@phadej remarks in https://github.com/agda/agda/issues/5659#issuecomment-1325301101 that GHC 8.6 has MonadFailDesugaring, so the problem could have been solved without changing anything in transformer-0.6:

{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module CrashOnFail where

import           Control.Monad.IO.Class
import           Control.Monad.Trans.Class
import           Control.Monad.Fail         (MonadFail)
import qualified Control.Monad.Fail         as Fail
import           System.Exit                (die)

-- A monad transformer that implements &#39;fail&#39; as &#39;die&#39;.

newtype CrashOnFailT m a = CrashOnFailT (m a)
  deriving (Functor, Applicative)

instance MonadIO m => MonadFail (CrashOnFailT m) where
  fail = CrashOnFailT . liftIO . die

#if __GLASGOW_HASKELL__ < 806
instance MonadIO m => Monad (CrashOnFailT m) where
#else
instance Monad m => Monad (CrashOnFailT m) where
#endif
  CrashOnFailT ma >>= k = CrashOnFailT $ do
    a <- ma
    let CrashOnFailT mb = k a
    mb
  return = pure
#if  __GLASGOW_HASKELL__ < 806
  fail   = Fail.fail
#endif

instance MonadTrans CrashOnFailT where
  lift = CrashOnFailT

This works with "all" GHCs and transformers-0.6.0.0/1/2.

hub.darcs.net :: ross -> transformers -> issue

#85New (0.6.0) qualified superclass constraint on `MonadTrans` breaks Agda