Remove redundant Data.Monoid imports

.travis.yml

@@ -17,7 +17,7 @@ sudo: required
 
 branches:
   only:
-    - imports
+    - monoid
     - master
     - future
     - maint-2.4

Agda.cabal

@@ -224,6 +224,7 @@ library
                 -- 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
                 , murmur-hash >= 0.1 && < 0.2
                 , pretty >= 1.1.3.3 && < 1.2

src/full/Agda/Auto/CaseSplit.hs

@@ -5,6 +5,7 @@ module Agda.Auto.CaseSplit where
 import Data.IORef
 import Data.Tuple (swap)
 import Data.List (elemIndex)
+-- Import of <> needed for 8.2.2, but redundant in 8.8.3
 import Data.Monoid ((<>), Sum(..))
 import qualified Data.Set    as Set
 import qualified Data.IntMap as IntMap

src/full/Agda/Auto/Typecheck.hs

@@ -2,7 +2,6 @@
 module Agda.Auto.Typecheck where
 
 import Data.IORef
-import Control.Monad (liftM)
 
 import Agda.Syntax.Common (Hiding (..))
 import Agda.Auto.NarrowingSearch

src/full/Agda/Compiler/CallCompiler.hs

@@ -8,7 +8,6 @@ module Agda.Compiler.CallCompiler where
 import qualified Control.Exception as E
 import Control.Monad.Trans
 
-import Data.List ( intercalate )
 import System.Exit
 import System.IO
 import System.Process

src/full/Agda/Compiler/JS/Syntax.hs

@@ -2,9 +2,7 @@
 
 module Agda.Compiler.JS.Syntax where
 
-import Data.Foldable (foldMap)
 import Data.Map (Map)
-import qualified Data.Map as Map
 
 import Data.Set (Set)
 import qualified Data.Set as Set

src/full/Agda/Compiler/Treeless/Subst.hs

@@ -6,7 +6,6 @@ module Agda.Compiler.Treeless.Subst where
 import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Maybe
-import Data.Monoid ( Monoid, mempty, mappend )
 import Data.Semigroup ( Semigroup, (<>), All(..), Any(..) )
 
 import Agda.Syntax.Treeless

src/full/Agda/Interaction/Base.hs

@@ -325,7 +325,7 @@ parseToReadsPrec p i s = case runIdentity . flip runStateT s . runExceptT $ pare
 -- | Demand an exact string.
 
 exact :: String -> Parse ()
-exact s = readsToParse (show s) $ fmap (\x -> ((),x)) . List.stripPrefix s . dropWhile (==' ')
+exact s = readsToParse (show s) $ fmap ((),) . List.stripPrefix s . dropWhile (==' ')
 
 readParse :: Read a => Parse a
 readParse = readsToParse "read failed" $ listToMaybe . reads

src/full/Agda/Interaction/Imports.hs

@@ -18,7 +18,6 @@ import qualified Data.List as List
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Maybe
-import Data.Monoid (mempty, mappend)
 import Data.Map (Map)
 import qualified Data.HashMap.Strict as HMap
 import Data.Text.Lazy (Text)

src/full/Agda/Main.hs

@@ -3,7 +3,6 @@
 -}
 module Agda.Main where
 
-import Control.Monad (void)
 import Control.Monad.State
 
 import Data.Maybe

src/full/Agda/Syntax/Abstract.hs

@@ -24,7 +24,6 @@ import qualified Data.Set as Set
 import Data.Set (Set)
 import Data.Void
 import Data.Data (Data)
-import Data.Monoid (mappend)
 
 import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)--, HoleContent'(..))
 import qualified Agda.Syntax.Concrete as C

src/full/Agda/Syntax/Concrete/Definitions.hs

@@ -45,7 +45,7 @@ module Agda.Syntax.Concrete.Definitions
 
 import Prelude hiding (null)
 
-import Control.Arrow ((***), first, second)
+import Control.Arrow (first, second)
 import Control.Monad.Except
 import Control.Monad.State
 

src/full/Agda/Syntax/Concrete/Operators.hs

@@ -20,7 +20,6 @@ module Agda.Syntax.Concrete.Operators
 
 import Control.Applicative ( Alternative((<|>)))
 import Control.Arrow (second)
-import Control.Monad
 import Control.Monad.Except (throwError)
 
 import Data.Either (partitionEithers)

src/full/Agda/Syntax/Concrete/Pattern.hs

@@ -9,8 +9,6 @@ import Control.Arrow ( first )
 import Control.Monad.Identity
 import Control.Monad.Writer
 
-import Data.Monoid
-
 import Agda.Syntax.Common
 import Agda.Syntax.Concrete
 

