diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
index de73acd..268a5bf 100644
--- a/src/Agda/Convert.hs
+++ b/src/Agda/Convert.hs
@@ -2,8 +2,6 @@
 
 module Agda.Convert where
 
-import Render ( Block(..), Inlines, renderATop, Render(..) )
-
 import Agda.IR (FromAgda (..))
 import qualified Agda.IR as IR
 import Agda.Interaction.Base
@@ -14,6 +12,9 @@ import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
 import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
 import qualified Agda.Interaction.Highlighting.Range as Highlighting
 import Agda.Interaction.InteractionTop (localStateCommandM)
+#if MIN_VERSION_Agda(2,7,0)
+import Agda.Interaction.Output ( OutputConstraint )
+#endif
 import Agda.Interaction.Response as R
 import Agda.Syntax.Abstract as A
 import Agda.Syntax.Abstract.Pretty (prettyATop)
@@ -22,7 +23,7 @@ import Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal (alwaysUnblock)
 import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
 import Agda.Syntax.Scope.Base
-import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError, explainWhyInScope)
+import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError)
 import Agda.TypeChecking.Monad hiding (Function)
 import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
 import Agda.TypeChecking.Pretty (prettyTCM)
@@ -35,14 +36,7 @@ import Agda.Utils.IO.TempFile (writeToTempFile)
 import Agda.Utils.Impossible (__IMPOSSIBLE__)
 import Agda.Utils.Maybe (catMaybes)
 import Agda.Utils.Null (empty)
-#if MIN_VERSION_Agda(2,6,4)
-import Agda.Syntax.Common.Pretty hiding (render)
--- import Prettyprinter hiding (Doc)
-import qualified Prettyprinter
-#else
-import Agda.Utils.Pretty hiding (render)
-#endif
-import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )
+import Agda.Utils.RangeMap (IsBasicRangeMap (toList))
 import Agda.Utils.String (delimiter)
 import Agda.Utils.Time (CPUTime)
 import Agda.VersionCommit (versionWithCommitInfo)
@@ -53,13 +47,17 @@ import qualified Data.ByteString.Lazy.Char8 as BS8
 import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.String (IsString)
+import Render (Block (..), Inlines, Render (..), renderATop)
 import qualified Render
 
-#if MIN_VERSION_Agda(2,7,0)
-import Agda.Interaction.Output ( OutputConstraint )
+#if MIN_VERSION_Agda(2,6,4)
+import Agda.Syntax.Common.Pretty hiding (render)
+import qualified Prettyprinter
+#else
+import Agda.Utils.Pretty hiding (render)
 #endif
 
-responseAbbr :: IsString a => Response -> a
+responseAbbr :: (IsString a) => Response -> a
 responseAbbr res = case res of
   Resp_HighlightingInfo {} -> "Resp_HighlightingInfo"
   Resp_Status {} -> "Resp_Status"
@@ -273,7 +271,8 @@ fromDisplayInfo = \case
       return (prettyShow x, ":" <+> doc)
     let doc =
           "Definitions about"
-            <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
+            <+> text (List.intercalate ", " $ words names)
+            $$ nest 2 (align 10 hitDocs)
     return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
   Info_WhyInScope why -> do
     doc <- explainWhyInScope why
@@ -331,18 +330,19 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
               if null boundaries
                 then []
                 else
-                  Header "Boundary" :
-                  fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
+                  Header "Boundary"
+                    : fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
         contextSect <- reverse . concat <$> mapM (renderResponseContext ii) resCtxs
         let constraintSect =
-                if null constraints
-                  then []
-                  else
-                    Header "Constraints" :
-                    fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
+              if null constraints
+                then []
+                else
+                  Header "Constraints"
+                    : fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
 
         return $
-          IR.DisplayInfoGeneric "Goal type etc" $ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
+          IR.DisplayInfoGeneric "Goal type etc" $
+            goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
       Goal_CurrentGoal norm -> do
         (rendered, raw) <- prettyTypeOfMeta norm ii
         return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)
@@ -443,8 +443,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
   modality <- asksTC getModality
 #endif
   do
-    let
-        rawCtxName :: String
+    let rawCtxName :: String
         rawCtxName
           | n == x = prettyShow x
           | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
@@ -468,7 +467,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
           where
             c = render (getCohesion ai)
 
-        extras :: IsString a => [a]
+        extras :: (IsString a) => [a]
         extras =
           concat
             [ ["not in scope" | isInScope nis == C.NotInScope],
@@ -498,7 +497,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
     -- rendered
     renderedExpr <- renderATop expr
     let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
-      -- (Render.fsep $ Render.punctuate "," extras)
+    -- (Render.fsep $ Render.punctuate "," extras)
 
     -- result
     let typeItem = Unlabeled renderedType (Just rawType) Nothing
@@ -526,7 +525,6 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
       | null docs = mempty
       | otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs
 
-
 -- | Pretty-prints the type of the meta-variable.
 prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
 prettyTypeOfMeta norm ii = do
diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs
index fb96494..e450a76 100644
--- a/src/Agda/IR.hs
+++ b/src/Agda/IR.hs
@@ -20,6 +20,7 @@ class FromAgdaTCM a b | a -> b where
   fromAgdaTCM :: a -> TCM b
 
 --------------------------------------------------------------------------------
+
 -- | IR for IOCTM
 data Response
   = -- non-last responses
diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs
index 5923248..6e52b91 100644
--- a/src/Agda/Parser.hs
+++ b/src/Agda/Parser.hs
@@ -6,17 +6,16 @@ module Agda.Parser where
 
 import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
 import Agda.Syntax.Parser.Tokens (Token)
-import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
-import Agda.Syntax.Position (RangeFile(RangeFile))
+import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, RangeFile (RangeFile), getRange, rEnd', rStart')
 import Agda.Utils.FileName (mkAbsolute)
-import Monad ( ServerM )
 import Control.Monad.State
 import Data.List (find)
 import Data.Maybe (fromMaybe)
 import Data.Text (Text, unpack)
 import qualified Data.Text as Text
+import qualified Language.LSP.Protocol.Types as LSP
 import Language.LSP.Server (LspM)
-import qualified Language.LSP.Protocol.Types   as LSP
+import Monad (ServerM)
 import Options (Config)
 
 --------------------------------------------------------------------------------
diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs
index 20a6cec..9257770 100644
--- a/src/Agda/Position.hs
+++ b/src/Agda/Position.hs
@@ -1,59 +1,66 @@
 {-# LANGUAGE CPP #-}
 
 module Agda.Position
-  ( ToOffset(..)
-  , makeToOffset
-  , toOffset
-  , FromOffset(..)
-  , makeFromOffset
-  , fromOffset
-  , toAgdaPositionWithoutFile
-  , toAgdaRange
-  , prettyPositionWithoutFile
-  -- , toLSPRange
-  -- , toLSPPosition
-  ) where
-
-import           Agda.Syntax.Position
-import           Agda.Utils.FileName            ( AbsolutePath(AbsolutePath) )
-import           Data.IntMap                    ( IntMap )
-import qualified Data.IntMap                   as IntMap
-import qualified Data.Sequence                 as Seq
-import qualified Data.Strict.Maybe             as Strict
-import           Data.Text                      ( Text )
-import qualified Data.Text                     as Text
-import qualified Language.LSP.Protocol.Types   as LSP
+  ( ToOffset (..),
+    makeToOffset,
+    toOffset,
+    FromOffset (..),
+    makeFromOffset,
+    fromOffset,
+    toAgdaPositionWithoutFile,
+    toAgdaRange,
+    prettyPositionWithoutFile,
+    -- , toLSPRange
+    -- , toLSPPosition
+  )
+where
+
+import Agda.Syntax.Position
+import Agda.Utils.FileName (AbsolutePath (AbsolutePath))
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import qualified Data.Sequence as Seq
+import qualified Data.Strict.Maybe as Strict
+import Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Language.LSP.Protocol.Types as LSP
 
 -- Note:  LSP srclocs are 0-base
 --        Agda srclocs are 1-base
 
 --------------------------------------------------------------------------------
+
 -- | LSP source locations => Agda source locations
 
 -- | LSP Range -> Agda Range
 toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range
-toAgdaRange table path (LSP.Range start end) = Range
-  (Strict.Just $ mkRangeFile $ AbsolutePath path)
-  (Seq.singleton interval)
- where
-  interval :: IntervalWithoutFile
-  interval = Interval (toAgdaPositionWithoutFile table start)
-                      (toAgdaPositionWithoutFile table end)
-  mkRangeFile path = RangeFile path Nothing
+toAgdaRange table path (LSP.Range start end) =
+  Range
+    (Strict.Just $ mkRangeFile $ AbsolutePath path)
+    (Seq.singleton interval)
+  where
+    interval :: IntervalWithoutFile
+    interval =
+      Interval
+        (toAgdaPositionWithoutFile table start)
+        (toAgdaPositionWithoutFile table end)
+    mkRangeFile path = RangeFile path Nothing
 
 -- | LSP Position -> Agda PositionWithoutFile
 toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
-toAgdaPositionWithoutFile table (LSP.Position line col) = Pn
-  ()
-  (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
-  (fromIntegral line + 1)
-  (fromIntegral col + 1)
+toAgdaPositionWithoutFile table (LSP.Position line col) =
+  Pn
+    ()
+    (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
+    (fromIntegral line + 1)
+    (fromIntegral col + 1)
 
 prettyPositionWithoutFile :: PositionWithoutFile -> String
 prettyPositionWithoutFile pos@(Pn () offset _line _col) =
   "[" <> show pos <> "-" <> show offset <> "]"
 
 --------------------------------------------------------------------------------
+
 -- | Positon => Offset convertion
 
 -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")
@@ -63,38 +70,39 @@ prettyPositionWithoutFile pos@(Pn () offset _line _col) =
 --  >def123\r\n          (2, 11)
 --  >ghi\r               (3, 15)
 --
-newtype ToOffset = ToOffset { unToOffset :: IntMap Int }
+newtype ToOffset = ToOffset {unToOffset :: IntMap Int}
 
 data Accum = Accum
-  { accumPreviousChar  :: Maybe Char
-  , accumCurrentOffset :: Int
-  , accumCurrentLine   :: Int
-  , accumResult        :: IntMap Int
+  { accumPreviousChar :: Maybe Char,
+    accumCurrentOffset :: Int,
+    accumCurrentLine :: Int,
+    accumResult :: IntMap Int
   }
 
 -- | Return a list of offsets of linebreaks ("\n", "\r" or "\r\n")
 makeToOffset :: Text -> ToOffset
 makeToOffset = ToOffset . accumResult . Text.foldl' go initAccum
- where
-  initAccum :: Accum
-  initAccum = Accum Nothing 0 0 IntMap.empty
-
-  go :: Accum -> Char -> Accum
-  go (Accum (Just '\r') n l table) '\n' =
-    Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)
-  go (Accum previous n l table) '\n' =
-    Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
-  go (Accum previous n l table) '\r' =
-    Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
-  go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
+  where
+    initAccum :: Accum
+    initAccum = Accum Nothing 0 0 IntMap.empty
+
+    go :: Accum -> Char -> Accum
+    go (Accum (Just '\r') n l table) '\n' =
+      Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)
+    go (Accum previous n l table) '\n' =
+      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
+    go (Accum previous n l table) '\r' =
+      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
+    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
 
 -- | (line, col) => offset (zero-based)
 toOffset :: ToOffset -> (Int, Int) -> Int
 toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of
-  Nothing     -> col
+  Nothing -> col
   Just offset -> offset + col
 
 --------------------------------------------------------------------------------
+
 -- | Offset => Position convertion
 
 -- An IntMap for speeding up Offset => Position convertion
@@ -105,29 +113,32 @@ toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of
 --  >def123\r\n          (11, 2)
 --  >ghi\r               (15, 3)
 --
-newtype FromOffset = FromOffset { unFromOffset :: IntMap Int }
+newtype FromOffset = FromOffset {unFromOffset :: IntMap Int}
 
 fromOffset :: FromOffset -> Int -> (Int, Int)
 fromOffset (FromOffset table) offset = case IntMap.lookupLE offset table of
-  Nothing                          -> (0, offset) -- no previous lines
+  Nothing -> (0, offset) -- no previous lines
   Just (offsetOfFirstChar, lineNo) -> (lineNo, offset - offsetOfFirstChar)
 
 makeFromOffset :: Text -> FromOffset
-makeFromOffset = FromOffset . accumResult . Text.foldl'
-  go
-  (Accum Nothing 0 0 IntMap.empty)
- where
-  go :: Accum -> Char -> Accum
-  -- encountered a "\r\n", update the latest entry
-  go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of
-    ((offset, lineNo), table') ->
-      Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')
-  -- encountered a line break, add a new entry
-  go (Accum previous n l table) '\n' =
-    Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
-  go (Accum previous n l table) '\r' =
-    Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
-  go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
+makeFromOffset =
+  FromOffset
+    . accumResult
+    . Text.foldl'
+      go
+      (Accum Nothing 0 0 IntMap.empty)
+  where
+    go :: Accum -> Char -> Accum
+    -- encountered a "\r\n", update the latest entry
+    go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of
+      ((offset, lineNo), table') ->
+        Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')
+    -- encountered a line break, add a new entry
+    go (Accum previous n l table) '\n' =
+      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
+    go (Accum previous n l table) '\r' =
+      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
+    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
 
 -- --------------------------------------------------------------------------------
 -- -- | Agda Highlighting Range -> Agda Range
diff --git a/src/Monad.hs b/src/Monad.hs
index 26c5965..3726b86 100644
--- a/src/Monad.hs
+++ b/src/Monad.hs
@@ -3,43 +3,44 @@
 
 module Monad where
 
-import           Agda.IR
-
-import           Agda.Interaction.Base          ( IOTCM )
-import           Agda.TypeChecking.Monad        ( TCMT )
-import           Control.Concurrent
-import           Control.Monad.Reader
-import           Data.Text                      ( Text
-                                                , pack
-                                                )
-import           Server.CommandController       ( CommandController )
-import qualified Server.CommandController      as CommandController
-import           Server.ResponseController      ( ResponseController )
-import qualified Server.ResponseController     as ResponseController
-
-import           Data.IORef                     ( IORef
-                                                , modifyIORef'
-                                                , newIORef
-                                                , readIORef
-                                                , writeIORef
-                                                )
-import           Data.Maybe                     ( isJust )
-import           Language.LSP.Server            ( MonadLsp
-                                                , getConfig
-                                                )
-import qualified Language.LSP.Protocol.Types   as LSP
-import           Options
+import Agda.IR
+import Agda.Interaction.Base (IOTCM)
+import Agda.TypeChecking.Monad (TCMT)
+import Control.Concurrent
+import Control.Monad.Reader
+import Data.IORef
+  ( IORef,
+    modifyIORef',
+    newIORef,
+    readIORef,
+    writeIORef,
+  )
+import Data.Maybe (isJust)
+import Data.Text
+  ( Text,
+    pack,
+  )
+import qualified Language.LSP.Protocol.Types as LSP
+import Language.LSP.Server
+  ( MonadLsp,
+    getConfig,
+  )
+import Options
+import Server.CommandController (CommandController)
+import qualified Server.CommandController as CommandController
+import Server.ResponseController (ResponseController)
+import qualified Server.ResponseController as ResponseController
 
 --------------------------------------------------------------------------------
 
 data Env = Env
-  { envOptions            :: Options
-  , envDevMode            :: Bool
-  , envConfig             :: Config
-  , envLogChan            :: Chan Text
-  , envCommandController  :: CommandController
-  , envResponseChan       :: Chan Response
-  , envResponseController :: ResponseController
+  { envOptions :: Options,
+    envDevMode :: Bool,
+    envConfig :: Config,
+    envLogChan :: Chan Text,
+    envCommandController :: CommandController,
+    envResponseChan :: Chan Response,
+    envResponseController :: ResponseController
   }
 
 createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env
diff --git a/src/Options.hs b/src/Options.hs
index ee1fd5a..37a13cb 100644
--- a/src/Options.hs
+++ b/src/Options.hs
@@ -1,27 +1,31 @@
 {-# LANGUAGE DeriveGeneric #-}
+
 module Options
-  ( Options(..)
-  , getOptionsFromArgv
-  , usageMessage
-  , Config(..)
-  , initConfig
-  ) where
-import           Data.Aeson.Types        hiding ( Options
-                                                , defaultOptions
-                                                )
-import           GHC.Generics                   ( Generic )
-import           System.Console.GetOpt
-import           System.Environment             ( getArgs )
-import           Text.Read                      ( readMaybe )
+  ( Options (..),
+    getOptionsFromArgv,
+    usageMessage,
+    Config (..),
+    initConfig,
+  )
+where
+
+import Data.Aeson.Types hiding
+  ( Options,
+    defaultOptions,
+  )
+import GHC.Generics (Generic)
+import System.Console.GetOpt
+import System.Environment (getArgs)
+import Text.Read (readMaybe)
 
 getOptionsFromArgv :: IO Options
 getOptionsFromArgv = do
-  -- extract options for Agda from ARGV 
+  -- extract options for Agda from ARGV
   (argvForALS, argvForAgda) <- extractAgdaOpts <$> getArgs
-  -- parse options for ALS 
-  (opts      , _          ) <- parseOpts argvForALS
+  -- parse options for ALS
+  (opts, _) <- parseOpts argvForALS
   -- save options for Agda back
-  return $ opts { optRawAgdaOptions = argvForAgda }
+  return $ opts {optRawAgdaOptions = argvForAgda}
 
 usageMessage :: String
 usageMessage = usageInfo usage options ++ usageAboutAgdaOptions
@@ -30,32 +34,33 @@ usageMessage = usageInfo usage options ++ usageAboutAgdaOptions
 
 -- | Command-line arguments
 data Options = Options
-  { optViaTCP         :: Maybe Int
-  , optRawAgdaOptions :: [String]
-  , optHelp           :: Bool
+  { optViaTCP :: Maybe Int,
+    optRawAgdaOptions :: [String],
+    optHelp :: Bool
   }
 
 defaultOptions :: Options
 defaultOptions =
-  Options { optViaTCP = Nothing, optRawAgdaOptions = [], optHelp = False }
+  Options {optViaTCP = Nothing, optRawAgdaOptions = [], optHelp = False}
 
 options :: [OptDescr (Options -> Options)]
 options =
-  [ Option ['h']
-           ["help"]
-           (NoArg (\opts -> opts { optHelp = True }))
-           "print this help message"
-  , Option
-    ['p']
-    ["port"]
-    (OptArg
-      (\port opts -> case port of
-        Just n  -> opts { optViaTCP = readMaybe n }
-        Nothing -> opts { optViaTCP = Just 4096 }
+  [ Option
+      ['h']
+      ["help"]
+      (NoArg (\opts -> opts {optHelp = True}))
+      "print this help message",
+    Option
+      ['p']
+      ["port"]
+      ( OptArg
+          ( \port opts -> case port of
+              Just n -> opts {optViaTCP = readMaybe n}
+              Nothing -> opts {optViaTCP = Just 4096}
+          )
+          "PORT"
       )
-      "PORT"
-    )
-    "talk with the editor via TCP port (4096 as default)"
+      "talk with the editor via TCP port (4096 as default)"
   ]
 
 usage :: String
@@ -64,41 +69,41 @@ usage = "Agda v2.7.0.1 Language Server v3\nUsage: als [Options...]\n"
 usageAboutAgdaOptions :: String
 usageAboutAgdaOptions =
   "\n\
-      \  +AGDA [Options for Agda ...] -AGDA\n\
-      \    To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n\
-      \    For example:\n\
-      \      als -p=3000 +AGDA --cubical -AGDA\n\
-      \    If you are using agda-mode on VS Code, put them in the Settings at:\n\
-      \      agdaMode.connection.commandLineOptions\n\
-      \"
+  \  +AGDA [Options for Agda ...] -AGDA\n\
+  \    To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n\
+  \    For example:\n\
+  \      als -p=3000 +AGDA --cubical -AGDA\n\
+  \    If you are using agda-mode on VS Code, put them in the Settings at:\n\
+  \      agdaMode.connection.commandLineOptions\n\
+  \"
 
 parseOpts :: [String] -> IO (Options, [String])
 parseOpts argv = case getOpt Permute options argv of
-  (o, n, []  ) -> return (foldl (flip id) defaultOptions o, n)
+  (o, n, []) -> return (foldl (flip id) defaultOptions o, n)
   (_, _, errs) -> ioError $ userError $ concat errs ++ usageInfo usage options
 
-
 -- | Removes RTS options from a list of options (stolen from Agda)
 stripRTS :: [String] -> [String]
-stripRTS []               = []
+stripRTS [] = []
 stripRTS ("--RTS" : argv) = argv
 stripRTS (arg : argv)
   | is "+RTS" arg = stripRTS $ drop 1 $ dropWhile (not . is "-RTS") argv
-  | otherwise     = arg : stripRTS argv
-  where is x arg = [x] == take 1 (words arg)
+  | otherwise = arg : stripRTS argv
+  where
+    is x arg = [x] == take 1 (words arg)
 
 -- | Extract Agda options (+AGDA ... -AGDA) from a list of options
 extractAgdaOpts :: [String] -> ([String], [String])
 extractAgdaOpts argv =
-  let (before , argv') = break (== "+AGDA") argv
+  let (before, argv') = break (== "+AGDA") argv
       (forAgda, after) = break (== "-AGDA") argv'
-      forALS           = before ++ dropWhile (== "-AGDA") after
-      forAgda'         = dropWhile (== "+AGDA") forAgda
-  in  (forALS, forAgda')
+      forALS = before ++ dropWhile (== "-AGDA") after
+      forAgda' = dropWhile (== "+AGDA") forAgda
+   in (forALS, forAgda')
 
 --------------------------------------------------------------------------------
 
-newtype Config = Config { configRawAgdaOptions :: [String] }
+newtype Config = Config {configRawAgdaOptions :: [String]}
   deriving (Eq, Show, Generic)
 
 instance FromJSON Config where
diff --git a/src/Render.hs b/src/Render.hs
index 15661a4..dd30cd0 100644
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -10,7 +10,7 @@ import Render.Concrete
 import Render.Interaction ()
 import Render.Internal ()
 import Render.Name ()
+import Render.Position ()
 import Render.RichText
 import Render.TypeChecking ()
-import Render.Position ()
 import Render.Utils ()
diff --git a/src/Render/Class.hs b/src/Render/Class.hs
index 6ac7718..7d340d7 100644
--- a/src/Render/Class.hs
+++ b/src/Render/Class.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Render.Class
   ( Render (..),
@@ -12,11 +12,11 @@ module Render.Class
   )
 where
 
-import           Agda.Syntax.Fixity (Precedence (TopCtx))
+import Agda.Syntax.Fixity (Precedence (TopCtx))
 import qualified Agda.Syntax.Translation.AbstractToConcrete as A
-import qualified Agda.TypeChecking.Monad.Base               as A
-import           Agda.Utils.List1 (List1)
-import           Agda.Utils.List2 (List2)
+import qualified Agda.TypeChecking.Monad.Base as A
+import Agda.Utils.List1 (List1)
+import Agda.Utils.List2 (List2)
 #if MIN_VERSION_Agda(2,6,4)
 import           Agda.Syntax.Common.Pretty (Doc)
 import qualified Agda.Syntax.Common.Pretty as Doc
@@ -25,8 +25,8 @@ import           Agda.Utils.Pretty (Doc)
 import qualified Agda.Utils.Pretty as Doc
 #endif
 
-import           Data.Int (Int32)
-import           GHC.Exts ( IsList(toList) )
+import Data.Int (Int32)
+import GHC.Exts (IsList (toList))
 import Render.RichText
 
 --------------------------------------------------------------------------------
@@ -77,14 +77,15 @@ instance Render Bool where
 instance Render Doc where
   render = text . Doc.render
 
-instance Render a => Render (Maybe a) where
-  renderPrec p Nothing  = mempty
+instance (Render a) => Render (Maybe a) where
+  renderPrec p Nothing = mempty
   renderPrec p (Just x) = renderPrec p x
 
-instance Render a => Render [a] where
+instance (Render a) => Render [a] where
   render xs = "[" <> fsep (punctuate "," (fmap render xs)) <> "]"
-instance Render a => Render (List1 a) where
+
+instance (Render a) => Render (List1 a) where
   render = render . toList
 
-instance Render a => Render (List2 a) where
+instance (Render a) => Render (List2 a) where
   render = render . toList
diff --git a/src/Render/Common.hs b/src/Render/Common.hs
index fbb5d63..0e59798 100644
--- a/src/Render/Common.hs
+++ b/src/Render/Common.hs
@@ -3,35 +3,36 @@
 module Render.Common where
 
 import Agda.Syntax.Common
-    ( Named(namedThing),
-      Hiding(NotHidden, Hidden, Instance),
-      LensHiding(getHiding),
-      RewriteEqn'(..),
-      MetaId(MetaId),
-      LensQuantity(getQuantity),
-      Quantity(..),
-      LensRelevance(getRelevance),
-      Relevance(..),
-      Induction(..),
-      Cohesion(..),
-      QωOrigin(..),
-      LensCohesion(getCohesion),
-      NameId(..),
-      Erased(..), asQuantity, Lock(..), 
+  ( Cohesion (..),
+    Erased (..),
+    Hiding (Hidden, Instance, NotHidden),
+    Induction (..),
+    LensCohesion (getCohesion),
+    LensHiding (getHiding),
+    LensQuantity (getQuantity),
+    LensRelevance (getRelevance),
+    Lock (..),
 #if MIN_VERSION_Agda(2,6,4)
-      LockOrigin (..), 
+    LockOrigin (..),
 #endif
+    MetaId (MetaId),
+    NameId (..),
+    Named (namedThing),
 #if MIN_VERSION_Agda(2,7,0)
-      OverlapMode (..),
+    OverlapMode (..),
 #endif
-    )
+    Quantity (..),
+    QωOrigin (..),
+    Relevance (..),
+    RewriteEqn' (..),
+    asQuantity,
+  )
+import Agda.Utils.Functor ((<&>))
+import Agda.Utils.List1 (toList)
+import qualified Agda.Utils.List1 as List1
 import qualified Agda.Utils.Null as Agda
-import           Agda.Utils.List1 (toList)
-import           Agda.Utils.Functor ((<&>))
-
 import Render.Class
 import Render.RichText
-import qualified Agda.Utils.List1 as List1
 
 --------------------------------------------------------------------------------
 
@@ -67,24 +68,24 @@ instance Render Quantity where
 instance Render QωOrigin where
   render = \case
     QωInferred -> mempty
-    Qω{}       -> "@ω"
-    QωPlenty{} -> "@plenty"
+    Qω {} -> "@ω"
+    QωPlenty {} -> "@plenty"
 
 instance Render Cohesion where
-  render Flat   = "@♭"
+  render Flat = "@♭"
   render Continuous = mempty
-  render Squash  = "@⊤"
+  render Squash = "@⊤"
 
 --------------------------------------------------------------------------------
 
 #if MIN_VERSION_Agda(2,7,0)
 instance Render OverlapMode where
   render = \case
-    Overlappable   -> "OVERLAPPABLE"
-    Overlapping    -> "OVERLAPPING"
-    Incoherent     -> "INCOHERENT"
-    Overlaps       -> "OVERLAPS"
-    FieldOverlap   -> "overlap"
+    Overlappable -> "OVERLAPPABLE"
+    Overlapping -> "OVERLAPPING"
+    Incoherent -> "INCOHERENT"
+    Overlaps -> "OVERLAPS"
+    FieldOverlap -> "overlap"
     DefaultOverlap -> mempty
 #endif
 
@@ -94,18 +95,18 @@ instance Render OverlapMode where
 --   @renderHiding info visible text@ puts the correct braces
 --   around @text@ according to info @info@ and returns
 --   @visible text@ if the we deal with a visible thing.
-renderHiding :: LensHiding a => a -> (Inlines -> Inlines) -> Inlines -> Inlines
+renderHiding :: (LensHiding a) => a -> (Inlines -> Inlines) -> Inlines -> Inlines
 renderHiding a parensF =
   case getHiding a of
     Hidden -> braces'
     Instance {} -> dbraces
     NotHidden -> parensF
 
-renderRelevance :: LensRelevance a => a -> Inlines -> Inlines
+renderRelevance :: (LensRelevance a) => a -> Inlines -> Inlines
 renderRelevance a d =
   if show d == "_" then d else render (getRelevance a) <> d
 
-renderQuantity :: LensQuantity a => a -> Inlines -> Inlines
+renderQuantity :: (LensQuantity a) => a -> Inlines -> Inlines
 renderQuantity a d =
   if show d == "_" then d else render (getQuantity a) <+> d
 
@@ -114,7 +115,7 @@ instance Render Lock where
 #if MIN_VERSION_Agda(2,6,4)
     IsLock LockOLock -> "@lock"
     IsLock LockOTick -> "@tick"
-#else 
+#else
     IsLock -> "@lock"
 #endif
     IsNotLock -> mempty
@@ -124,17 +125,16 @@ renderErased :: Erased -> Inlines -> Inlines
 renderErased = renderQuantity . asQuantity
 #endif
 
-renderCohesion :: LensCohesion a => a -> Inlines -> Inlines
+renderCohesion :: (LensCohesion a) => a -> Inlines -> Inlines
 renderCohesion a d =
   if show d == "_" then d else render (getCohesion a) <+> d
 
 --------------------------------------------------------------------------------
 
-
 instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where
   render = \case
-    Rewrite es   -> prefixedThings (text "rewrite") (render . snd <$> toList es)
-    Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\ (p, e) -> render p <+> "<-" <+> render e) . namedThing)
+    Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es)
+    Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\(p, e) -> render p <+> "<-" <+> render e) . namedThing)
 #if MIN_VERSION_Agda(2,7,0)
     LeftLet pes  -> prefixedThings (text "using") [render p <+> "<-" <+> render e | (p, e) <- List1.toList pes]
 #endif
@@ -145,5 +145,5 @@ prefixedThings kw = \case
   (doc : docs) -> fsep $ (kw <+> doc) : fmap ("|" <+>) docs
 
 instance Render Induction where
-  render Inductive   = "inductive"
+  render Inductive = "inductive"
   render CoInductive = "coinductive"
diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs
index e865ef2..3fd39df 100644
--- a/src/Render/Concrete.hs
+++ b/src/Render/Concrete.hs
@@ -5,23 +5,20 @@
 
 module Render.Concrete where
 
-import qualified Data.Text     as T
-import Data.Maybe (isNothing, maybeToList)
-import qualified Data.Strict.Maybe as Strict
-
 import Agda.Syntax.Common
-import           Agda.Syntax.Concrete
-import           Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
---import           Agda.Syntax.Position (noRange)
-import           Agda.Utils.List1 as List1 (toList, fromList)
-import qualified Agda.Utils.List1 as List1
-import qualified Agda.Utils.List2 as List2
+import Agda.Syntax.Concrete
+import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
 import Agda.Utils.Float (toStringWithoutDotZero)
 import Agda.Utils.Function
-import Agda.Utils.Null
 import Agda.Utils.Functor (dget, (<&>))
 import Agda.Utils.Impossible (__IMPOSSIBLE__)
-
+import Agda.Utils.List1 as List1 (fromList, toList)
+import qualified Agda.Utils.List1 as List1
+import qualified Agda.Utils.List2 as List2
+import Agda.Utils.Null
+import Data.Maybe (isNothing, maybeToList)
+import qualified Data.Strict.Maybe as Strict
+import qualified Data.Text as T
 import Render.Class
 import Render.Common
 import Render.Literal ()
@@ -33,23 +30,24 @@ import Prelude hiding (null)
 --------------------------------------------------------------------------------
 
 #if MIN_VERSION_Agda(2,7,0)
-instance Render a => Render (TacticAttribute' a) where
+instance (Render a) => Render (TacticAttribute' a) where
   render (TacticAttribute t) =
-    ifNull (render t) empty $ \ d -> "@" <> parens ("tactic" <+> d)
+    ifNull (render t) empty $ \d -> "@" <> parens ("tactic" <+> d)
 #endif
 
-instance Render a => Render (Ranged a) where
+instance (Render a) => Render (Ranged a) where
   render = render . rangedThing
 
-instance Render a => Render (WithHiding a) where
+instance (Render a) => Render (WithHiding a) where
   render w = renderHiding w id $ render $ dget w
 
 instance Render Modality where
-  render mod = hsep
-    [ render (getRelevance mod)
-    , render (getQuantity mod)
-    , render (getCohesion mod)
-    ]
+  render mod =
+    hsep
+      [ render (getRelevance mod),
+        render (getQuantity mod),
+        render (getCohesion mod)
+      ]
 
 -- | OpApp
 instance Render (OpApp Expr) where
@@ -57,7 +55,7 @@ instance Render (OpApp Expr) where
   render (SyntaxBindingLambda r bs e) = render (Lam r bs e)
 
 -- | MaybePlaceholder
-instance Render a => Render (MaybePlaceholder a) where
+instance (Render a) => Render (MaybePlaceholder a) where
   render Placeholder {} = "_"
   render (NoPlaceholder _ e) = render e
 
@@ -138,15 +136,12 @@ instance Render Expr where
       absurd Instance {} = "{{}}"
       absurd Hidden = "{}"
 
--- instance RenderTCM Expr where
---   renderTCM = render
-
 --------------------------------------------------------------------------------
 
 instance (Render a, Render b) => Render (Either a b) where
   render = either render render
 
-instance Render a => Render (FieldAssignment' a) where
+instance (Render a) => Render (FieldAssignment' a) where
   render (FieldAssignment x e) = sep [render x <+> "=", render e]
 
 instance Render ModuleAssignment where
@@ -165,7 +160,7 @@ instance Render LamClause where
 instance Render BoundName where
   render BName {boundName = x} = render x
 
-instance Render a => Render (Binder' a) where
+instance (Render a) => Render (Binder' a) where
   render (Binder mpat n) =
     let d = render n
      in case mpat of
@@ -177,42 +172,50 @@ instance Render a => Render (Binder' a) where
 -- | NamedBinding
 instance Render NamedBinding where
 #if MIN_VERSION_Agda(2,7,0)
-  render (NamedBinding withH
-           x@(Arg (ArgInfo h (Modality r q c) _o _fv (Annotation lock))
-               (Named _mn xb@(Binder _mp (BName _y _fix t _fin))))) =
-    applyWhen withH prH $
-    applyWhenJust (isLabeled x) (\ l -> (text l <+>) . ("=" <+>)) (render xb)
-      -- isLabeled looks at _mn and _y
-      -- pretty xb prints also the pattern _mp
-    where
-    prH = (render r <>)
-        . renderHiding h mparens
-        . (coh <+>)
-        . (qnt <+>)
-        . (lck <+>)
-        . (tac <+>)
-    coh = render c
-    qnt = render q
-    tac = render t
-    lck = render lock
-    -- Parentheses are needed when an attribute @... is printed
-    mparens = applyUnless (null coh && null qnt && null lck && null tac) parens
-#else 
+  render
+    ( NamedBinding
+        withH
+        x@( Arg
+              (ArgInfo h (Modality r q c) _o _fv (Annotation lock))
+              (Named _mn xb@(Binder _mp (BName _y _fix t _fin)))
+            )
+      ) =
+      applyWhen withH prH $
+        applyWhenJust (isLabeled x) (\l -> (text l <+>) . ("=" <+>)) (render xb)
+      where
+        -- isLabeled looks at _mn and _y
+        -- pretty xb prints also the pattern _mp
+
+        prH =
+          (render r <>)
+            . renderHiding h mparens
+            . (coh <+>)
+            . (qnt <+>)
+            . (lck <+>)
+            . (tac <+>)
+        coh = render c
+        qnt = render q
+        tac = render t
+        lck = render lock
+        -- Parentheses are needed when an attribute @... is printed
+        mparens = applyUnless (null coh && null qnt && null lck && null tac) parens
+
+#else
   render (NamedBinding withH x) =
     prH $
       if
-          | Just l <- isLabeled x -> text l <> " = " <> render xb
-          | otherwise -> render xb
+        | Just l <- isLabeled x -> text l <> " = " <> render xb
+        | otherwise -> render xb
     where
       xb = namedArg x
       bn = binderName xb
       prH
         | withH =
-          renderRelevance x
-            . renderHiding x mparens'
-            . renderCohesion x
-            . renderQuantity x
-            . renderTactic bn
+            renderRelevance x
+              . renderHiding x mparens'
+              . renderCohesion x
+              . renderQuantity x
+              . renderTactic bn
         | otherwise = id
       -- Parentheses are needed when an attribute @... is present
       mparens'
@@ -231,8 +234,6 @@ renderTactic' Nothing d = d
 renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d)
 #endif
 
-
-
 --------------------------------------------------------------------------------
 
 -- | LamBinding
@@ -297,18 +298,22 @@ instance Render WhereClause where
   render (AnyWhere _range [Module _ x [] ds])
 #endif
     | isNoName (unqualify x) =
-      vcat ["where", vcat $ fmap render ds]
+        vcat ["where", vcat $ fmap render ds]
   render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds]
 #if MIN_VERSION_Agda(2,7,0)
   render (SomeWhere _ erased m a ds) =
-    vcat [ hsep $ privateWhenUserWritten a
-             [ "module", renderErased erased (render m), "where" ]
-         , vcat $ map render ds
-         ]
+    vcat
+      [ hsep $
+          privateWhenUserWritten
+            a
+            ["module", renderErased erased (render m), "where"],
+        vcat $ map render ds
+      ]
     where
       privateWhenUserWritten = \case
         PrivateAccess _ UserWritten -> ("private" :)
         _ -> id
+
 #else
 #if MIN_VERSION_Agda(2,6,4)
   render (SomeWhere _range _er m a ds) =
@@ -335,19 +340,19 @@ instance Render LHS where
     where
       renderWithd :: WithExpr -> Inlines
       renderWithd (Named nm wh) =
-        let e = render wh in
-        case nm of
-          Nothing -> e
-          Just n  -> render n <+> ":" <+> e
+        let e = render wh
+         in case nm of
+              Nothing -> e
+              Just n -> render n <+> ":" <+> e
 
 instance Render LHSCore where
   render (LHSHead f ps) = sep $ render f : fmap (parens . render) ps
   render (LHSProj d ps lhscore ps') =
     sep $
-      render d :
-      fmap (parens . render) ps
-        ++ parens (render lhscore) :
-      fmap (parens . render) ps'
+      render d
+        : fmap (parens . render) ps
+        ++ parens (render lhscore)
+        : fmap (parens . render) ps'
   render (LHSWith h wps ps) =
     if null ps
       then doc
@@ -384,16 +389,18 @@ instance Render Declaration where
               renderHiding i id $
                 renderCohesion i $
                   renderQuantity i $
-                    render $ TypeSig (setRelevance Relevant i) tac x e
+                    render $
+                      TypeSig (setRelevance Relevant i) tac x e
         where
           mkInst (InstanceDef _) f = sep ["instance", f]
           mkInst NotInstanceDef f = f
 #if MIN_VERSION_Agda(2,7,0)
-          mkOverlap i d | isYesOverlap i = "overlap" <+> d
+          mkOverlap i d
+            | isYesOverlap i = "overlap" <+> d
 #else
           mkOverlap i d | isOverlappable i = "overlap" <+> d
 #endif
-                        | otherwise        = d
+            | otherwise = d
       Field _ fs ->
         sep
           [ "field",
@@ -465,10 +472,9 @@ instance Render Declaration where
                 render e
               ]
           ]
-
 #if MIN_VERSION_Agda(2,7,0)
       Record _ erased x dir tel e cs -> pRecord erased x dir tel (Just e) cs
-#else 
+#else
 #if MIN_VERSION_Agda(2,6,4)
       Record _ _er x dir tel e cs -> pRecord x dir tel (Just e) cs
 #else
@@ -480,18 +486,19 @@ instance Render Declaration where
 #else
       RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs
 #endif
-#if MIN_VERSION_Agda(2,7,0)
-#else
+#if !MIN_VERSION_Agda(2,7,0)
       RecordDirective r -> pRecordDirective r
 #endif
       Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs))
       Syntax n _ -> "syntax" <+> render n <+> "..."
       PatternSyn _ n as p ->
-        "pattern" <+> render n <+> fsep (fmap render as)
+        "pattern"
+          <+> render n
+          <+> fsep (fmap render as)
           <+> "="
           <+> render p
       Mutual _ ds -> namedBlock "mutual" ds
-      InterleavedMutual _ ds  -> namedBlock "interleaved mutual" ds
+      InterleavedMutual _ ds -> namedBlock "interleaved mutual" ds
       LoneConstructor _ ds -> namedBlock "constructor" ds
       Abstract _ ds -> namedBlock "abstract" ds
       Private _ _ ds -> namedBlock "private" ds
@@ -519,22 +526,24 @@ instance Render Declaration where
 #else
       ModuleMacro _ x m open i -> case m of
 #endif
-       (SectionApp _ [] e) | open == DoOpen, isNoName x ->
+        (SectionApp _ [] e)
+          | open == DoOpen,
+            isNoName x ->
+              fsep
+                [ render open,
+                  render e,
+                  render i
+                ]
+        (SectionApp _ tel e) ->
           fsep
-            [ render open,
-              render e,
-              render i
+            [ render open <+> "module" <+> render x <+> fcat (fmap render tel),
+              "=" <+> render e <+> render i
+            ]
+        (RecordModuleInstance _ rec) ->
+          fsep
+            [ render open <+> "module" <+> render x,
+              "=" <+> render rec <+> "{{...}}"
             ]
-       (SectionApp _ tel e) ->
-        fsep
-          [ render open <+> "module" <+> render x <+> fcat (fmap render tel),
-            "=" <+> render e <+> render i
-          ]
-       (RecordModuleInstance _ rec) ->
-        fsep
-          [ render open <+> "module" <+> render x,
-            "=" <+> render rec <+> "{{...}}"
-          ]
       Open _ x i -> hsep ["open", render x, render i]
       Import _ x rn open i ->
         hsep [render open, "import", render x, as rn, render i]
@@ -547,7 +556,7 @@ instance Render Declaration where
         fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]
       Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
       UnquoteData _ x xs e ->
-        fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ]
+        fsep [hsep ["unquoteData", render x, fsep (fmap render xs), "="], render e]
 #if MIN_VERSION_Agda(2,6,4)
       Opaque _ ds ->
         namedBlock "opaque" ds
@@ -555,6 +564,7 @@ instance Render Declaration where
         fsep ("unfolding" : fmap render xs)
 #endif
     where
+
       namedBlock s ds =
         fsep
           [ text s,
@@ -563,7 +573,7 @@ instance Render Declaration where
 
 pHasEta0 :: HasEta0 -> Inlines
 pHasEta0 = \case
-  YesEta   -> "eta-equality"
+  YesEta -> "eta-equality"
   NoEta () -> "no-eta-equality"
 
 instance Render RecordDirective where
@@ -574,42 +584,49 @@ pRecordDirective ::
   Inlines
 pRecordDirective = \case
   Induction ind -> render ind
-  Constructor n inst -> hsep [ pInst, "constructor", render n ] where
-    pInst = case inst of
-      InstanceDef{} -> "instance"
-      NotInstanceDef{} -> mempty
+  Constructor n inst -> hsep [pInst, "constructor", render n]
+    where
+      pInst = case inst of
+        InstanceDef {} -> "instance"
+        NotInstanceDef {} -> mempty
   Eta eta -> pHasEta0 (rangedThing eta)
-  PatternOrCopattern{} -> "pattern"
+  PatternOrCopattern {} -> "pattern"
 
 #if MIN_VERSION_Agda(2,7,0)
-pRecord
-  :: Erased
-  -> Name
-  -> [RecordDirective]
-  -> [LamBinding]
-  -> Maybe Expr
-  -> [Declaration]
-  -> Inlines
-pRecord erased x directives tel me ds = vcat
+pRecord ::
+  Erased ->
+  Name ->
+  [RecordDirective] ->
+  [LamBinding] ->
+  Maybe Expr ->
+  [Declaration] ->
+  Inlines
+pRecord erased x directives tel me ds =
+  vcat
     [ sep
-      [ hsep  [ "record"
-              , renderErased erased (render x)
-              , fsep (map render tel)
-              ]
-      , pType me
-      ]
-    , vcat $ concat
-      [ map render directives
-      , map render ds
-      ]
+        [ hsep
+            [ "record",
+              renderErased erased (render x),
+              fsep (map render tel)
+            ],
+          pType me
+        ],
+      vcat $
+        concat
+          [ map render directives,
+            map render ds
+          ]
     ]
-  where pType (Just e) = hsep
-                [ ":"
-                , render e
-                , "where"
-                ]
-        pType Nothing  =
-                  "where"
+  where
+    pType (Just e) =
+      hsep
+        [ ":",
+          render e,
+          "where"
+        ]
+    pType Nothing =
+      "where"
+
 #else
 pRecord ::
   Name ->
@@ -692,10 +709,10 @@ instance Render Pragma where
     hsep ("POLARITY" : render q : fmap render occs)
   render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
   render (NotProjectionLikePragma _ q) =
-    hsep [ "NOT_PROJECTION_LIKE", render q ]
+    hsep ["NOT_PROJECTION_LIKE", render q]
 #if MIN_VERSION_Agda(2,7,0)
   render (InjectiveForInferencePragma _ i) =
-    hsep $ ["INJECTIVE_FOR_INFERENCE", render i]
+    hsep ["INJECTIVE_FOR_INFERENCE", render i]
   render (OverlapPragma _ x m) = hsep [render m, render x]
 #endif
 
@@ -710,10 +727,10 @@ instance Render Fixity where
 
 instance Render NotationPart where
   render = \case
-    IdPart  x  -> text $ rangedThing x
-    HolePart{} -> "_"
+    IdPart x -> text $ rangedThing x
+    HolePart {} -> "_"
     VarPart {} -> "_"
-    WildPart{} -> "_"
+    WildPart {} -> "_"
 
 instance Render Fixity' where
   render (Fixity' fix nota _)
@@ -721,7 +738,7 @@ instance Render Fixity' where
     | otherwise = "syntax" <+> render nota
 
 -- | Arg
-instance Render a => Render (Arg a) where
+instance (Render a) => Render (Arg a) where
   renderPrec p (Arg ai e) = renderHiding ai localParens $ renderPrec p' e
     where
       p'
@@ -732,7 +749,7 @@ instance Render a => Render (Arg a) where
         | otherwise = id
 
 -- | Named NamedName (Named_)
-instance Render e => Render (Named NamedName e) where
+instance (Render e) => Render (Named NamedName e) where
   renderPrec p (Named nm e)
     | Just s <- bareNameOf nm = mparens (p > 0) $ sep [text s <> " =", render e]
     | otherwise = renderPrec p e
@@ -767,7 +784,7 @@ bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ fmap (";" <+>) ds ++ ["}"])
 
 renderOpApp ::
   forall a.
-  Render a =>
+  (Render a) =>
   QName ->
   [NamedArg (MaybePlaceholder a)] ->
   [Inlines]
@@ -780,7 +797,7 @@ renderOpApp q args = merge [] $ prOp moduleNames concreteNames args
       Name _ _ xs -> List1.toList xs
       NoName {} -> __IMPOSSIBLE__
 
-    prOp :: Render a => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
+    prOp :: (Render a) => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
     prOp ms (Hole : xs) (e : es) =
       case namedArg e of
         Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es
@@ -790,8 +807,8 @@ renderOpApp q args = merge [] $ prOp moduleNames concreteNames args
     prOp ms (Id x : xs) es =
       ( qual ms $ render $ simpleName x,
         Nothing
-      ) :
-      prOp [] xs es
+      )
+        : prOp [] xs es
     -- Qualify the name part with the module.
     -- We then clear @ms@ such that the following name parts will not be qualified.
 
diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs
index e352d57..012209a 100644
--- a/src/Render/Interaction.hs
+++ b/src/Render/Interaction.hs
@@ -3,53 +3,58 @@
 
 module Render.Interaction where
 
-import qualified Data.IntMap                   as IntMap
-import qualified Data.Map                      as Map
-import qualified Data.Set                      as Set
-
-import           Agda.Interaction.Base
+import Agda.Interaction.Base
 #if MIN_VERSION_Agda(2,7,0)
-import           Agda.Interaction.Output        ( OutputForm, OutputConstraint )
+import Agda.Interaction.Output (OutputConstraint, OutputForm)
 #endif
-import           Agda.Syntax.Internal           ( Blocker(..) )
-import           Agda.TypeChecking.Monad
-import           Render.Class
-import           Render.Concrete                ( )
-import           Render.Internal                ( )
-import           Render.Name                    ( )
-import           Render.Position                ( )
-import           Render.RichText
-import           Render.TypeChecking            ( )
+import Agda.Syntax.Internal (Blocker (..))
+import Agda.TypeChecking.Monad
+import qualified Data.IntMap as IntMap
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Render.Class
+import Render.Concrete ()
+import Render.Internal ()
+import Render.Name ()
+import Render.Position ()
+import Render.RichText
+import Render.TypeChecking ()
 
 --------------------------------------------------------------------------------
 
 -- | OutputForm
-
 instance (Render a, Render b) => Render (OutputForm a b) where
-  render (OutputForm r pids unblock c) = fsep
-    [render c, prange r, parens (sep [blockedOn unblock, prPids pids])]
-   where
-    prPids []    = mempty
-    prPids [pid] = parens $ "belongs to problem" <+> render pid
-    prPids pids' = parens $ "belongs to problems" <+> fsep
-      (punctuate "," $ fmap render pids')
+  render (OutputForm r pids unblock c) =
+    fsep
+      [render c, prange r, parens (sep [blockedOn unblock, prPids pids])]
+    where
+      prPids [] = mempty
+      prPids [pid] = parens $ "belongs to problem" <+> render pid
+      prPids pids' =
+        parens $
+          "belongs to problems"
+            <+> fsep
+              (punctuate "," $ fmap render pids')
 
-    comma | null pids = mempty
-          | otherwise = ","
+      comma
+        | null pids = mempty
+        | otherwise = ","
 
-    blockedOn (UnblockOnAll bs) | Set.null bs = mempty
-    blockedOn (UnblockOnAny bs) | Set.null bs = "stuck" <> comma
-    blockedOn u = "blocked on" <+> (render u <> comma)
+      blockedOn (UnblockOnAll bs) | Set.null bs = mempty
+      blockedOn (UnblockOnAny bs) | Set.null bs = "stuck" <> comma
+      blockedOn u = "blocked on" <+> (render u <> comma)
 
-    prange rr | null s    = mempty
-              | otherwise = text $ " [ at " ++ s ++ " ]"
-      where s = show $ render rr
+      prange rr
+        | null s = mempty
+        | otherwise = text $ " [ at " ++ s ++ " ]"
+        where
+          s = show $ render rr
 
 -- | OutputConstraint
 instance (Render a, Render b) => Render (OutputConstraint a b) where
   render (OfType name expr) = render name <> " : " <> render expr
-  render (JustType name   ) = "Type " <> render name
-  render (JustSort name   ) = "Sort " <> render name
+  render (JustType name) = "Type " <> render name
+  render (JustSort name) = "Sort " <> render name
   render (CmpInType cmp expr name1 name2) =
     render name1
       <> " "
@@ -79,7 +84,7 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where
     render name <> " := " <> render expr1 <> " :? " <> render expr2
   render (PostponedCheckArgs name exprs expr1 expr2) =
     let exprs' = fmap (parens . render) exprs
-    in  render name
+     in render name
           <> " := "
           <> parens ("_ : " <> render expr1)
           <> " "
@@ -87,16 +92,16 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where
           <> " : "
           <> render expr2
   render (IsEmptyType expr) = "Is empty: " <> render expr
-  render (SizeLtSat   expr) = "Not empty type of sizes: " <> render expr
+  render (SizeLtSat expr) = "Not empty type of sizes: " <> render expr
   render (FindInstanceOF name expr exprs) =
     let exprs' =
           (\(q, e, t) -> render q <> "=" <> render e <> " : " <> render t)
             <$> exprs
-    in  fsep
-          [ "Resolve instance argument "
-          , render name <> " : " <> render expr
-          , "Candidate:"
-          , vcat exprs'
+     in fsep
+          [ "Resolve instance argument ",
+            render name <> " : " <> render expr,
+            "Candidate:",
+            vcat exprs'
           ]
 #if MIN_VERSION_Agda(2,7,0)
   render (ResolveInstanceOF q) = "Resolve output type of instance" <?> render q
@@ -110,17 +115,17 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where
   render (UsableAtMod modality t) =
     "Is usable at" <+> render modality <+> render t
   render (DataSort _name expr) =
-    fsep [ "Sort", render expr, "allows data/record definitions" ]
+    fsep ["Sort", render expr, "allows data/record definitions"]
 
 -- | IPBoundary'
-instance Render c => Render (IPBoundary' c) where
+instance (Render c) => Render (IPBoundary' c) where
 #if MIN_VERSION_Agda(2,6,4)
   render (IPBoundary m) = vcat $ flip fmap (Map.toList m) $ \case
     (boundary, rhs) ->
       fsep (punctuate "," xs) <+> "⊢" <+> render rhs
       where
         xs = flip fmap (IntMap.toList boundary) $ \(l, r) ->
-          text $ concat [ "@", show l, " = ", if r then "i1" else "i0" ]
+          text $ concat ["@", show l, " = ", if r then "i1" else "i0"]
 #else
   render (IPBoundary eqs val meta over) = do
     let xs  = fmap (\(l, r) -> render l <+> "=" <+> render r) eqs
diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs
index 2ef5994..5db6b75 100644
--- a/src/Render/Internal.hs
+++ b/src/Render/Internal.hs
@@ -3,14 +3,12 @@
 
 module Render.Internal where
 
-import Control.Monad
-import qualified Data.List as List
-import qualified Data.Set as Set
-
 import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing))
 import Agda.Syntax.Internal hiding (telToList)
 import Agda.Utils.Function (applyWhen)
-
+import Control.Monad
+import qualified Data.List as List
+import qualified Data.Set as Set
 import Render.Class
 import Render.Common (renderHiding)
 import Render.Concrete ()
@@ -18,7 +16,7 @@ import Render.RichText
 
 --------------------------------------------------------------------------------
 
-instance Render a => Render (Substitution' a) where
+instance (Render a) => Render (Substitution' a) where
   renderPrec = pr
     where
       pr p input = case input of
@@ -72,7 +70,7 @@ instance (Render t, Render e) => Render (Dom' t e) where
         | Just t <- domTactic dom = "@" <> parens ("tactic" <+> render t)
         | otherwise = mempty
 
-renderDom :: LensHiding a => a -> Inlines -> Inlines
+renderDom :: (LensHiding a) => a -> Inlines -> Inlines
 renderDom i =
   case getHiding i of
     NotHidden -> parens
@@ -93,7 +91,7 @@ instance Render Clause where
       pBody (Just b) Nothing = render b
       pBody (Just b) (Just t) = fsep [render b <+> ":", render t]
 
-instance Render a => Render (Tele (Dom a)) where
+instance (Render a) => Render (Tele (Dom a)) where
   render tel = fsep [renderDom a (text x <+> ":" <+> render (unDom a)) | (x, a) <- telToList tel]
     where
       telToList EmptyTel = []
@@ -118,7 +116,7 @@ instance Render Level where
 instance Render PlusLevel where
   renderPrec p (Plus n a) = renderPrecLevelSucs p n $ \p' -> renderPrec p' a
 
---instance Render LevelAtom where
+-- instance Render LevelAtom where
 -- LevelAtom is just Term
 --  renderPrec p a =
 --    case a of
@@ -130,51 +128,52 @@ instance Render PlusLevel where
 instance Render Sort where
   renderPrec p = \case
 #if MIN_VERSION_Agda(2,6,4)
-      Univ u (ClosedLevel n) -> text $ suffix n $ showUniv u
-      Univ u l -> mparens (p > 9) $ text (showUniv u) <+> renderPrec 10 l
-      Inf u n -> text $ suffix n $ showUniv u ++ "ω"
-      LevelUniv -> "LevelUniv"
+    Univ u (ClosedLevel n) -> text $ suffix n $ showUniv u
+    Univ u l -> mparens (p > 9) $ text (showUniv u) <+> renderPrec 10 l
+    Inf u n -> text $ suffix n $ showUniv u ++ "ω"
+    LevelUniv -> "LevelUniv"
 #else
-      Type (ClosedLevel 0) -> "Set"
-      Type (ClosedLevel n) -> text $ "Set" ++ show n
-      Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l
-      Prop (ClosedLevel 0) -> "Prop"
-      Prop (ClosedLevel n) -> text $ "Prop" ++ show n
-      Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l
-      Inf IsFibrant 0 -> "Setω"
-      Inf IsStrict 0 -> "SSetω"
-      Inf IsFibrant n -> text $ "Setω" ++ show n
-      Inf IsStrict n -> text $ "SSetω" ++ show n
-      SSet l -> mparens (p > 9) $ "SSet" <+> renderPrec 10 l
+    Type (ClosedLevel 0) -> "Set"
+    Type (ClosedLevel n) -> text $ "Set" ++ show n
+    Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l
+    Prop (ClosedLevel 0) -> "Prop"
+    Prop (ClosedLevel n) -> text $ "Prop" ++ show n
+    Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l
+    Inf IsFibrant 0 -> "Setω"
+    Inf IsStrict 0 -> "SSetω"
+    Inf IsFibrant n -> text $ "Setω" ++ show n
+    Inf IsStrict n -> text $ "SSetω" ++ show n
+    SSet l -> mparens (p > 9) $ "SSet" <+> renderPrec 10 l
 #endif
-      SizeUniv -> "SizeUniv"
-      LockUniv -> "LockUniv"
-      PiSort a _s1 s2 ->
-        mparens (p > 9) $
-          "piSort" <+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a))
-            <+> parens
-              ( fsep
-                  [ text ("λ " ++ absName s2 ++ " ->"),
-                    render (unAbs s2)
-                  ]
-              )
-      FunSort a b ->
-        mparens (p > 9) $
-          "funSort" <+> renderPrec 10 a <+> renderPrec 10 b
-      UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s
-      MetaS x es -> renderPrec p $ MetaV x es
-      DefS d es -> renderPrec p $ Def d es
-      DummyS s -> parens $ text s
-      IntervalUniv -> "IntervalUniv"
+    SizeUniv -> "SizeUniv"
+    LockUniv -> "LockUniv"
+    PiSort a _s1 s2 ->
+      mparens (p > 9) $
+        "piSort"
+          <+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a))
+          <+> parens
+            ( fsep
+                [ text ("λ " ++ absName s2 ++ " ->"),
+                  render (unAbs s2)
+                ]
+            )
+    FunSort a b ->
+      mparens (p > 9) $
+        "funSort" <+> renderPrec 10 a <+> renderPrec 10 b
+    UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s
+    MetaS x es -> renderPrec p $ MetaV x es
+    DefS d es -> renderPrec p $ Def d es
+    DummyS s -> parens $ text s
+    IntervalUniv -> "IntervalUniv"
 #if MIN_VERSION_Agda(2,6,4)
-   where
-     suffix n = applyWhen (n /= 0) (++ show n)
+    where
+      suffix n = applyWhen (n /= 0) (++ show n)
 #endif
 
 instance Render Type where
   renderPrec p (El _ a) = renderPrec p a
 
-instance Render tm => Render (Elim' tm) where
+instance (Render tm) => Render (Elim' tm) where
   renderPrec p (Apply v) = renderPrec p v
   renderPrec _ (Proj _o x) = "." <> render x
   renderPrec p (IApply _ _ r) = renderPrec p r
@@ -182,7 +181,7 @@ instance Render tm => Render (Elim' tm) where
 instance Render DBPatVar where
   renderPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)
 
-instance Render a => Render (Pattern' a) where
+instance (Render a) => Render (Pattern' a) where
   renderPrec n (VarP _o x) = renderPrec n x
   renderPrec _ (DotP _o t) = "." <> renderPrec 10 t
   renderPrec n (ConP c i nps) =
@@ -212,8 +211,8 @@ instance Render a => Render (Pattern' a) where
 -- Agda.Syntax.Internal.Blockers
 
 instance Render Blocker where
-  render (UnblockOnAll us)      = "all" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
-  render (UnblockOnAny us)      = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
-  render (UnblockOnMeta m)      = render m
+  render (UnblockOnAll us) = "all" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
+  render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
+  render (UnblockOnMeta m) = render m
   render (UnblockOnProblem pid) = "problem" <+> render pid
-  render (UnblockOnDef q)       = "definition" <+> render q
+  render (UnblockOnDef q) = "definition" <+> render q
diff --git a/src/Render/Literal.hs b/src/Render/Literal.hs
index ba966c2..984288d 100644
--- a/src/Render/Literal.hs
+++ b/src/Render/Literal.hs
@@ -1,19 +1,19 @@
 module Render.Literal where
 
-import Agda.Syntax.Literal ( Literal(..), showChar', showText )
+import Agda.Syntax.Literal (Literal (..), showChar', showText)
 import Render.Class
-import Render.RichText
-import Render.Name ()
 import Render.Common ()
+import Render.Name ()
+import Render.RichText
 
 --------------------------------------------------------------------------------
 
 -- | Literal
 instance Render Literal where
-  render (LitNat n)    = text $ show n
+  render (LitNat n) = text $ show n
   render (LitWord64 n) = text $ show n
-  render (LitFloat d)  = text $ show d
+  render (LitFloat d) = text $ show d
   render (LitString s) = text $ showText s ""
-  render (LitChar c)   = text $ "'" ++ showChar' c "'"
-  render (LitQName x)  = render x
+  render (LitChar c) = text $ "'" ++ showChar' c "'"
+  render (LitQName x) = render x
   render (LitMeta _ x) = render x
\ No newline at end of file
diff --git a/src/Render/Name.hs b/src/Render/Name.hs
index ae5abda..5f88c9a 100644
--- a/src/Render/Name.hs
+++ b/src/Render/Name.hs
@@ -1,35 +1,33 @@
 module Render.Name where
 
 import qualified Agda.Syntax.Abstract as A
+import qualified Agda.Syntax.Common as C
 import qualified Agda.Syntax.Concrete as C
-import qualified Agda.Syntax.Common   as C
-import qualified Agda.Utils.List1     as Agda
-
+import qualified Agda.Utils.List1 as Agda
 import Render.Class
 import Render.RichText
 
 --------------------------------------------------------------------------------
 
--- | Concrete 
+-- | Concrete
 instance Render C.NamePart where
   render C.Hole = "_"
   render (C.Id s) = text $ C.rawNameToString s
 
--- glueing name parts together 
+-- glueing name parts together
 instance Render C.Name where
-  render (C.Name range _inScope xs) = linkRange range $ mconcat (fmap render $ Agda.toList xs)
+  render (C.Name range _inScope xs) = linkRange range $ mconcat (render <$> Agda.toList xs)
   render (C.NoName _ _) = "_"
 
 instance Render C.QName where
   render (C.Qual m x)
     | C.isUnderscore m = render x -- don't print anonymous modules
-    | otherwise      = render m <> "." <> render x
-  render (C.QName x)  = render x
-
+    | otherwise = render m <> "." <> render x
+  render (C.QName x) = render x
 
 --------------------------------------------------------------------------------
 
--- | Abstract 
+-- | Abstract
 instance Render A.Name where
   render = render . A.nameConcrete
 
diff --git a/src/Render/Position.hs b/src/Render/Position.hs
index c72c839..e53b28b 100644
--- a/src/Render/Position.hs
+++ b/src/Render/Position.hs
@@ -13,11 +13,11 @@ instance Render AbsolutePath where
   render = text . filePath
 
 instance Render RangeFile where
-  render = render . rangeFilePath  -- TODO rangeFileName ?
+  render = render . rangeFilePath -- TODO rangeFileName ?
 
 --------------------------------------------------------------------------------
 
-instance Render a => Render (Position' (Strict.Maybe a)) where
+instance (Render a) => Render (Position' (Strict.Maybe a)) where
   render (Pn Strict.Nothing _ l c) = render l <> "," <> render c
   render (Pn (Strict.Just f) _ l c) =
     render f <> ":" <> render l <> "," <> render c
@@ -39,7 +39,7 @@ instance Render IntervalWithoutFile where
         | sl == el = render ec
         | otherwise = render el <> "," <> render ec
 
-instance Render a => Render (Interval' (Strict.Maybe a)) where
+instance (Render a) => Render (Interval' (Strict.Maybe a)) where
   render i@(Interval s _) = file <> render (setIntervalFile () i)
     where
       file :: Inlines
@@ -47,5 +47,5 @@ instance Render a => Render (Interval' (Strict.Maybe a)) where
         Strict.Nothing -> mempty
         Strict.Just f -> render f <> ":"
 
-instance Render a => Render (Range' (Strict.Maybe a)) where
+instance (Render a) => Render (Range' (Strict.Maybe a)) where
   render r = maybe mempty render (rangeToIntervalWithFile r)
diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs
index 29a85de..3bcb0cb 100644
--- a/src/Render/RichText.hs
+++ b/src/Render/RichText.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 
 module Render.RichText
-  ( Block(..),
+  ( Block (..),
     Inlines (..),
     -- LinkTarget (..),
     space,
@@ -41,32 +41,30 @@ where
 
 -- import qualified Agda.Interaction.Options   as Agda
 -- import qualified Agda.Syntax.Concrete.Glyph as Agda
-import qualified Agda.Syntax.Position       as Agda
-import qualified Agda.Utils.FileName        as Agda
-import qualified Agda.Utils.Null            as Agda
-import           Agda.Utils.Suffix (toSubscriptDigit)
-
-import           Data.Aeson (ToJSON (toJSON), Value (Null))
-import           Data.Foldable (toList)
-import           Data.Sequence (Seq (..))
-import qualified Data.Sequence     as Seq
-import           Data.String (IsString (..))
-import qualified Data.Strict.Maybe as Strict
-
-import           GHC.Generics (Generic)
+import qualified Agda.Syntax.Position as Agda
+import qualified Agda.Utils.FileName as Agda
 import Agda.Utils.Null
+import qualified Agda.Utils.Null as Agda
+import Agda.Utils.Suffix (toSubscriptDigit)
+import Data.Aeson (ToJSON (toJSON), Value (Null))
+import Data.Foldable (toList)
+import Data.Sequence (Seq (..))
+import qualified Data.Sequence as Seq
+import qualified Data.Strict.Maybe as Strict
+import Data.String (IsString (..))
+import GHC.Generics (Generic)
 import Prelude hiding (null)
 
 --------------------------------------------------------------------------------
--- | Block elements
 
+-- | Block elements
 data Block
-  -- for blocks like "Goal" & "Have"
-  = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String
-  -- for ordinary goals & context
-  | Unlabeled Inlines (Maybe String) (Maybe Agda.Range)
-  -- headers
-  | Header String
+  = -- for blocks like "Goal" & "Have"
+    Labeled Inlines (Maybe String) (Maybe Agda.Range) String String
+  | -- for ordinary goals & context
+    Unlabeled Inlines (Maybe String) (Maybe Agda.Range)
+  | -- headers
+    Header String
   deriving (Generic)
 
 instance ToJSON Block
@@ -83,21 +81,20 @@ instance Semigroup Inlines where
   Inlines as <> Inlines bs = Inlines (merge as bs)
     where
       merge :: Seq Inline -> Seq Inline -> Seq Inline
-      merge Empty      ys = ys
+      merge Empty ys = ys
       merge (xs :|> x) ys = merge xs (cons x ys)
 
       cons :: Inline -> Seq Inline -> Seq Inline
       cons (Text s c) (Text t d :<| xs)
         -- merge 2 adjacent Text if they have the same classnames
-        | c == d    = Text (s <> t) c :<| xs
+        | c == d = Text (s <> t) c :<| xs
         | otherwise = Text s c :<| Text t d :<| xs
       cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs
-      cons (Text s c) (Horz (Inlines t:ts) :<| xs)
+      cons (Text s c) (Horz (Inlines t : ts) :<| xs) =
         -- merge Text with Horz when possible
-        = Horz (Inlines (cons (Text s c) t) :ts) :<| xs
+        Horz (Inlines (cons (Text s c) t) : ts) :<| xs
       cons x xs = x :<| xs
 
-
 instance Monoid Inlines where
   mempty = Inlines mempty
 
@@ -124,7 +121,6 @@ instance Null Inlines where
 
 -- -- | see if the rendered text is "empty"
 
-
 infixr 6 <+>
 
 (<+>) :: Inlines -> Inlines -> Inlines
@@ -134,6 +130,7 @@ x <+> y
   | otherwise = x <> " " <> y
 
 infixl 6 <?>
+
 -- | A synonym for '<+>' at the moment
 (<?>) :: Inlines -> Inlines -> Inlines
 (<?>) = (<+>)
@@ -221,10 +218,9 @@ instance ToJSON Agda.RangeFile where
 
 -- | Utilities / Combinators
 
-
 -- TODO: implement this
 -- Modeled after `nest` defined in ‘Text.PrettyPrint.Annotated.HughesPJ’ (pretty-1.1.3.6)
--- 
+--
 -- Indent a Inline by a given number of positions (which may also be negative). `indent` satisfies the laws:
 --
 -- `indent`  0 x = x
@@ -317,6 +313,7 @@ showIndex = map toSubscriptDigit . show
 
 --------------------------------------------------------------------------------
 --
+
 -- | Picking the appropriate set of special characters depending on
 -- whether we are allowed to use unicode or have to limit ourselves
 -- to ascii.
diff --git a/src/Render/TypeChecking.hs b/src/Render/TypeChecking.hs
index 49d9305..0ba57b8 100644
--- a/src/Render/TypeChecking.hs
+++ b/src/Render/TypeChecking.hs
@@ -8,9 +8,9 @@ import Render.Common
 import Render.RichText
 
 instance Render NamedMeta where
-  render (NamedMeta ""  x) = render x
+  render (NamedMeta "" x) = render x
   render (NamedMeta "_" x) = render x
-  render (NamedMeta s   x) = "_" <> text s <> render x
+  render (NamedMeta s x) = "_" <> text s <> render x
 
 instance Render Occurrence where
   render =
diff --git a/src/Render/Utils.hs b/src/Render/Utils.hs
index 52246df..641103b 100644
--- a/src/Render/Utils.hs
+++ b/src/Render/Utils.hs
@@ -2,7 +2,7 @@
 
 module Render.Utils where
 
-import Agda.Utils.Time ( CPUTime )
+import Agda.Utils.Time (CPUTime)
 #if MIN_VERSION_Agda(2,6,4)
 import Agda.Syntax.Common.Pretty (pretty)
 #else
diff --git a/src/Server/CommandController.hs b/src/Server/CommandController.hs
index 89f43f1..657b3d7 100644
--- a/src/Server/CommandController.hs
+++ b/src/Server/CommandController.hs
@@ -15,10 +15,10 @@ import Prelude hiding (take)
 
 data CommandController
   = CommandController
+      -- | Unbounded Command queue
       (SizedChan IOTCM)
-      -- ^ Unbounded Command queue
+      -- | MVar for the Command consumer
       (MVar IOTCM)
-      -- ^ MVar for the Command consumer
 
 new :: IO CommandController
 new = CommandController <$> newSizedChan <*> newEmptyMVar
diff --git a/src/Server/ResponseController.hs b/src/Server/ResponseController.hs
index 174e372..97e444a 100644
--- a/src/Server/ResponseController.hs
+++ b/src/Server/ResponseController.hs
@@ -2,28 +2,28 @@
 -- Makes sure that all dispatched works are done.
 -- Notify when all dispatched works are done.
 module Server.ResponseController
-  ( ResponseController
-  , new
-  , dispatch
-  , setCheckpointAndWait
-  ) where
+  ( ResponseController,
+    new,
+    dispatch,
+    setCheckpointAndWait,
+  )
+where
 
-import           Control.Concurrent
-import           Control.Concurrent.SizedChan
-import           Control.Monad                  ( void
-                                                , when
-                                                )
-import           Data.IORef
+import Control.Concurrent
+import Control.Concurrent.SizedChan
+import Control.Monad
+  ( void,
+    when,
+  )
+import Data.IORef
 
 data ResponseController = ResponseController
   { -- | The number of work dispatched
-    dispatchedCount :: IORef Int
-  ,
+    dispatchedCount :: IORef Int,
     -- | The number of work completed
-    completedCount  :: IORef Int
-  ,
+    completedCount :: IORef Int,
     -- | A channel of "Checkpoints" to be met
-    checkpointChan  :: SizedChan Checkpoint
+    checkpointChan :: SizedChan Checkpoint
   }
 
 -- | An "Checkpoint" is just a number with a callback, the callback will be invoked once the number is "met"
@@ -47,7 +47,7 @@ dispatch controller = do
     result <- tryPeekSizedChan (checkpointChan controller)
     case result of
       -- no checkpoints, do nothing
-      Nothing                     -> return ()
+      Nothing -> return ()
       -- a checkpoint is set!
       Just (dispatched, callback) -> do
         completed <- readIORef (completedCount controller)
@@ -62,7 +62,7 @@ dispatch controller = do
 setCheckpoint :: ResponseController -> (() -> IO ()) -> IO ()
 setCheckpoint controller callback = do
   dispatched <- readIORef (dispatchedCount controller)
-  completed  <- readIORef (completedCount controller)
+  completed <- readIORef (completedCount controller)
   -- see if the previously dispatched works have been completed
   if dispatched == completed
     then callback ()
diff --git a/src/Switchboard.hs b/src/Switchboard.hs
index d18156e..5d3183c 100644
--- a/src/Switchboard.hs
+++ b/src/Switchboard.hs
@@ -3,30 +3,31 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeApplications #-}
 
-module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy, agdaCustomMethod ) where
+module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy, agdaCustomMethod) where
 
-import Monad
+import qualified Agda
 import Control.Concurrent
-import qualified Server.ResponseController as ResponseController
 import Control.Monad
 import Control.Monad.Reader
-import qualified Agda
 import qualified Data.Aeson as JSON
+import Data.IORef
+import Data.Proxy (Proxy (Proxy))
 import qualified Data.Text.IO as Text
-import Language.LSP.Server
-import Data.Proxy (Proxy(Proxy))
 import Language.LSP.Protocol.Message
-import Language.LSP.Protocol.Types
-  hiding (TextDocumentSyncClientCapabilities (..))
-import Data.IORef
+import Language.LSP.Protocol.Types hiding
+  ( TextDocumentSyncClientCapabilities (..),
+  )
+import Language.LSP.Server
+import Monad
 import Options (Config)
+import qualified Server.ResponseController as ResponseController
 import System.IO (stderr)
 
 data Switchboard = Switchboard
-  { sbPrintLog :: ThreadId
-  , sbSendResponse :: ThreadId
-  , sbRunAgda :: ThreadId
-  , sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv Config))
+  { sbPrintLog :: ThreadId,
+    sbSendResponse :: ThreadId,
+    sbRunAgda :: ThreadId,
+    sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv Config))
   }
 
 -- | All channels go in and out from here