Skip to content

Commit

Permalink
Fix #5659: port instance Monad (TCMT m) to transformers-0.6
Browse files Browse the repository at this point in the history
  • Loading branch information
andreasabel committed Mar 14, 2022
1 parent 4440d27 commit fdf39ab
Show file tree
Hide file tree
Showing 3 changed files with 25 additions and 4 deletions.
10 changes: 7 additions & 3 deletions Agda.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -240,11 +240,9 @@ library
, haskeline >= 0.7.2.3 && < 0.9
-- monad-control-1.0.1.0 is the first to contain liftThrough
, monad-control >= 1.0.1.0 && < 1.1
-- mtl-2.1 contains a severe bug.
--
-- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
-- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+)
, mtl >= 2.2.1 && < 2.3
, mtl >= 2.2.1 && < 2.4
, murmur-hash >= 0.1 && < 0.2
, parallel >= 3.2.2.0 && < 3.3
, pretty >= 1.1.3.3 && < 1.2
Expand All @@ -261,6 +259,12 @@ library
, uri-encode >= 1.5.0.4 && < 1.6
, zlib == 0.6.*

-- Andreas, 2022-02-02, issue #5659:
-- Build failure with transformers-0.6.0.{0,1,2} and GHC 8.6.
-- Transformers-0.6.0.3 might restored GHC 8.6 buildability.
if impl(ghc == 8.6.*)
build-depends: transformers < 0.6 || >= 0.6.0.3

-- Andreas, 2021-03-10:
-- All packages we depend upon should be mentioned in an unconditional
-- build-depends field, but additional restrictions on their
Expand Down
7 changes: 7 additions & 0 deletions src/full/Agda/TypeChecking/Monad/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4244,7 +4244,14 @@ 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
-- Andreas, 2022-02-02, issue #5659:
-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here
-- if we want @instance MonadTrans TCMT@.
instance Monad m => Monad (TCMT m) where
#endif
return = pure
(>>=) = bindTCMT
(>>) = (*>)
Expand Down
12 changes: 11 additions & 1 deletion src/full/Agda/TypeChecking/Monad/Base.hs-boot
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Monad.Base where

import Control.Monad.IO.Class (MonadIO)
Expand Down Expand Up @@ -28,9 +30,17 @@ newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }

instance Applicative m => Applicative (TCMT m)
instance Functor m => Functor (TCMT m)
instance MonadIO m => Monad (TCMT m)
instance MonadIO m => MonadIO (TCMT m)

#if __GLASGOW_HASKELL__ < 808
instance MonadIO m => Monad (TCMT m) where
#else
-- Andreas, 2022-02-02, issue #5659:
-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here
-- if we want @instance MonadTrans TCMT@.
instance Monad m => Monad (TCMT m) where
#endif

type TCM = TCMT IO

type ModuleToSource = Map TopLevelModuleName AbsolutePath
Expand Down

0 comments on commit fdf39ab

Please sign in to comment.