src/full/Agda/Syntax/Internal.hs

@@ -19,7 +19,6 @@ import Control.DeepSeq
 import Data.Function
 import qualified Data.List as List
 import Data.Maybe
-import Data.Monoid ( Monoid, mempty, mappend )
 import Data.Semigroup ( Semigroup, (<>), Sum(..) )
 
 import Data.Traversable

src/full/Agda/Syntax/Notation.hs

@@ -25,7 +25,7 @@ import qualified Data.Set as Set
 import qualified Agda.Syntax.Abstract.Name as A
 import Agda.Syntax.Common
 import Agda.Syntax.Concrete.Name
-import Agda.Syntax.Concrete.Pretty
+import Agda.Syntax.Concrete.Pretty()
 import Agda.Syntax.Position
 
 import Agda.Utils.Except ( MonadError(throwError) )

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

@@ -32,7 +32,6 @@ import Control.Monad.State hiding (mapM_, mapM)
 import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.Maybe
-import Data.Monoid ( Monoid, mempty, mappend )
 import Data.Semigroup ( Semigroup, (<>) )
 import Data.Set (Set)
 import qualified Data.Set as Set

src/full/Agda/Termination/Monad.hs

@@ -16,7 +16,6 @@ import qualified Control.Monad.Fail as Fail
 
 import Control.Monad.Reader
 
-import Data.Monoid ( Monoid(..) )
 import Data.Semigroup ( Semigroup(..) )
 import qualified Data.Set as Set
 

src/full/Agda/TypeChecking/Datatypes.hs

@@ -4,7 +4,6 @@ module Agda.TypeChecking.Datatypes where
 import Control.Monad.Except
 
 import Data.Maybe (fromMaybe)
-import qualified Data.List as List
 
 import Agda.Syntax.Common
 import Agda.Syntax.Internal

src/full/Agda/TypeChecking/Forcing.hs

@@ -64,7 +64,7 @@ module Agda.TypeChecking.Forcing
     isForced,
     nextIsForced ) where
 
-import Data.Monoid
+import Data.Monoid -- for (<>) in GHC 8.0.2
 
 import Agda.Interaction.Options
 

src/full/Agda/TypeChecking/Free.hs

@@ -61,18 +61,12 @@ module Agda.TypeChecking.Free
 
 import Prelude hiding (null)
 
-
-
-
-import Data.Monoid ( Monoid, mempty, mappend)
 import Data.Semigroup ( Semigroup, (<>), Any(..), All(..) )
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 
-
-
 import qualified Agda.Benchmarking as Bench
 
 import Agda.Syntax.Common hiding (Arg, NamedArg)

src/full/Agda/TypeChecking/Free/Lazy.hs

@@ -70,7 +70,6 @@ import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
-import Data.Monoid ( Monoid, mempty, mappend, mconcat )
 import Data.Semigroup ( Semigroup, (<>) )
 
 

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -29,14 +29,13 @@ import Data.List.NonEmpty (NonEmpty(..))
 import Data.Maybe
 import Data.Map (Map)
 import qualified Data.Map as Map -- hiding (singleton, null, empty)
-import Data.Monoid ( Monoid, mempty, mappend )
 import Data.Sequence (Seq)
 import Data.Set (Set)
 import qualified Data.Set as Set -- hiding (singleton, null, empty)
 import Data.HashMap.Strict (HashMap)
 import qualified Data.HashMap.Strict as HMap
 import Data.Semigroup ( Semigroup, (<>)) --, Any(..) )
-import Data.Data (Data, toConstr)
+import Data.Data (Data)
 import Data.String
 import Data.Text.Lazy (Text)
 import qualified Data.Text.Lazy as T

src/full/Agda/TypeChecking/Monad/Debug.hs

@@ -15,7 +15,6 @@ import Control.Monad.Trans.Identity
 import Control.Monad.Writer
 
 import Data.Maybe
-import Data.Monoid ( Monoid)
 
 import {-# SOURCE #-} Agda.TypeChecking.Errors
 import Agda.TypeChecking.Monad.Base

src/full/Agda/TypeChecking/Monad/MetaVars.hs

@@ -14,7 +14,6 @@ import qualified Data.IntMap as IntMap
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
 import qualified Data.Map as Map
-import Data.Maybe (catMaybes)
 import Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.Foldable as Fold

src/full/Agda/TypeChecking/Positivity.hs

@@ -19,7 +19,6 @@ import qualified Data.IntMap as IntMap
 import qualified Data.List as List
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Monoid (mconcat)
 import Data.Sequence (Seq)
 import qualified Data.Sequence as DS
 import Data.Set (Set)