{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE UndecidableInstances       #-}

module Agda.TypeChecking.Monad.Base where

import Prelude hiding (null)

import qualified Control.Concurrent as C
import qualified Control.Exception as E
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Maybe
import Control.Applicative hiding (empty)

import Data.Function
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map -- hiding (singleton, null, empty)
import Data.Set (Set)
import qualified Data.Set as Set -- hiding (singleton, null, empty)
import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend, Any(..))
import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable
import Data.IORef

import qualified System.Console.Haskeline as Haskeline

import Agda.Benchmarking (Benchmark, Phase)

import Agda.Syntax.Concrete (TopLevelModuleName)
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Definitions as D
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract (AllNames)
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern ()
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Parser (PM(..), ParseWarning, runPMIO)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import qualified Agda.Syntax.Info as Info

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Free.Lazy (Free'(freeVars'), bind', bind)

-- import {-# SOURCE #-} Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Response
  (InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
  (CompressedFile, HighlightingInfo)

import qualified Agda.Compiler.UHC.Pragmas.Base as CR

import Agda.Utils.Except
  ( Error(strMsg)
  , ExceptT
  , MonadError(catchError, throwError)
  , runExceptT
  )

import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.FileName
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Functor

#include "undefined.h"
import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Type checking state
---------------------------------------------------------------------------

data TCState = TCSt
  { stPreScopeState   :: !PreScopeState
    -- ^ The state which is frozen after scope checking.
  , stPostScopeState  :: !PostScopeState
    -- ^ The state which is modified after scope checking.
  , stPersistentState :: !PersistentTCState
    -- ^ State which is forever, like a diamond.
  }

class Monad m => ReadTCState m where
  getTCState :: m TCState

instance Show TCState where
  show _ = "TCSt{}"

data PreScopeState = PreScopeState
  { stPreTokens             :: !CompressedFile -- from lexer
    -- ^ Highlighting info for tokens (but not those tokens for
    -- which highlighting exists in 'stSyntaxInfo').
  , stPreImports            :: !Signature  -- XX populated by scopec hecker
    -- ^ Imported declared identifiers.
    --   Those most not be serialized!
  , stPreImportedModules    :: !(Set ModuleName)  -- imports logic
  , stPreModuleToSource     :: !ModuleToSource   -- imports
  , stPreVisitedModules     :: !VisitedModules   -- imports
  , stPreScope              :: !ScopeInfo
    -- generated by scope checker, current file: which modules you have, public definitions, current file, maps concrete names to abstract names.
  , stPrePatternSyns        :: !A.PatternSynDefns
    -- ^ Pattern synonyms of the current file.  Serialized.
  , stPrePatternSynImports  :: !A.PatternSynDefns
    -- ^ Imported pattern synonyms.  Must not be serialized!
  , stPrePragmaOptions      :: !PragmaOptions
    -- ^ Options applying to the current file. @OPTIONS@
    -- pragmas only affect this field.
  , stPreImportedBuiltins   :: !(BuiltinThings PrimFun)
  , stPreImportedDisplayForms :: !DisplayForms
    -- ^ Display forms added by someone else to imported identifiers
  , stPreImportedInstanceDefs :: !InstanceTable
  , stPreHaskellImports     :: !(Set String)
    -- ^ Imports that should be generated by the compiler / MAlonzo
    -- (this includes imports from imported modules).
  , stPreHaskellImportsUHC  :: !(Set String)
    -- ^ Imports that should be generated by the compiler / UHC backend
    -- (this includes imports from imported modules).
  , stPreHaskellCode        :: ![String]
    -- ^ Inline Haskell code that should be inserted by the GHC backend
  , stPreFreshInteractionId :: !InteractionId
  }

type DisambiguatedNames = IntMap A.QName

data PostScopeState = PostScopeState
  { stPostSyntaxInfo          :: !CompressedFile
    -- ^ Highlighting info.
  , stPostDisambiguatedNames  :: !DisambiguatedNames
    -- ^ Disambiguation carried out by the type checker.
    --   Maps position of first name character to disambiguated @'A.QName'@
    --   for each @'A.AmbiguousQName'@ already passed by the type checker.
  , stPostMetaStore           :: !MetaStore
  , stPostInteractionPoints   :: !InteractionPoints -- scope checker first
  , stPostSolvedInteractionPoints :: !InteractionPoints
    -- ^ Interaction points that have been filled by a give or solve action.
  , stPostAwakeConstraints    :: !Constraints
  , stPostSleepingConstraints :: !Constraints
  , stPostDirty               :: !Bool -- local
    -- ^ Dirty when a constraint is added, used to prevent pointer update.
    -- Currently unused.
  , stPostOccursCheckDefs     :: !(Set QName) -- local
    -- ^ Definitions to be considered during occurs check.
    --   Initialized to the current mutual block before the check.
    --   During occurs check, we remove definitions from this set
    --   as soon we have checked them.
  , stPostSignature           :: !Signature
    -- ^ Declared identifiers of the current file.
    --   These will be serialized after successful type checking.
  , stPostModuleParameters    :: !ModuleParamDict
    -- ^ TODO: can these be moved into the @TCEnv@?
  , stPostImportsDisplayForms :: !DisplayForms
    -- ^ Display forms we add for imported identifiers
  , stPostCurrentModule       :: !(Maybe ModuleName)
    -- ^ The current module is available after it has been type
    -- checked.
  , stPostInstanceDefs        :: !TempInstanceTable
  , stPostStatistics          :: !Statistics
    -- ^ Counters to collect various statistics about meta variables etc.
    --   Only for current file.
  , stPostTCWarnings          :: ![TCWarning]
  , stPostMutualBlocks        :: !(Map MutualId MutualBlock)
  , stPostLocalBuiltins       :: !(BuiltinThings PrimFun)
  , stPostFreshMetaId         :: !MetaId
  , stPostFreshMutualId       :: !MutualId
  , stPostFreshCtxId          :: !CtxId
  , stPostFreshProblemId      :: !ProblemId
  , stPostFreshInt            :: !Int
  , stPostFreshNameId         :: !NameId
  }

-- | A mutual block of names in the signature.
data MutualBlock = MutualBlock
  { mutualInfo  :: Info.MutualInfo
    -- ^ The original info of the mutual block.
  , mutualNames :: Set QName
  } deriving (Show, Eq)

instance Null MutualBlock where
  empty = MutualBlock empty empty

-- | A part of the state which is not reverted when an error is thrown
-- or the state is reset.
data PersistentTCState = PersistentTCSt
  { stDecodedModules    :: DecodedModules
  , stPersistentOptions :: CommandLineOptions
  , stInteractionOutputCallback  :: InteractionOutputCallback
    -- ^ Callback function to call when there is a response
    --   to give to the interactive frontend.
    --   See the documentation of 'InteractionOutputCallback'.
  , stBenchmark         :: !Benchmark
    -- ^ Structure to track how much CPU time was spent on which Agda phase.
    --   Needs to be a strict field to avoid space leaks!
  , stAccumStatistics   :: !Statistics
    -- ^ Should be strict field.
  , stLoadedFileCache   :: !(Maybe LoadedFileCache)
    -- ^ Cached typechecking state from the last loaded file.
    --   Should be Nothing when checking imports.
  }

data LoadedFileCache = LoadedFileCache
  { lfcCached  :: !CachedTypeCheckLog
  , lfcCurrent :: !CurrentTypeCheckLog
  }

-- | A log of what the type checker does and states after the action is
-- completed.  The cached version is stored first executed action first.
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]

-- | Like 'CachedTypeCheckLog', but storing the log for an ongoing type
-- checking of a module.  Stored in reverse order (last performed action
-- first).
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]

-- | A complete log for a module will look like this:
--
--   * 'Pragmas'
--
--   * 'EnterSection', entering the main module.
--
--   * 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested
--     modules
--
--   * 'LeaveSection', leaving the main module.
data TypeCheckAction
  = EnterSection !Info.ModuleInfo !ModuleName ![A.TypedBindings]
  | LeaveSection !ModuleName
  | Decl !A.Declaration
    -- ^ Never a Section or ScopeDecl
  | Pragmas !PragmaOptions

-- | Empty persistent state.

initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
  { stPersistentOptions         = defaultOptions
  , stDecodedModules            = Map.empty
  , stInteractionOutputCallback = defaultInteractionOutputCallback
  , stBenchmark                 = empty
  , stAccumStatistics           = Map.empty
  , stLoadedFileCache           = Nothing
  }

-- | Empty state of type checker.

initPreScopeState :: PreScopeState
initPreScopeState = PreScopeState
  { stPreTokens               = mempty
  , stPreImports              = emptySignature
  , stPreImportedModules      = Set.empty
  , stPreModuleToSource       = Map.empty
  , stPreVisitedModules       = Map.empty
  , stPreScope                = emptyScopeInfo
  , stPrePatternSyns          = Map.empty
  , stPrePatternSynImports    = Map.empty
  , stPrePragmaOptions        = defaultInteractionOptions
  , stPreImportedBuiltins     = Map.empty
  , stPreImportedDisplayForms = HMap.empty
  , stPreImportedInstanceDefs = Map.empty
  , stPreHaskellImports       = Set.empty
  , stPreHaskellImportsUHC    = Set.empty
  , stPreHaskellCode          = []
  , stPreFreshInteractionId   = 0
  }

initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
  { stPostSyntaxInfo           = mempty
  , stPostDisambiguatedNames   = IntMap.empty
  , stPostMetaStore            = Map.empty
  , stPostInteractionPoints    = Map.empty
  , stPostSolvedInteractionPoints = Map.empty
  , stPostAwakeConstraints     = []
  , stPostSleepingConstraints  = []
  , stPostDirty                = False
  , stPostOccursCheckDefs      = Set.empty
  , stPostSignature            = emptySignature
  , stPostModuleParameters     = Map.empty
  , stPostImportsDisplayForms  = HMap.empty
  , stPostCurrentModule        = Nothing
  , stPostInstanceDefs         = (Map.empty , Set.empty)
  , stPostStatistics           = Map.empty
  , stPostTCWarnings           = []
  , stPostMutualBlocks         = Map.empty
  , stPostLocalBuiltins        = Map.empty
  , stPostFreshMetaId          = 0
  , stPostFreshMutualId        = 0
  , stPostFreshCtxId           = 0
  , stPostFreshProblemId       = 1
  , stPostFreshInt             = 0
  , stPostFreshNameId           = NameId 0 0
  }

initState :: TCState
initState = TCSt
  { stPreScopeState   = initPreScopeState
  , stPostScopeState  = initPostScopeState
  , stPersistentState = initPersistentState
  }

-- * st-prefixed lenses
------------------------------------------------------------------------

stTokens :: Lens' CompressedFile TCState
stTokens f s =
  f (stPreTokens (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreTokens = x}}

stImports :: Lens' Signature TCState
stImports f s =
  f (stPreImports (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreImports = x}}

stImportedModules :: Lens' (Set ModuleName) TCState
stImportedModules f s =
  f (stPreImportedModules (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedModules = x}}

stModuleToSource :: Lens' ModuleToSource TCState
stModuleToSource f s =
  f (stPreModuleToSource (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreModuleToSource = x}}

stVisitedModules :: Lens' VisitedModules TCState
stVisitedModules f s =
  f (stPreVisitedModules (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreVisitedModules = x}}

stScope :: Lens' ScopeInfo TCState
stScope f s =
  f (stPreScope (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreScope = x}}

stPatternSyns :: Lens' A.PatternSynDefns TCState
stPatternSyns f s =
  f (stPrePatternSyns (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSyns = x}}

stPatternSynImports :: Lens' A.PatternSynDefns TCState
stPatternSynImports f s =
  f (stPrePatternSynImports (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSynImports = x}}

stPragmaOptions :: Lens' PragmaOptions TCState
stPragmaOptions f s =
  f (stPrePragmaOptions (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPrePragmaOptions = x}}

stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins f s =
  f (stPreImportedBuiltins (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedBuiltins = x}}

stHaskellImports :: Lens' (Set String) TCState
stHaskellImports f s =
  f (stPreHaskellImports (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellImports = x}}

stHaskellImportsUHC :: Lens' (Set String) TCState
stHaskellImportsUHC f s =
  f (stPreHaskellImportsUHC (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellImportsUHC = x}}

stHaskellCode :: Lens' [String] TCState
stHaskellCode f s =
  f (stPreHaskellCode (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellCode = x}}

stFreshInteractionId :: Lens' InteractionId TCState
stFreshInteractionId f s =
  f (stPreFreshInteractionId (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}

stFreshNameId :: Lens' NameId TCState
stFreshNameId f s =
  f (stPostFreshNameId (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshNameId = x}}

stSyntaxInfo :: Lens' CompressedFile TCState
stSyntaxInfo f s =
  f (stPostSyntaxInfo (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostSyntaxInfo = x}}

stDisambiguatedNames :: Lens' DisambiguatedNames TCState
stDisambiguatedNames f s =
  f (stPostDisambiguatedNames (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostDisambiguatedNames = x}}

stMetaStore :: Lens' MetaStore TCState
stMetaStore f s =
  f (stPostMetaStore (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostMetaStore = x}}

stInteractionPoints :: Lens' InteractionPoints TCState
stInteractionPoints f s =
  f (stPostInteractionPoints (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}}

stSolvedInteractionPoints :: Lens' InteractionPoints TCState
stSolvedInteractionPoints f s =
  f (stPostSolvedInteractionPoints (stPostScopeState s)) <&>
  \ x -> s {stPostScopeState = (stPostScopeState s)
             {stPostSolvedInteractionPoints = x}}

stAwakeConstraints :: Lens' Constraints TCState
stAwakeConstraints f s =
  f (stPostAwakeConstraints (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostAwakeConstraints = x}}

stSleepingConstraints :: Lens' Constraints TCState
stSleepingConstraints f s =
  f (stPostSleepingConstraints (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostSleepingConstraints = x}}

stDirty :: Lens' Bool TCState
stDirty f s =
  f (stPostDirty (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostDirty = x}}

stOccursCheckDefs :: Lens' (Set QName) TCState
stOccursCheckDefs f s =
  f (stPostOccursCheckDefs (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostOccursCheckDefs = x}}

stSignature :: Lens' Signature TCState
stSignature f s =
  f (stPostSignature (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}}

stModuleParameters :: Lens' (ModuleParamDict) TCState
stModuleParameters f s =
  f (stPostModuleParameters (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostModuleParameters = x}}

stImportsDisplayForms :: Lens' DisplayForms TCState
stImportsDisplayForms f s =
  f (stPostImportsDisplayForms (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostImportsDisplayForms = x}}

stImportedDisplayForms :: Lens' DisplayForms TCState
stImportedDisplayForms f s =
  f (stPreImportedDisplayForms (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}}

stCurrentModule :: Lens' (Maybe ModuleName) TCState
stCurrentModule f s =
  f (stPostCurrentModule (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = x}}

stImportedInstanceDefs :: Lens' InstanceTable TCState
stImportedInstanceDefs f s =
  f (stPreImportedInstanceDefs (stPreScopeState s)) <&>
  \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedInstanceDefs = x}}

stInstanceDefs :: Lens' TempInstanceTable TCState
stInstanceDefs f s =
  f (stPostInstanceDefs (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostInstanceDefs = x}}

stStatistics :: Lens' Statistics TCState
stStatistics f s =
  f (stPostStatistics (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}}

stTCWarnings :: Lens' [TCWarning] TCState
stTCWarnings f s =
  f (stPostTCWarnings (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}}

stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks f s =
  f (stPostMutualBlocks (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}}

stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins f s =
  f (stPostLocalBuiltins (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostLocalBuiltins = x}}

stFreshMetaId :: Lens' MetaId TCState
stFreshMetaId f s =
  f (stPostFreshMetaId (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMetaId = x}}

stFreshMutualId :: Lens' MutualId TCState
stFreshMutualId f s =
  f (stPostFreshMutualId (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMutualId = x}}

stFreshCtxId :: Lens' CtxId TCState
stFreshCtxId f s =
  f (stPostFreshCtxId (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshCtxId = x}}

stFreshProblemId :: Lens' ProblemId TCState
stFreshProblemId f s =
  f (stPostFreshProblemId (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshProblemId = x}}

stFreshInt :: Lens' Int TCState
stFreshInt f s =
  f (stPostFreshInt (stPostScopeState s)) <&>
  \x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshInt = x}}

stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings s = (s^.stLocalBuiltins) `Map.union` (s^.stImportedBuiltins)

-- * Fresh things
------------------------------------------------------------------------

class Enum i => HasFresh i where
    freshLens :: Lens' i TCState
    nextFresh' :: i -> i
    nextFresh' = succ

nextFresh :: HasFresh i => TCState -> (i, TCState)
nextFresh s =
  let !c = s^.freshLens
  in (c, set freshLens (nextFresh' c) s)

fresh :: (HasFresh i, MonadState TCState m) => m i
fresh =
    do  !s <- get
        let (!c , !s') = nextFresh s
        put s'
        return c

instance HasFresh MetaId where
  freshLens = stFreshMetaId

instance HasFresh MutualId where
  freshLens = stFreshMutualId

instance HasFresh InteractionId where
  freshLens = stFreshInteractionId

instance HasFresh NameId where
  freshLens = stFreshNameId
  -- nextFresh increments the current fresh name by 2 so @NameId@s used
  -- before caching starts do not overlap with the ones used after.
  nextFresh' = succ . succ

instance HasFresh CtxId where
  freshLens = stFreshCtxId

instance HasFresh Int where
  freshLens = stFreshInt

newtype ProblemId = ProblemId Nat
  deriving (Typeable, Eq, Ord, Enum, Real, Integral, Num)

-- TODO: 'Show' should output Haskell-parseable representations.
-- The following instance is deprecated, and Pretty[TCM] should be used
-- instead. Later, simply derive Show for this type.

-- ASR (28 December 2014). This instance is not used anymore (module
-- the test suite) when reporting errors. See Issue 1293.

instance Show ProblemId where
  show (ProblemId n) = show n

instance Pretty ProblemId where
  pretty (ProblemId n) = pretty n

instance HasFresh ProblemId where
  freshLens = stFreshProblemId

freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name
freshName r s = do
  i <- fresh
  return $ mkName r i s

freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name
freshNoName r =
    do  i <- fresh
        return $ Name i (C.NoName noRange i) r noFixity'

freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name
freshNoName_ = freshNoName noRange

-- | Create a fresh name from @a@.
class FreshName a where
  freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name

instance FreshName (Range, String) where
  freshName_ = uncurry freshName

instance FreshName String where
  freshName_ = freshName noRange

instance FreshName Range where
  freshName_ = freshNoName

instance FreshName () where
  freshName_ () = freshNoName_

---------------------------------------------------------------------------
-- ** Managing file names
---------------------------------------------------------------------------

-- | Maps top-level module names to the corresponding source file
-- names.

type ModuleToSource = Map TopLevelModuleName AbsolutePath

-- | Maps source file names to the corresponding top-level module
-- names.

type SourceToModule = Map AbsolutePath TopLevelModuleName

-- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
--
--   O(n log n).
--
--   For a single reverse lookup in 'stModuleToSource',
--   rather use 'lookupModuleFromSourse'.

sourceToModule :: TCM SourceToModule
sourceToModule =
  Map.fromList
     .  List.map (\(m, f) -> (f, m))
     .  Map.toList
    <$> use stModuleToSource

-- | Lookup an 'AbsolutePath' in 'sourceToModule'.
--
--   O(n).

lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
lookupModuleFromSource f =
  fmap fst . List.find ((f ==) . snd) . Map.toList <$> use stModuleToSource

---------------------------------------------------------------------------
-- ** Interface
---------------------------------------------------------------------------

data ModuleInfo = ModuleInfo
  { miInterface  :: Interface
  , miWarnings   :: Bool
    -- ^ 'True' if warnings were encountered when the module was type
    -- checked.
  }

-- Note that the use of 'C.TopLevelModuleName' here is a potential
-- performance problem, because these names do not contain unique
-- identifiers.

type VisitedModules = Map C.TopLevelModuleName ModuleInfo
type DecodedModules = Map C.TopLevelModuleName Interface

data Interface = Interface
  { iSourceHash      :: Hash
    -- ^ Hash of the source code.
  , iImportedModules :: [(ModuleName, Hash)]
    -- ^ Imported modules and their hashes.
  , iModuleName      :: ModuleName
    -- ^ Module name of this interface.
  , iScope           :: Map ModuleName Scope
    -- ^ Scope defined by this module.
  , iInsideScope     :: ScopeInfo
    -- ^ Scope after we loaded this interface.
    --   Used in 'Agda.Interaction.BasicOps.AtTopLevel'
    --   and     'Agda.Interaction.CommandLine.interactionLoop'.
    --
    --   Andreas, AIM XX: For performance reason, this field is
    --   not serialized, so if you deserialize an interface, @iInsideScope@
    --   will be empty.  You need to type-check the file to get @iInsideScope@.
  , iSignature       :: Signature
  , iDisplayForms    :: DisplayForms
    -- ^ Display forms added for imported identifiers.
  , iBuiltin         :: BuiltinThings (String, QName)
  , iHaskellImports  :: Set String
                        -- ^ Haskell imports listed in
                        -- (transitively) imported modules are
                        -- not included here.
  , iHaskellImportsUHC :: Set String
                        -- ^ Haskell imports listed in
                        -- (transitively) imported modules are
                        -- not included here.
  , iHaskellCode     :: [String] -- ^ Inline Haskell code
  , iHighlighting    :: HighlightingInfo
  , iPragmaOptions   :: [OptionsPragma]
                        -- ^ Pragma options set in the file.
  , iPatternSyns     :: A.PatternSynDefns
  }
  deriving (Typeable, Show)

instance Pretty Interface where
  pretty (Interface sourceH importedM moduleN scope insideS signature display builtin
                    haskellI haskellIUHC haskellCode highlighting pragmaO patternS) =
    hang (text "Interface") 2 $ vcat
      [ text "source hash:"         <+> (pretty . show) sourceH
      , text "imported modules:"    <+> (pretty . show) importedM
      , text "module name:"         <+> pretty moduleN
      , text "scope:"               <+> (pretty . show) scope
      , text "inside scope:"        <+> (pretty . show) insideS
      , text "signature:"           <+> (pretty . show) signature
      , text "display:"             <+> (pretty . show) display
      , text "builtin:"             <+> (pretty . show) builtin
      , text "Haskell imports:"     <+> (pretty . show) haskellI
      , text "Haskell imports UHC:" <+> (pretty . show) haskellIUHC
      , text "Haskell code:"        <+> (vcat $ map (vcat . map text . lines) $ reverse haskellCode)
      , text "highlighting:"        <+> (pretty . show) highlighting
      , text "pragma options:"      <+> (pretty . show) pragmaO
      , text "pattern syns:"        <+> (pretty . show) patternS
      ]

-- | Combines the source hash and the (full) hashes of the imported modules.
iFullHash :: Interface -> Hash
iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i)

---------------------------------------------------------------------------
-- ** Closure
---------------------------------------------------------------------------

data Closure a = Closure
  { clSignature        :: Signature
  , clEnv              :: TCEnv
  , clScope            :: ScopeInfo
  , clModuleParameters :: ModuleParamDict
      -- ^ Since module parameters are currently stored in 'TCState'
      --   not in 'TCEnv', we save them here.
      --   The map contains for each 'ModuleName' @M@ with module telescope @Γ_M@
      --   a substitution @Γ ⊢ ρ_M : Γ_M@ from the current context @Γ = envContext (clEnv)@.
  , clValue            :: a
  }
    deriving (Typeable, Functor, Foldable)

instance Show a => Show (Closure a) where
  show cl = "Closure " ++ show (clValue cl)

instance HasRange a => HasRange (Closure a) where
    getRange = getRange . clValue

buildClosure :: a -> TCM (Closure a)
buildClosure x = do
    env   <- ask
    sig   <- use stSignature
    scope <- use stScope
    pars  <- use stModuleParameters
    return $ Closure sig env scope pars x

---------------------------------------------------------------------------
-- ** Constraints
---------------------------------------------------------------------------

type Constraints = [ProblemConstraint]

data ProblemConstraint = PConstr
  { constraintProblems :: [ProblemId]
  , theConstraint      :: Closure Constraint
  }
  deriving (Typeable, Show)

instance HasRange ProblemConstraint where
  getRange = getRange . theConstraint

data Constraint
  = ValueCmp Comparison Type Term Term
  | ElimCmp [Polarity] Type Term [Elim] [Elim]
  | TypeCmp Comparison Type Type
  | TelCmp Type Type Comparison Telescope Telescope -- ^ the two types are for the error message only
  | SortCmp Comparison Sort Sort
  | LevelCmp Comparison Level Level
--  | ShortCut MetaId Term Type
--    -- ^ A delayed instantiation.  Replaces @ValueCmp@ in 'postponeTypeCheckingProblem'.
  | UnBlock MetaId
  | Guarded Constraint ProblemId
  | IsEmpty Range Type
    -- ^ The range is the one of the absurd pattern.
  | CheckSizeLtSat Term
    -- ^ Check that the 'Term' is either not a SIZELT or a non-empty SIZELT.
  | FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])
    -- ^ the first argument is the instance argument, the second one is the meta
    --   on which the constraint may be blocked on and the third one is the list
    --   of candidates (or Nothing if we haven’t determined the list of
    --   candidates yet)
  deriving (Typeable, Show)

instance HasRange Constraint where
  getRange (IsEmpty r t) = r
  getRange _ = noRange
{- no Range instances for Term, Type, Elm, Tele, Sort, Level, MetaId
  getRange (ValueCmp cmp a u v) = getRange (a,u,v)
  getRange (ElimCmp pol a v es es') = getRange (a,v,es,es')
  getRange (TypeCmp cmp a b) = getRange (a,b)
  getRange (TelCmp a b cmp tel tel') = getRange (a,b,tel,tel')
  getRange (SortCmp cmp s s') = getRange (s,s')
  getRange (LevelCmp cmp l l') = getRange (l,l')
  getRange (UnBlock x) = getRange x
  getRange (Guarded c pid) = getRange c
  getRange (FindInScope x cands) = getRange x
-}

instance Free' Constraint c where
  freeVars' c =
    case c of
      ValueCmp _ t u v      -> freeVars' (t, (u, v))
      ElimCmp _ t u es es'  -> freeVars' ((t, u), (es, es'))
      TypeCmp _ t t'        -> freeVars' (t, t')
      TelCmp _ _ _ tel tel' -> freeVars' (tel, tel')
      SortCmp _ s s'        -> freeVars' (s, s')
      LevelCmp _ l l'       -> freeVars' (l, l')
      UnBlock _             -> mempty
      Guarded c _           -> freeVars' c
      IsEmpty _ t           -> freeVars' t
      CheckSizeLtSat u      -> freeVars' u
      FindInScope _ _ cs    -> freeVars' cs

instance TermLike Constraint where
  foldTerm f = \case
      ValueCmp _ t u v       -> foldTerm f (t, u, v)
      ElimCmp _ t u es es'   -> foldTerm f (t, u, es, es')
      TypeCmp _ t t'         -> foldTerm f (t, t')
      LevelCmp _ l l'        -> foldTerm f (l, l')
      IsEmpty _ t            -> foldTerm f t
      CheckSizeLtSat u       -> foldTerm f u
      TelCmp _ _ _ tel1 tel2 -> __IMPOSSIBLE__  -- foldTerm f (tel1, tel2) -- Not yet implemented
      SortCmp _ s1 s2        -> __IMPOSSIBLE__  -- foldTerm f (s1, s2) -- Not yet implemented
      UnBlock _              -> __IMPOSSIBLE__  -- mempty     -- Not yet implemented
      Guarded c _            -> __IMPOSSIBLE__  -- foldTerm c -- Not yet implemented
      FindInScope _ _ cs     -> __IMPOSSIBLE__  -- Not yet implemented
  traverseTerm f c  = __IMPOSSIBLE__ -- Not yet implemented
  traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented


data Comparison = CmpEq | CmpLeq
  deriving (Eq, Typeable)

-- TODO: 'Show' should output Haskell-parseable representations.
-- The following instance is deprecated, and Pretty[TCM] should be used
-- instead. Later, simply derive Show for this type.

-- ASR (27 December 2014). This instance is not used anymore (module
-- the test suite) when reporting errors. See Issue 1293.
instance Show Comparison where
  show CmpEq  = "="
  show CmpLeq = "=<"

instance Pretty Comparison where
  pretty CmpEq  = text "="
  pretty CmpLeq = text "=<"

-- | An extension of 'Comparison' to @>=@.
data CompareDirection = DirEq | DirLeq | DirGeq
  deriving (Eq, Typeable)

instance Show CompareDirection where
  show DirEq  = "="
  show DirLeq = "=<"
  show DirGeq = ">="

-- | Embed 'Comparison' into 'CompareDirection'.
fromCmp :: Comparison -> CompareDirection
fromCmp CmpEq  = DirEq
fromCmp CmpLeq = DirLeq

-- | Flip the direction of comparison.
flipCmp :: CompareDirection -> CompareDirection
flipCmp DirEq  = DirEq
flipCmp DirLeq = DirGeq
flipCmp DirGeq = DirLeq

-- | Turn a 'Comparison' function into a 'CompareDirection' function.
--
--   Property: @dirToCmp f (fromCmp cmp) = f cmp@
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp cont DirEq  = cont CmpEq
dirToCmp cont DirLeq = cont CmpLeq
dirToCmp cont DirGeq = flip $ cont CmpLeq

---------------------------------------------------------------------------
-- * Open things
---------------------------------------------------------------------------

-- | A thing tagged with the context it came from.
data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a }
    deriving (Typeable, Show, Functor)

instance Decoration Open where
  traverseF f (OpenThing cxt x) = OpenThing cxt <$> f x

data Local a = Local ModuleName a   -- ^ Local to a given module, the value
                                    -- should have module parameters as free variables.
             | Global a             -- ^ Global value, should be closed.
    deriving (Typeable, Show, Functor, Foldable, Traversable)

isGlobal :: Local a -> Bool
isGlobal Global{} = True
isGlobal Local{}  = False

instance Decoration Local where
  traverseF f (Local m x) = Local m <$> f x
  traverseF f (Global x)  = Global <$> f x

---------------------------------------------------------------------------
-- * Judgements
--
-- Used exclusively for typing of meta variables.
---------------------------------------------------------------------------

-- | Parametrized since it is used without MetaId when creating a new meta.
data Judgement a
  = HasType { jMetaId :: a, jMetaType :: Type }
  | IsSort  { jMetaId :: a, jMetaType :: Type } -- Andreas, 2011-04-26: type needed for higher-order sort metas
  deriving (Typeable)

instance Show a => Show (Judgement a) where
    show (HasType a t) = show a ++ " : " ++ show t
    show (IsSort  a t) = show a ++ " :sort " ++ show t

---------------------------------------------------------------------------
-- ** Meta variables
---------------------------------------------------------------------------

data MetaVariable =
        MetaVar { mvInfo          :: MetaInfo
                , mvPriority      :: MetaPriority -- ^ some metavariables are more eager to be instantiated
                , mvPermutation   :: Permutation
                  -- ^ a metavariable doesn't have to depend on all variables
                  --   in the context, this "permutation" will throw away the
                  --   ones it does not depend on
                , mvJudgement     :: Judgement MetaId
                , mvInstantiation :: MetaInstantiation
                , mvListeners     :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one
                , mvFrozen        :: Frozen -- ^ are we past the point where we can instantiate this meta variable?
                }
    deriving (Typeable)

data Listener = EtaExpand MetaId
              | CheckConstraint Nat ProblemConstraint
  deriving (Typeable)

instance Eq Listener where
  EtaExpand       x   == EtaExpand       y   = x == y
  CheckConstraint x _ == CheckConstraint y _ = x == y
  _ == _ = False

instance Ord Listener where
  EtaExpand       x   `compare` EtaExpand       y   = x `compare` y
  CheckConstraint x _ `compare` CheckConstraint y _ = x `compare` y
  EtaExpand{} `compare` CheckConstraint{} = LT
  CheckConstraint{} `compare` EtaExpand{} = GT

-- | Frozen meta variable cannot be instantiated by unification.
--   This serves to prevent the completion of a definition by its use
--   outside of the current block.
--   (See issues 118, 288, 399).
data Frozen
  = Frozen        -- ^ Do not instantiate.
  | Instantiable
    deriving (Eq, Show)

data MetaInstantiation
        = InstV [Arg String] Term -- ^ solved by term (abstracted over some free variables)
        | Open               -- ^ unsolved
        | OpenIFS            -- ^ open, to be instantiated as "implicit from scope"
        | BlockedConst Term  -- ^ solution blocked by unsolved constraints
        | PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
    deriving (Typeable)

data TypeCheckingProblem
  = CheckExpr A.Expr Type
  | CheckArgs ExpandHidden Range [NamedArg A.Expr] Type Type (Args -> Type -> TCM Term)
  | CheckLambda (Arg ([WithHiding Name], Maybe Type)) A.Expr Type
    -- ^ @(λ (xs : t₀) → e) : t@
    --   This is not an instance of 'CheckExpr' as the domain type
    --   has already been checked.
    --   For example, when checking
    --     @(λ (x y : Fin _) → e) : (x : Fin n) → ?@
    --   we want to postpone @(λ (y : Fin n) → e) : ?@ where @Fin n@
    --   is a 'Type' rather than an 'A.Expr'.
  | UnquoteTactic Term Term Type   -- ^ First argument is computation and the others are hole and goal type
  deriving (Typeable)

instance Show MetaInstantiation where
  show (InstV tel t) = "InstV " ++ show tel ++ " (" ++ show t ++ ")"
  show Open      = "Open"
  show OpenIFS   = "OpenIFS"
  show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")"
  show (PostponedTypeCheckingProblem{}) = "PostponedTypeCheckingProblem (...)"

-- | Meta variable priority:
--   When we have an equation between meta-variables, which one
--   should be instantiated?
--
--   Higher value means higher priority to be instantiated.
newtype MetaPriority = MetaPriority Int
    deriving (Eq, Ord, Show)

data RunMetaOccursCheck
  = RunMetaOccursCheck
  | DontRunMetaOccursCheck
  deriving (Eq, Ord, Show)

-- | @MetaInfo@ is cloned from one meta to the next during pruning.
data MetaInfo = MetaInfo
  { miClosRange       :: Closure Range -- TODO: Not so nice. But we want both to have the environment of the meta (Closure) and its range.
--  , miRelevance       :: Relevance          -- ^ Created in irrelevant position?
  , miMetaOccursCheck :: RunMetaOccursCheck -- ^ Run the extended occurs check that goes in definitions?
  , miNameSuggestion  :: MetaNameSuggestion
    -- ^ Used for printing.
    --   @Just x@ if meta-variable comes from omitted argument with name @x@.
  }

-- | Name suggestion for meta variable.  Empty string means no suggestion.
type MetaNameSuggestion = String

-- | For printing, we couple a meta with its name suggestion.
data NamedMeta = NamedMeta
  { nmSuggestion :: MetaNameSuggestion
  , nmid         :: MetaId
  }

instance Pretty NamedMeta where
  pretty (NamedMeta "" x) = pretty x
  pretty (NamedMeta s  x) = text $ "_" ++ s ++ prettyShow x

type MetaStore = Map MetaId MetaVariable

instance HasRange MetaInfo where
  getRange = clValue . miClosRange

instance HasRange MetaVariable where
    getRange m = getRange $ getMetaInfo m

instance SetRange MetaInfo where
  setRange r m = m { miClosRange = (miClosRange m) { clValue = r }}

instance SetRange MetaVariable where
  setRange r m = m { mvInfo = setRange r (mvInfo m) }

normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0

lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (-10)

highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10

getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = miClosRange . mvInfo

getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope m = clScope $ getMetaInfo m

getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv m = clEnv $ getMetaInfo m

getMetaSig :: MetaVariable -> Signature
getMetaSig m = clSignature $ getMetaInfo m

getMetaRelevance :: MetaVariable -> Relevance
getMetaRelevance = envRelevance . getMetaEnv

---------------------------------------------------------------------------
-- ** Interaction meta variables
---------------------------------------------------------------------------

-- | Interaction points are created by the scope checker who sets the range.
--   The meta variable is created by the type checker and then hooked up to the
--   interaction point.
data InteractionPoint = InteractionPoint
  { ipRange :: Range        -- ^ The position of the interaction point.
  , ipMeta  :: Maybe MetaId -- ^ The meta variable, if any, holding the type etc.
  , ipClause:: IPClause
      -- ^ The clause of the interaction point (if any).
      --   Used for case splitting.
  }

instance Eq InteractionPoint where (==) = (==) `on` ipMeta

-- | Data structure managing the interaction points.
type InteractionPoints = Map InteractionId InteractionPoint

-- | Which clause is an interaction point located in?
data IPClause = IPClause
  { ipcQName    :: QName  -- ^ The name of the function.
  , ipcClauseNo :: Int    -- ^ The number of the clause of this function.
  , ipcClause   :: A.RHS  -- ^ The original AST clause rhs.
  }
  | IPNoClause -- ^ The interaction point is not in the rhs of a clause.

instance Eq IPClause where
  IPNoClause     == IPNoClause       = True
  IPClause x i _ == IPClause x' i' _ = x == x' && i == i'
  _              == _                = False

---------------------------------------------------------------------------
-- ** Signature
---------------------------------------------------------------------------

data Signature = Sig
      { _sigSections    :: Sections
      , _sigDefinitions :: Definitions
      , _sigRewriteRules:: RewriteRuleMap  -- ^ The rewrite rules defined in this file.
      }
  deriving (Typeable, Show)

sigSections :: Lens' Sections Signature
sigSections f s =
  f (_sigSections s) <&>
  \x -> s {_sigSections = x}

sigDefinitions :: Lens' Definitions Signature
sigDefinitions f s =
  f (_sigDefinitions s) <&>
  \x -> s {_sigDefinitions = x}

sigRewriteRules :: Lens' RewriteRuleMap Signature
sigRewriteRules f s =
  f (_sigRewriteRules s) <&>
  \x -> s {_sigRewriteRules = x}

type Sections    = Map ModuleName Section
type Definitions = HashMap QName Definition
type RewriteRuleMap = HashMap QName RewriteRules
type DisplayForms = HashMap QName [LocalDisplayForm]

data Section = Section { _secTelescope :: Telescope }
  deriving (Typeable, Show)

secTelescope :: Lens' Telescope Section
secTelescope f s =
  f (_secTelescope s) <&>
  \x -> s {_secTelescope = x}

emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty HMap.empty

-- | A @DisplayForm@ is in essence a rewrite rule
--   @
--      q ts --> dt
--   @
--   for a defined symbol (could be a constructor as well) @q@.
--   The right hand side is a 'DisplayTerm' which is used to
--   'reify' to a more readable 'Abstract.Syntax'.
--
--   The patterns @ts@ are just terms, but @var 0@ is interpreted
--   as a hole.  Each occurrence of @var 0@ is a new hole (pattern var).
--   For each *occurrence* of @var0@ the rhs @dt@ has a free variable.
--   These are instantiated when matching a display form against a
--   term @q vs@ succeeds.
data DisplayForm = Display
  { dfFreeVars :: Nat
    -- ^ Number @n@ of free variables in 'dfRHS'.
  , dfPats     :: Elims
    -- ^ Left hand side patterns, where @var 0@ stands for a pattern
    --   variable.  There should be @n@ occurrences of @var0@ in
    --   'dfPats'.
    --   The 'ArgInfo' is ignored in these patterns.
  , dfRHS      :: DisplayTerm
    -- ^ Right hand side, with @n@ free variables.
  }
  deriving (Typeable, Show)

type LocalDisplayForm = Local DisplayForm

-- | A structured presentation of a 'Term' for reification into
--   'Abstract.Syntax'.
data DisplayTerm
  = DWithApp DisplayTerm [DisplayTerm] Elims
    -- ^ @(f vs | ws) es@.
    --   The first 'DisplayTerm' is the parent function @f@ with its args @vs@.
    --   The list of 'DisplayTerm's are the with expressions @ws@.
    --   The 'Elims' are additional arguments @es@
    --   (possible in case the with-application is of function type)
    --   or projections (if it is of record type).
  | DCon ConHead ConInfo [Arg DisplayTerm]
    -- ^ @c vs@.
  | DDef QName [Elim' DisplayTerm]
    -- ^ @d vs@.
  | DDot Term
    -- ^ @.v@.
  | DTerm Term
    -- ^ @v@.
  deriving (Typeable, Show)

instance Free' DisplayForm c where
  freeVars' (Display n ps t) = bind (freeVars' ps) `mappend` bind' n (freeVars' t)

instance Free' DisplayTerm c where
  freeVars' (DWithApp t ws es) = freeVars' (t, (ws, es))
  freeVars' (DCon _ _ vs)      = freeVars' vs
  freeVars' (DDef _ es)        = freeVars' es
  freeVars' (DDot v)           = freeVars' v
  freeVars' (DTerm v)          = freeVars' v

-- | By default, we have no display form.
defaultDisplayForm :: QName -> [LocalDisplayForm]
defaultDisplayForm c = []

defRelevance :: Definition -> Relevance
defRelevance = argInfoRelevance . defArgInfo

-- | Non-linear (non-constructor) first-order pattern.
data NLPat
  = PVar (Maybe CtxId) !Int [Arg Int]
    -- ^ Matches anything (modulo non-linearity) that only contains bound
    --   variables that occur in the given arguments.
  | PWild
    -- ^ Matches anything (e.g. irrelevant terms).
  | PDef QName PElims
    -- ^ Matches @f es@
  | PLam ArgInfo (Abs NLPat)
    -- ^ Matches @λ x → t@
  | PPi (Dom NLPType) (Abs NLPType)
    -- ^ Matches @(x : A) → B@
  | PBoundVar {-# UNPACK #-} !Int PElims
    -- ^ Matches @x es@ where x is a lambda-bound variable
  | PTerm Term
    -- ^ Matches the term modulo β (ideally βη).
  deriving (Typeable, Show)
type PElims = [Elim' NLPat]

data NLPType = NLPType
  { nlpTypeLevel :: NLPat  -- always PWild or PVar (with all bound variables in scope)
  , nlpTypeUnEl  :: NLPat
  } deriving (Typeable, Show)

type RewriteRules = [RewriteRule]

-- | Rewrite rules can be added independently from function clauses.
data RewriteRule = RewriteRule
  { rewName    :: QName      -- ^ Name of rewrite rule @q : Γ → f ps ≡ rhs@
                             --   where @≡@ is the rewrite relation.
  , rewContext :: Telescope  -- ^ @Γ@.
  , rewHead    :: QName      -- ^ @f@.
  , rewPats    :: PElims     -- ^ @Γ ⊢ ps  : t@.
  , rewRHS     :: Term       -- ^ @Γ ⊢ rhs : t@.
  , rewType    :: Type       -- ^ @Γ ⊢ t@.
  }
    deriving (Typeable, Show)

data Definition = Defn
  { defArgInfo        :: ArgInfo -- ^ Hiding should not be used.
  , defName           :: QName
  , defType           :: Type    -- ^ Type of the lifted definition.
  , defPolarity       :: [Polarity]
    -- ^ Variance information on arguments of the definition.
    --   Does not include info for dropped parameters to
    --   projection(-like) functions and constructors.
  , defArgOccurrences :: [Occurrence]
    -- ^ Positivity information on arguments of the definition.
    --   Does not include info for dropped parameters to
    --   projection(-like) functions and constructors.

    --   Sometimes Agda looks up 'Occurrence's in these lists based on
    --   their position, so one might consider replacing the list
    --   with, say, an 'IntMap'. However, presumably these lists tend
    --   to be short, in which case 'IntMap's could be slower than
    --   lists. For instance, at one point the longest list
    --   encountered for the standard library (in serialised
    --   interfaces) had length 27. Distribution:
    --
    --   Length, number of lists
    --   -----------------------
    --
    --    0, 2444
    --    1,  721
    --    2,  433
    --    3,  668
    --    4,  602
    --    5,  624
    --    6,  626
    --    7,  484
    --    8,  375
    --    9,  264
    --   10,  305
    --   11,  188
    --   12,  171
    --   13,  108
    --   14,   84
    --   15,   80
    --   16,   38
    --   17,   23
    --   18,   16
    --   19,    8
    --   20,    7
    --   21,    5
    --   22,    2
    --   23,    3
    --   27,    1

  , defDisplay        :: [LocalDisplayForm]
  , defMutual         :: MutualId
  , defCompiledRep    :: CompiledRepresentation
  , defInstance       :: Maybe QName
    -- ^ @Just q@ when this definition is an instance of class q
  , defCopy           :: Bool
    -- ^ Has this function been created by a module
                         -- instantiation?
  , defMatchable      :: Bool
    -- ^ Is the def matched against in a rewrite rule?
  , theDef            :: Defn
  }
    deriving (Typeable, Show)

theDefLens :: Lens' Defn Definition
theDefLens f d = f (theDef d) <&> \ df -> d { theDef = df }

-- | Create a definition with sensible defaults.
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn info x t def = Defn
  { defArgInfo        = info
  , defName           = x
  , defType           = t
  , defPolarity       = []
  , defArgOccurrences = []
  , defDisplay        = defaultDisplayForm x
  , defMutual         = 0
  , defCompiledRep    = noCompiledRep
  , defInstance       = Nothing
  , defCopy           = False
  , defMatchable      = False
  , theDef            = def
  }

type HaskellCode = String
type HaskellType = String
type EpicCode    = String
type JSCode      = String

data HaskellRepresentation
      = HsDefn HaskellType HaskellCode
      | HsType HaskellType
  deriving (Typeable, Show)

data HaskellExport = HsExport HaskellType String deriving (Show, Typeable)

data CoreRepresentation
      = CrDefn CR.CoreExpr -- ^ Core code for functions.
      | CrType CR.CoreType -- ^ Core type for agda type.
      | CrConstr CR.CoreConstr  -- ^ Core constructor for agda constructor.
    deriving (Typeable, Show)

-- | Polarity for equality and subtype checking.
data Polarity
  = Covariant      -- ^ monotone
  | Contravariant  -- ^ antitone
  | Invariant      -- ^ no information (mixed variance)
  | Nonvariant     -- ^ constant
  deriving (Typeable, Show, Eq)

data CompiledRepresentation = CompiledRep
  { compiledHaskell :: Maybe HaskellRepresentation
  , exportHaskell   :: Maybe HaskellExport
  , compiledEpic    :: Maybe EpicCode
  , compiledJS      :: Maybe JSCode
  , compiledCore    :: Maybe CoreRepresentation
  }
  deriving (Typeable, Show)

noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing Nothing Nothing

-- | Additional information for extended lambdas.
data ExtLamInfo = ExtLamInfo
  { extLamNumHidden :: Int  -- Number of hidden args to be dropped when printing.
  , extLamNumNonHid :: Int  -- Number of visible args to be dropped when printing.
  } deriving (Typeable, Eq, Ord, Show)

-- | Additional information for projection 'Function's.
data Projection = Projection
  { projProper    :: Bool
    -- ^ @False@ if only projection-like, @True@ if record projection.
  , projOrig      :: QName
    -- ^ The original projection name
    --   (current name could be from module application).
  , projFromType  :: Arg QName
    -- ^ Type projected from. Record type if @projProper = Just{}@. Also
    -- stores @ArgInfo@ of the principal argument.
  , projIndex     :: Int
    -- ^ Index of the record argument.
    --   Start counting with 1, because 0 means that
    --   it is already applied to the record value.
    --   This can happen in module instantiation, but
    --   then either the record value is @var 0@, or @funProjection == Nothing@.
  , projLams :: ProjLams
    -- ^ Term @t@ to be be applied to record parameters and record value.
    --   The parameters will be dropped.
    --   In case of a proper projection, a postfix projection application
    --   will be created: @t = \ pars r -> r .p@
    --   (Invariant: the number of abstractions equals 'projIndex'.)
    --   In case of a projection-like function, just the function symbol
    --   is returned as 'Def':  @t = \ pars -> f@.
  } deriving (Typeable, Show)

-- | Abstractions to build projection function (dropping parameters).
newtype ProjLams = ProjLams { getProjLams :: [Arg ArgName] }
  deriving (Typeable, Show, Null)

-- | Building the projection function (which drops the parameters).
projDropPars :: Projection -> ProjOrigin -> Term
-- Proper projections:
projDropPars (Projection True d _ _ lams) o =
  case initLast $ getProjLams lams of
    Nothing -> Def d []
    Just (pars, Arg i y) ->
      let core = Lam i $ Abs y $ Var 0 [Proj o d] in
      List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) core pars
-- Projection-like functions:
projDropPars (Projection False _ _ _ lams) o | null lams = __IMPOSSIBLE__
projDropPars (Projection False d _ _ lams) o =
  List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (Def d []) $ init $ getProjLams lams

-- | The info of the principal (record) argument.
projArgInfo :: Projection -> ArgInfo
projArgInfo (Projection _ _ _ _ lams) =
  maybe __IMPOSSIBLE__ getArgInfo $ lastMaybe $ getProjLams lams

-- | Should a record type admit eta-equality?
data EtaEquality
  = Specified !Bool  -- ^ User specifed 'eta-equality' or 'no-eta-equality'
  | Inferred !Bool   -- ^ Positivity checker inferred whether eta is safe/
  deriving (Typeable, Show, Eq)

etaEqualityToBool :: EtaEquality -> Bool
etaEqualityToBool (Specified b) = b
etaEqualityToBool (Inferred b) = b

-- | Make sure we do not overwrite a user specification.
setEtaEquality :: EtaEquality -> Bool -> EtaEquality
setEtaEquality e@Specified{} _ = e
setEtaEquality _ b = Inferred b

data FunctionFlag
  = FunStatic  -- ^ Should calls to this function be normalised at compile-time?
  | FunInline  -- ^ Should calls to this function be inlined by the compiler?
  | FunMacro   -- ^ Is this function a macro?
  deriving (Typeable, Eq, Ord, Enum, Show)

data Defn = Axiom
            -- ^ Postulate.
          | AbstractDefn
            -- ^ Returned by 'getConstInfo' if definition is abstract.
          | Function
            { funClauses        :: [Clause]
            , funCompiled       :: Maybe CompiledClauses
              -- ^ 'Nothing' while function is still type-checked.
              --   @Just cc@ after type and coverage checking and
              --   translation to case trees.
            , funTreeless       :: Maybe Compiled
              -- ^ Intermediate representation for compiler backends.
            , funInv            :: FunctionInverse
            , funMutual         :: [QName]
              -- ^ Mutually recursive functions, @data@s and @record@s.
              --   Does not include this function.
            , funAbstr          :: IsAbstract
            , funDelayed        :: Delayed
              -- ^ Are the clauses of this definition delayed?
            , funProjection     :: Maybe Projection
              -- ^ Is it a record projection?
              --   If yes, then return the name of the record type and index of
              --   the record argument.  Start counting with 1, because 0 means that
              --   it is already applied to the record. (Can happen in module
              --   instantiation.) This information is used in the termination
              --   checker.
            , funFlags          :: Set FunctionFlag
            , funTerminates     :: Maybe Bool
              -- ^ Has this function been termination checked?  Did it pass?
            , funExtLam         :: Maybe ExtLamInfo
              -- ^ Is this function generated from an extended lambda?
              --   If yes, then return the number of hidden and non-hidden lambda-lifted arguments
            , funWith           :: Maybe QName
              -- ^ Is this a generated with-function? If yes, then what's the
              --   name of the parent function.
            , funCopatternLHS   :: Bool
              -- ^ Is this a function defined by copatterns?
            }
          | Datatype
            { dataPars           :: Nat            -- ^ Number of parameters.
            , dataSmallPars      :: Permutation    -- ^ Parameters that are maybe small.
            , dataNonLinPars     :: Drop Permutation  -- ^ Parameters that appear in indices.
            , dataIxs            :: Nat            -- ^ Number of indices.
            , dataInduction      :: Induction      -- ^ @data@ or @codata@ (legacy).
            , dataClause         :: (Maybe Clause) -- ^ This might be in an instantiated module.
            , dataCons           :: [QName]        -- ^ Constructor names.
            , dataSort           :: Sort
            , dataMutual         :: [QName]        -- ^ Mutually recursive functions, @data@s and @record@s.  Does not include this data type.
            , dataAbstr          :: IsAbstract
            }
          | Record
            { recPars           :: Nat                  -- ^ Number of parameters.
            , recClause         :: Maybe Clause
            , recConHead        :: ConHead              -- ^ Constructor name and fields.
            , recNamedCon       :: Bool
            , recFields         :: [Arg QName]
            , recTel            :: Telescope            -- ^ The record field telescope. (Includes record parameters.)
                                                        --   Note: @TelV recTel _ == telView' recConType@.
                                                        --   Thus, @recTel@ is redundant.
            , recMutual         :: [QName]              -- ^ Mutually recursive functions, @data@s and @record@s.  Does not include this record.
            , recEtaEquality'    :: EtaEquality          -- ^ Eta-expand at this record type.  @False@ for unguarded recursive records and coinductive records unless the user specifies otherwise.
            , recInduction      :: Maybe Induction
              -- ^ 'Inductive' or 'CoInductive'?  Matters only for recursive records.
              --   'Nothing' means that the user did not specify it, which is an error
              --   for recursive records.
            , recRecursive      :: Bool                 -- ^ Recursive record.  Infers @recEtaEquality = False@.  Projections are not size-preserving.
            , recAbstr          :: IsAbstract
            }
          | Constructor
            { conPars   :: Nat         -- ^ Number of parameters.
            , conSrcCon :: ConHead     -- ^ Name of (original) constructor and fields. (This might be in a module instance.)
            , conData   :: QName       -- ^ Name of datatype or record type.
            , conAbstr  :: IsAbstract
            , conInd    :: Induction   -- ^ Inductive or coinductive?
            , conErased :: [Bool]      -- ^ Which arguments are erased at runtime (computed during compilation to treeless)
            }
          | Primitive
            { primAbstr :: IsAbstract
            , primName  :: String
            , primClauses :: [Clause]
              -- ^ 'null' for primitive functions, @not null@ for builtin functions.
            , primCompiled :: Maybe CompiledClauses
              -- ^ 'Nothing' for primitive functions,
              --   @'Just' something@ for builtin functions.
            }
            -- ^ Primitive or builtin functions.
    deriving (Typeable, Show)

recEtaEquality :: Defn -> Bool
recEtaEquality = etaEqualityToBool . recEtaEquality'

-- | A template for creating 'Function' definitions, with sensible defaults.
emptyFunction :: Defn
emptyFunction = Function
  { funClauses     = []
  , funCompiled    = Nothing
  , funTreeless    = Nothing
  , funInv         = NotInjective
  , funMutual      = []
  , funAbstr       = ConcreteDef
  , funDelayed     = NotDelayed
  , funProjection  = Nothing
  , funFlags       = Set.empty
  , funTerminates  = Nothing
  , funExtLam      = Nothing
  , funWith        = Nothing
  , funCopatternLHS = False
  }

funFlag :: FunctionFlag -> Lens' Bool Defn
funFlag flag f def@Function{ funFlags = flags } =
  f (Set.member flag flags) <&>
  \ b -> def{ funFlags = (if b then Set.insert else Set.delete) flag flags }
funFlag _ f def = f False <&> const def

funStatic, funInline, funMacro :: Lens' Bool Defn
funStatic       = funFlag FunStatic
funInline       = funFlag FunInline
funMacro        = funFlag FunMacro

isMacro :: Defn -> Bool
isMacro = (^. funMacro)

-- | Checking whether we are dealing with a function yet to be defined.
isEmptyFunction :: Defn -> Bool
isEmptyFunction def =
  case def of
    Function { funClauses = [] } -> True
    _ -> False

isCopatternLHS :: [Clause] -> Bool
isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats)

recCon :: Defn -> QName
recCon Record{ recConHead } = conName recConHead
recCon _ = __IMPOSSIBLE__

defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _        = False

defIsDataOrRecord :: Defn -> Bool
defIsDataOrRecord Record{}   = True
defIsDataOrRecord Datatype{} = True
defIsDataOrRecord _          = False

newtype Fields = Fields [(C.Name, Type)]
  deriving (Typeable, Null)

-- | Did we encounter a simplifying reduction?
--   In terms of CIC, that would be a iota-reduction.
--   In terms of Agda, this is a constructor or literal
--   pattern that matched.
--   Just beta-reduction (substitution) or delta-reduction
--   (unfolding of definitions) does not count as simplifying?

data Simplification = YesSimplification | NoSimplification
  deriving (Typeable, Eq, Show)

instance Null Simplification where
  empty = NoSimplification
  null  = (== NoSimplification)

instance Semigroup Simplification where
  YesSimplification <> _ = YesSimplification
  NoSimplification  <> s = s

instance Monoid Simplification where
  mempty = NoSimplification
  mappend = (<>)

data Reduced no yes = NoReduction no | YesReduction Simplification yes
    deriving (Typeable, Functor)

-- | Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.
data IsReduced
  = NotReduced
  | Reduced    (Blocked ())

data MaybeReduced a = MaybeRed
  { isReduced     :: IsReduced
  , ignoreReduced :: a
  }
  deriving (Functor)

instance IsProjElim e => IsProjElim (MaybeReduced e) where
  isProjElim = isProjElim . ignoreReduced

type MaybeReducedArgs = [MaybeReduced (Arg Term)]
type MaybeReducedElims = [MaybeReduced Elim]

notReduced :: a -> MaybeReduced a
notReduced x = MaybeRed NotReduced x

reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced b = case fmap ignoreSharing <$> b of
  NotBlocked _ (Arg _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
  _                                -> MaybeRed (Reduced $ () <$ b)      v
  where
    v = ignoreBlocking b

-- | Controlling 'reduce'.
data AllowedReduction
  = ProjectionReductions     -- ^ (Projection and) projection-like functions may be reduced.
  | InlineReductions         -- ^ Functions marked INLINE may be reduced.
  | CopatternReductions      -- ^ Copattern definitions may be reduced.
  | FunctionReductions       -- ^ Functions which are not projections may be reduced.
  | LevelReductions          -- ^ Reduce @'Level'@ terms.
  | NonTerminatingReductions -- ^ Functions that have not passed termination checking.
  deriving (Show, Eq, Ord, Enum, Bounded)

type AllowedReductions = [AllowedReduction]

-- | Not quite all reductions (skip non-terminating reductions)
allReductions :: AllowedReductions
allReductions = [minBound..pred maxBound]

data PrimFun = PrimFun
        { primFunName           :: QName
        , primFunArity          :: Arity
        , primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
        }
    deriving (Typeable)

defClauses :: Definition -> [Clause]
defClauses Defn{theDef = Function{funClauses = cs}}        = cs
defClauses Defn{theDef = Primitive{primClauses = cs}}      = cs
defClauses Defn{theDef = Datatype{dataClause = Just c}}    = [c]
defClauses Defn{theDef = Record{recClause = Just c}}       = [c]
defClauses _                                               = []

defCompiled :: Definition -> Maybe CompiledClauses
defCompiled Defn{theDef = Function {funCompiled  = mcc}} = mcc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing

defParameters :: Definition -> Maybe Nat
defParameters Defn{theDef = Datatype{dataPars = n}} = Just n
defParameters Defn{theDef = Record  {recPars  = n}} = Just n
defParameters _                                     = Nothing

defJSDef :: Definition -> Maybe JSCode
defJSDef = compiledJS . defCompiledRep

defEpicDef :: Definition -> Maybe EpicCode
defEpicDef = compiledEpic . defCompiledRep

defCoreDef :: Definition -> Maybe CoreRepresentation
defCoreDef = compiledCore . defCompiledRep

-- | Are the clauses of this definition delayed?
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _                                       = NotDelayed

-- | Has the definition failed the termination checker?
defNonterminating :: Definition -> Bool
defNonterminating Defn{theDef = Function{funTerminates = Just False}} = True
defNonterminating _                                                   = False

defAbstract :: Definition -> IsAbstract
defAbstract d = case theDef d of
    Axiom{}                   -> ConcreteDef
    AbstractDefn{}            -> AbstractDef
    Function{funAbstr = a}    -> a
    Datatype{dataAbstr = a}   -> a
    Record{recAbstr = a}      -> a
    Constructor{conAbstr = a} -> a
    Primitive{primAbstr = a}  -> a

---------------------------------------------------------------------------
-- ** Injectivity
---------------------------------------------------------------------------

type FunctionInverse = FunctionInverse' Clause

data FunctionInverse' c
  = NotInjective
  | Inverse (Map TermHead c)
  deriving (Typeable, Show, Functor)

data TermHead = SortHead
              | PiHead
              | ConsHead QName
  deriving (Typeable, Eq, Ord, Show)

---------------------------------------------------------------------------
-- ** Mutual blocks
---------------------------------------------------------------------------

newtype MutualId = MutId Int32
  deriving (Typeable, Eq, Ord, Show, Num, Enum)

---------------------------------------------------------------------------
-- ** Statistics
---------------------------------------------------------------------------

type Statistics = Map String Integer

---------------------------------------------------------------------------
-- ** Trace
---------------------------------------------------------------------------

data Call = CheckClause Type A.SpineClause
          | CheckPattern A.Pattern Telescope Type
          | CheckLetBinding A.LetBinding
          | InferExpr A.Expr
          | CheckExprCall A.Expr Type
          | CheckDotPattern A.Expr Term
          | CheckPatternShadowing A.SpineClause
          | CheckProjection Range QName Type
          | IsTypeCall A.Expr Sort
          | IsType_ A.Expr
          | InferVar Name
          | InferDef QName
          | CheckArguments Range [NamedArg A.Expr] Type Type
          | CheckDataDef Range Name [A.LamBinding] [A.Constructor]
          | CheckRecDef Range Name [A.LamBinding] [A.Constructor]
          | CheckConstructor QName Telescope Sort A.Constructor
          | CheckFunDef Range Name [A.Clause]
          | CheckPragma Range A.Pragma
          | CheckPrimitive Range Name A.Expr
          | CheckIsEmpty Range Type
          | CheckWithFunctionType A.Expr
          | CheckSectionApplication Range ModuleName A.ModuleApplication
          | ScopeCheckExpr C.Expr
          | ScopeCheckDeclaration D.NiceDeclaration
          | ScopeCheckLHS C.QName C.Pattern
          | NoHighlighting
          | ModuleContents  -- ^ Interaction command: show module contents.
          | SetRange Range  -- ^ used by 'setCurrentRange'
    deriving (Typeable)

instance Pretty Call where
    pretty CheckClause{}             = text "CheckClause"
    pretty CheckPattern{}            = text "CheckPattern"
    pretty InferExpr{}               = text "InferExpr"
    pretty CheckExprCall{}           = text "CheckExprCall"
    pretty CheckLetBinding{}         = text "CheckLetBinding"
    pretty CheckProjection{}         = text "CheckProjection"
    pretty IsTypeCall{}              = text "IsTypeCall"
    pretty IsType_{}                 = text "IsType_"
    pretty InferVar{}                = text "InferVar"
    pretty InferDef{}                = text "InferDef"
    pretty CheckArguments{}          = text "CheckArguments"
    pretty CheckDataDef{}            = text "CheckDataDef"
    pretty CheckRecDef{}             = text "CheckRecDef"
    pretty CheckConstructor{}        = text "CheckConstructor"
    pretty CheckFunDef{}             = text "CheckFunDef"
    pretty CheckPragma{}             = text "CheckPragma"
    pretty CheckPrimitive{}          = text "CheckPrimitive"
    pretty CheckWithFunctionType{}   = text "CheckWithFunctionType"
    pretty ScopeCheckExpr{}          = text "ScopeCheckExpr"
    pretty ScopeCheckDeclaration{}   = text "ScopeCheckDeclaration"
    pretty ScopeCheckLHS{}           = text "ScopeCheckLHS"
    pretty CheckDotPattern{}         = text "CheckDotPattern"
    pretty CheckPatternShadowing{}   = text "CheckPatternShadowing"
    pretty SetRange{}                = text "SetRange"
    pretty CheckSectionApplication{} = text "CheckSectionApplication"
    pretty CheckIsEmpty{}            = text "CheckIsEmpty"
    pretty NoHighlighting{}          = text "NoHighlighting"
    pretty ModuleContents{}          = text "ModuleContents"

instance HasRange Call where
    getRange (CheckClause _ c)               = getRange c
    getRange (CheckPattern p _ _)            = getRange p
    getRange (InferExpr e)                   = getRange e
    getRange (CheckExprCall e _)             = getRange e
    getRange (CheckLetBinding b)             = getRange b
    getRange (CheckProjection r _ _)         = r
    getRange (IsTypeCall e s)                = getRange e
    getRange (IsType_ e)                     = getRange e
    getRange (InferVar x)                    = getRange x
    getRange (InferDef f)                    = getRange f
    getRange (CheckArguments r _ _ _)        = r
    getRange (CheckDataDef i _ _ _)          = getRange i
    getRange (CheckRecDef i _ _ _)           = getRange i
    getRange (CheckConstructor _ _ _ c)      = getRange c
    getRange (CheckFunDef i _ _)             = getRange i
    getRange (CheckPragma r _)               = r
    getRange (CheckPrimitive i _ _)          = getRange i
    getRange CheckWithFunctionType{}         = noRange
    getRange (ScopeCheckExpr e)              = getRange e
    getRange (ScopeCheckDeclaration d)       = getRange d
    getRange (ScopeCheckLHS _ p)             = getRange p
    getRange (CheckDotPattern e _)           = getRange e
    getRange (CheckPatternShadowing c)       = getRange c
    getRange (SetRange r)                    = r
    getRange (CheckSectionApplication r _ _) = r
    getRange (CheckIsEmpty r _)              = r
    getRange NoHighlighting                  = noRange
    getRange ModuleContents                  = noRange

---------------------------------------------------------------------------
-- ** Instance table
---------------------------------------------------------------------------

-- | The instance table is a @Map@ associating to every name of
--   record/data type/postulate its list of instances
type InstanceTable = Map QName (Set QName)

-- | When typechecking something of the following form:
--
--     instance
--       x : _
--       x = y
--
--   it's not yet known where to add @x@, so we add it to a list of
--   unresolved instances and we'll deal with it later.
type TempInstanceTable = (InstanceTable , Set QName)

---------------------------------------------------------------------------
-- ** Builtin things
---------------------------------------------------------------------------

data BuiltinDescriptor
  = BuiltinData (TCM Type) [String]
  | BuiltinDataCons (TCM Type)
  | BuiltinPrim String (Term -> TCM ())
  | BuiltinPostulate Relevance (TCM Type)
  | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
    -- ^ Builtin of any kind.
    --   Type can be checked (@Just t@) or inferred (@Nothing@).
    --   The second argument is the hook for the verification function.

data BuiltinInfo =
   BuiltinInfo { builtinName :: String
               , builtinDesc :: BuiltinDescriptor }

type BuiltinThings pf = Map String (Builtin pf)

data Builtin pf
        = Builtin Term
        | Prim pf
    deriving (Typeable, Show, Functor, Foldable, Traversable)

---------------------------------------------------------------------------
-- * Highlighting levels
---------------------------------------------------------------------------

-- | How much highlighting should be sent to the user interface?

data HighlightingLevel
  = None
  | NonInteractive
  | Interactive
    -- ^ This includes both non-interactive highlighting and
    -- interactive highlighting of the expression that is currently
    -- being type-checked.
    deriving (Eq, Ord, Show, Read)

-- | How should highlighting be sent to the user interface?

data HighlightingMethod
  = Direct
    -- ^ Via stdout.
  | Indirect
    -- ^ Both via files and via stdout.
    deriving (Eq, Show, Read)

-- | @ifTopLevelAndHighlightingLevelIs l m@ runs @m@ when we're
-- type-checking the top-level module and the highlighting level is
-- /at least/ @l@.

ifTopLevelAndHighlightingLevelIs ::
  MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l m = do
  e <- ask
  when (envModuleNestingLevel e == 0 &&
        envHighlightingLevel e >= l)
       m

---------------------------------------------------------------------------
-- * Type checking environment
---------------------------------------------------------------------------

data ModuleParameters = ModuleParams
  { mpSubstitution :: Substitution
      -- ^ @Δ ⊢ σ : Γ@ for a @module M Γ@ where @Δ@ is the current context @envContext@.
  } deriving (Typeable, Show)

defaultModuleParameters :: ModuleParameters
defaultModuleParameters = ModuleParams IdS

type ModuleParamDict = Map ModuleName ModuleParameters
  -- ^ The map contains for each 'ModuleName' @M@ with module telescope @Γ_M@
  --   a substitution @Γ ⊢ ρ_M : Γ_M@ from the current context @Γ = envContext (clEnv)@.

data TCEnv =
    TCEnv { envContext             :: Context
          , envLetBindings         :: LetBindings
          , envCurrentModule       :: ModuleName
          , envCurrentPath         :: Maybe AbsolutePath
            -- ^ The path to the file that is currently being
            -- type-checked.  'Nothing' if we do not have a file
            -- (like in interactive mode see @CommandLine@).
          , envAnonymousModules    :: [(ModuleName, Nat)] -- ^ anonymous modules and their number of free variables
          , envImportPath          :: [C.TopLevelModuleName] -- ^ to detect import cycles
          , envMutualBlock         :: Maybe MutualId -- ^ the current (if any) mutual block
          , envTerminationCheck    :: TerminationCheck ()  -- ^ are we inside the scope of a termination pragma
          , envSolvingConstraints  :: Bool
                -- ^ Are we currently in the process of solving active constraints?
          , envCheckingWhere       :: Bool
                -- ^ Have we stepped into the where-declarations of a clause?
                --   Everything under a @where@ will be checked with this flag on.
          , envAssignMetas         :: Bool
            -- ^ Are we allowed to assign metas?
          , envActiveProblems      :: [ProblemId]
          , envAbstractMode        :: AbstractMode
                -- ^ When checking the typesignature of a public definition
                --   or the body of a non-abstract definition this is true.
                --   To prevent information about abstract things leaking
                --   outside the module.
          , envRelevance           :: Relevance
                -- ^ Are we checking an irrelevant argument? (=@Irrelevant@)
                -- Then top-level irrelevant declarations are enabled.
                -- Other value: @Relevant@, then only relevant decls. are avail.
          , envDisplayFormsEnabled :: Bool
                -- ^ Sometimes we want to disable display forms.
          , envRange :: Range
          , envHighlightingRange :: Range
                -- ^ Interactive highlighting uses this range rather
                --   than 'envRange'.
          , envClause :: IPClause
                -- ^ What is the current clause we are type-checking?
                --   Will be recorded in interaction points in this clause.
          , envCall  :: Maybe (Closure Call)
                -- ^ what we're doing at the moment
          , envHighlightingLevel  :: HighlightingLevel
                -- ^ Set to 'None' when imported modules are
                --   type-checked.
          , envHighlightingMethod :: HighlightingMethod
          , envModuleNestingLevel :: !Int
                -- ^ This number indicates how far away from the
                --   top-level module Agda has come when chasing
                --   modules. The level of a given module is not
                --   necessarily the same as the length, in the module
                --   dependency graph, of the shortest path from the
                --   top-level module; it depends on in which order
                --   Agda chooses to chase dependencies.
          , envAllowDestructiveUpdate :: Bool
                -- ^ When True, allows destructively shared updating terms
                --   during evaluation or unification. This is disabled when
                --   doing speculative checking, like solve instance metas, or
                --   when updating might break abstraction, as is the case when
                --   checking abstract definitions.
          , envExpandLast :: ExpandHidden
                -- ^ When type-checking an alias f=e, we do not want
                -- to insert hidden arguments in the end, because
                -- these will become unsolved metas.
          , envAppDef :: Maybe QName
                -- ^ We are reducing an application of this function.
                -- (For debugging of incomplete matches only.)
          , envSimplification :: Simplification
                -- ^ Did we encounter a simplification (proper match)
                --   during the current reduction process?
          , envAllowedReductions :: AllowedReductions
          , envCompareBlocked :: Bool
                -- ^ Can we compare blocked things during conversion?
                --   No by default.
                --   Yes for rewriting feature.
          , envPrintDomainFreePi :: Bool
                -- ^ When @True@, types will be omitted from printed pi types if they
                --   can be inferred.
          , envPrintMetasBare :: Bool
                -- ^ When @True@, throw away meta numbers and meta elims.
                --   This is used for reifying terms for feeding into the
                --   user's source code, e.g., for the interaction tactics @solveAll@.
          , envInsideDotPattern :: Bool
                -- ^ Used by the scope checker to make sure that certain forms
                --   of expressions are not used inside dot patterns: extended
                --   lambdas and let-expressions.
          , envUnquoteFlags :: UnquoteFlags
          , envInstanceDepth :: !Int
                -- ^ Until we get a termination checker for instance search (#1743) we
                --   limit the search depth to ensure termination.
          }
    deriving (Typeable)

initEnv :: TCEnv
initEnv = TCEnv { envContext             = []
                , envLetBindings         = Map.empty
                , envCurrentModule       = noModuleName
                , envCurrentPath         = Nothing
                , envAnonymousModules    = []
                , envImportPath          = []
                , envMutualBlock         = Nothing
                , envTerminationCheck    = TerminationCheck
                , envSolvingConstraints  = False
                , envCheckingWhere       = False
                , envActiveProblems      = [0]
                , envAssignMetas         = True
                , envAbstractMode        = ConcreteMode
  -- Andreas, 2013-02-21:  This was 'AbstractMode' until now.
  -- However, top-level checks for mutual blocks, such as
  -- constructor-headedness, should not be able to look into
  -- abstract definitions unless abstract themselves.
  -- (See also discussion on issue 796.)
  -- The initial mode should be 'ConcreteMode', ensuring you
  -- can only look into abstract things in an abstract
  -- definition (which sets 'AbstractMode').
                , envRelevance           = Relevant
                , envDisplayFormsEnabled = True
                , envRange                  = noRange
                , envHighlightingRange      = noRange
                , envClause                 = IPNoClause
                , envCall                   = Nothing
                , envHighlightingLevel      = None
                , envHighlightingMethod     = Indirect
                , envModuleNestingLevel     = -1
                , envAllowDestructiveUpdate = True
                , envExpandLast             = ExpandLast
                , envAppDef                 = Nothing
                , envSimplification         = NoSimplification
                , envAllowedReductions      = allReductions
                , envCompareBlocked         = False
                , envPrintDomainFreePi      = False
                , envPrintMetasBare         = False
                , envInsideDotPattern       = False
                , envUnquoteFlags           = defaultUnquoteFlags
                , envInstanceDepth          = 0
                }

disableDestructiveUpdate :: TCM a -> TCM a
disableDestructiveUpdate = local $ \e -> e { envAllowDestructiveUpdate = False }

data UnquoteFlags = UnquoteFlags
  { _unquoteNormalise :: Bool }
  deriving (Typeable)

defaultUnquoteFlags :: UnquoteFlags
defaultUnquoteFlags = UnquoteFlags
  { _unquoteNormalise = False }

unquoteNormalise :: Lens' Bool UnquoteFlags
unquoteNormalise f e = f (_unquoteNormalise e) <&> \ x -> e { _unquoteNormalise = x }

eUnquoteNormalise :: Lens' Bool TCEnv
eUnquoteNormalise = eUnquoteFlags . unquoteNormalise

-- * e-prefixed lenses
------------------------------------------------------------------------

eContext :: Lens' Context TCEnv
eContext f e = f (envContext e) <&> \ x -> e { envContext = x }

eLetBindings :: Lens' LetBindings TCEnv
eLetBindings f e = f (envLetBindings e) <&> \ x -> e { envLetBindings = x }

eCurrentModule :: Lens' ModuleName TCEnv
eCurrentModule f e = f (envCurrentModule e) <&> \ x -> e { envCurrentModule = x }

eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
eCurrentPath f e = f (envCurrentPath e) <&> \ x -> e { envCurrentPath = x }

eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
eAnonymousModules f e = f (envAnonymousModules e) <&> \ x -> e { envAnonymousModules = x }

eImportPath :: Lens' [C.TopLevelModuleName] TCEnv
eImportPath f e = f (envImportPath e) <&> \ x -> e { envImportPath = x }

eMutualBlock :: Lens' (Maybe MutualId) TCEnv
eMutualBlock f e = f (envMutualBlock e) <&> \ x -> e { envMutualBlock = x }

eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
eTerminationCheck f e = f (envTerminationCheck e) <&> \ x -> e { envTerminationCheck = x }

eSolvingConstraints :: Lens' Bool TCEnv
eSolvingConstraints f e = f (envSolvingConstraints e) <&> \ x -> e { envSolvingConstraints = x }

eCheckingWhere :: Lens' Bool TCEnv
eCheckingWhere f e = f (envCheckingWhere e) <&> \ x -> e { envCheckingWhere = x }

eAssignMetas :: Lens' Bool TCEnv
eAssignMetas f e = f (envAssignMetas e) <&> \ x -> e { envAssignMetas = x }

eActiveProblems :: Lens' [ProblemId] TCEnv
eActiveProblems f e = f (envActiveProblems e) <&> \ x -> e { envActiveProblems = x }

eAbstractMode :: Lens' AbstractMode TCEnv
eAbstractMode f e = f (envAbstractMode e) <&> \ x -> e { envAbstractMode = x }

eRelevance :: Lens' Relevance TCEnv
eRelevance f e = f (envRelevance e) <&> \ x -> e { envRelevance = x }

eDisplayFormsEnabled :: Lens' Bool TCEnv
eDisplayFormsEnabled f e = f (envDisplayFormsEnabled e) <&> \ x -> e { envDisplayFormsEnabled = x }

eRange :: Lens' Range TCEnv
eRange f e = f (envRange e) <&> \ x -> e { envRange = x }

eHighlightingRange :: Lens' Range TCEnv
eHighlightingRange f e = f (envHighlightingRange e) <&> \ x -> e { envHighlightingRange = x }

eCall :: Lens' (Maybe (Closure Call)) TCEnv
eCall f e = f (envCall e) <&> \ x -> e { envCall = x }

eHighlightingLevel :: Lens' HighlightingLevel TCEnv
eHighlightingLevel f e = f (envHighlightingLevel e) <&> \ x -> e { envHighlightingLevel = x }

eHighlightingMethod :: Lens' HighlightingMethod TCEnv
eHighlightingMethod f e = f (envHighlightingMethod e) <&> \ x -> e { envHighlightingMethod = x }

eModuleNestingLevel :: Lens' Int TCEnv
eModuleNestingLevel f e = f (envModuleNestingLevel e) <&> \ x -> e { envModuleNestingLevel = x }

eAllowDestructiveUpdate :: Lens' Bool TCEnv
eAllowDestructiveUpdate f e = f (envAllowDestructiveUpdate e) <&> \ x -> e { envAllowDestructiveUpdate = x }

eExpandLast :: Lens' ExpandHidden TCEnv
eExpandLast f e = f (envExpandLast e) <&> \ x -> e { envExpandLast = x }

eAppDef :: Lens' (Maybe QName) TCEnv
eAppDef f e = f (envAppDef e) <&> \ x -> e { envAppDef = x }

eSimplification :: Lens' Simplification TCEnv
eSimplification f e = f (envSimplification e) <&> \ x -> e { envSimplification = x }

eAllowedReductions :: Lens' AllowedReductions TCEnv
eAllowedReductions f e = f (envAllowedReductions e) <&> \ x -> e { envAllowedReductions = x }

eCompareBlocked :: Lens' Bool TCEnv
eCompareBlocked f e = f (envCompareBlocked e) <&> \ x -> e { envCompareBlocked = x }

ePrintDomainFreePi :: Lens' Bool TCEnv
ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x }

eInsideDotPattern :: Lens' Bool TCEnv
eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x }

eUnquoteFlags :: Lens' UnquoteFlags TCEnv
eUnquoteFlags f e = f (envUnquoteFlags e) <&> \ x -> e { envUnquoteFlags = x }

eInstanceDepth :: Lens' Int TCEnv
eInstanceDepth f e = f (envInstanceDepth e) <&> \ x -> e { envInstanceDepth = x }

---------------------------------------------------------------------------
-- ** Context
---------------------------------------------------------------------------

-- | The @Context@ is a stack of 'ContextEntry's.
type Context      = [ContextEntry]
data ContextEntry = Ctx { ctxId    :: CtxId
                        , ctxEntry :: Dom (Name, Type)
                        }
  deriving (Typeable)

newtype CtxId     = CtxId Nat
  deriving (Typeable, Eq, Ord, Show, Enum, Real, Integral, Num)

---------------------------------------------------------------------------
-- ** Let bindings
---------------------------------------------------------------------------

type LetBindings = Map Name (Open (Term, Dom Type))

---------------------------------------------------------------------------
-- ** Abstract mode
---------------------------------------------------------------------------

data AbstractMode
  = AbstractMode        -- ^ Abstract things in the current module can be accessed.
  | ConcreteMode        -- ^ No abstract things can be accessed.
  | IgnoreAbstractMode  -- ^ All abstract things can be accessed.
  deriving (Typeable, Show, Eq)

aDefToMode :: IsAbstract -> AbstractMode
aDefToMode AbstractDef = AbstractMode
aDefToMode ConcreteDef = ConcreteMode

aModeToDef :: AbstractMode -> IsAbstract
aModeToDef AbstractMode = AbstractDef
aModeToDef ConcreteMode = ConcreteDef
aModeToDef _ = __IMPOSSIBLE__

---------------------------------------------------------------------------
-- ** Insertion of implicit arguments
---------------------------------------------------------------------------

data ExpandHidden
  = ExpandLast      -- ^ Add implicit arguments in the end until type is no longer hidden 'Pi'.
  | DontExpandLast  -- ^ Do not append implicit arguments.
  deriving (Eq)

data ExplicitToInstance
  = ExplicitToInstance    -- ^ Explicit arguments are considered as instance arguments
  | ExplicitStayExplicit
    deriving (Eq, Show)

-- | A candidate solution for an instance meta is a term with its type.
--   It may be the case that the candidate is not fully applied yet or
--   of the wrong type, hence the need for the type.
data Candidate  = Candidate { candidateTerm :: Term
                            , candidateType :: Type
                            , candidateEti  :: ExplicitToInstance
                            , candidateOverlappable :: Bool
                            }
  deriving (Show)

instance Free' Candidate c where
  freeVars' (Candidate t u _ _) = freeVars' (t, u)

---------------------------------------------------------------------------
-- * Type checking warnings (aka non-fatal errors)
---------------------------------------------------------------------------

-- | A non-fatal error is an error which does not prevent us from
-- checking the document further and interacting with the user.

-- We keep the state for termination issues, positivity issues and
-- unsolved constraints from when we encountered the warning so that
-- we can print it later
data Warning =
    TerminationIssue         [TerminationError]
  | NotStrictlyPositive      QName OccursWhere
  | UnsolvedMetaVariables    [Range]  -- ^ Do not use directly with 'warning'
  | UnsolvedInteractionMetas [Range]  -- ^ Do not use directly with 'warning'
  | UnsolvedConstraints      Constraints
    -- ^ Do not use directly with 'warning'
  | OldBuiltin               String String
    -- ^ In `OldBuiltin old new`, the BUILTIN old has been replaced by new
  | EmptyRewritePragma
    -- ^ If the user wrote just @{-# REWRITE #-}@.
  | ParseWarning             ParseWarning
  deriving Show

data TCWarning
  = TCWarning
    { tcWarningState   :: TCState
        -- ^ The state in which the warning was raised.
    , tcWarningClosure :: Closure Warning
        -- ^ The warning and the environment in which it was raised.
    }
  deriving Show

tcWarning :: TCWarning -> Warning
tcWarning = clValue . tcWarningClosure

---------------------------------------------------------------------------
-- * Type checking errors
---------------------------------------------------------------------------

-- | Information about a call.

data CallInfo = CallInfo
  { callInfoTarget :: QName
    -- ^ Target function name.
  , callInfoRange :: Range
    -- ^ Range of the target function.
  , callInfoCall :: Closure Term
    -- ^ To be formatted representation of the call.
  } deriving Typeable

-- no Eq, Ord instances: too expensive! (see issues 851, 852)

-- | We only 'show' the name of the callee.
instance Show   CallInfo where show   = show . callInfoTarget
instance Pretty CallInfo where pretty = text . show
instance AllNames CallInfo where allNames = singleton . callInfoTarget

-- UNUSED, but keep!
-- -- | Call pathes are sequences of 'CallInfo's starting from a 'callSource'.
-- data CallPath = CallPath
--   { callSource :: QName
--     -- ^ The originator of the first call.
--   , callInfos :: [CallInfo]
--     -- ^ The calls, in order from source to final target.
--   }
--   deriving (Show)

-- -- | 'CallPath'es can be connected, but there is no empty callpath.
-- --   Thus, they form a semigroup, but we choose to abuse 'Monoid'.
-- instance Monoid CallPath where
--   mempty = __IMPOSSIBLE__
--   mappend (CallPath src cs) (CallPath _ cs') = CallPath src $ cs ++ cs'

-- | Information about a mutual block which did not pass the
-- termination checker.

data TerminationError = TerminationError
  { termErrFunctions :: [QName]
    -- ^ The functions which failed to check. (May not include
    -- automatically generated functions.)
  , termErrCalls :: [CallInfo]
    -- ^ The problematic call sites.
  } deriving (Typeable, Show)

-- | Error when splitting a pattern variable into possible constructor patterns.
data SplitError
  = NotADatatype        (Closure Type)  -- ^ Neither data type nor record.
  | IrrelevantDatatype  (Closure Type)  -- ^ Data type, but in irrelevant position.
  | CoinductiveDatatype (Closure Type)  -- ^ Split on codata not allowed.
  -- UNUSED, but keep!
  -- -- | NoRecordConstructor Type  -- ^ record type, but no constructor
  | CantSplit
    { cantSplitConName  :: QName        -- ^ Constructor.
    , cantSplitTel      :: Telescope    -- ^ Context for indices.
    , cantSplitConIdx   :: Args         -- ^ Inferred indices (from type of constructor).
    , cantSplitGivenIdx :: Args         -- ^ Expected indices (from checking pattern).
    }
  | GenericSplitError String
  deriving (Show)

instance Error SplitError where
  strMsg = GenericSplitError

data UnquoteError
  = BadVisibility String (Arg I.Term)
  | ConInsteadOfDef QName String String
  | DefInsteadOfCon QName String String
  | NonCanonical String I.Term
  | BlockedOnMeta TCState MetaId
  | UnquotePanic String
  deriving (Show)

instance Error UnquoteError where
  strMsg msg = UnquotePanic msg

data TypeError
        = InternalError String
        | NotImplemented String
        | NotSupported String
        | CompilationError String
        | TerminationCheckFailed [TerminationError]
        | PropMustBeSingleton
        | DataMustEndInSort Term
{- UNUSED
        | DataTooManyParameters
            -- ^ In @data D xs where@ the number of parameters @xs@ does not fit the
            --   the parameters given in the forward declaraion @data D Gamma : T@.
-}
        | ShouldEndInApplicationOfTheDatatype Type
            -- ^ The target of a constructor isn't an application of its
            -- datatype. The 'Type' records what it does target.
        | ShouldBeAppliedToTheDatatypeParameters Term Term
            -- ^ The target of a constructor isn't its datatype applied to
            --   something that isn't the parameters. First term is the correct
            --   target and the second term is the actual target.
        | ShouldBeApplicationOf Type QName
            -- ^ Expected a type to be an application of a particular datatype.
        | ConstructorPatternInWrongDatatype QName QName -- ^ constructor, datatype
        | IndicesNotConstructorApplications [Arg Term] -- ^ Indices.
        | IndexVariablesNotDistinct [Nat] [Arg Term] -- ^ Variables, indices.
        | IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
          -- ^ Indices (variables), index expressions (with
          -- constructors applied to reconstructed parameters),
          -- parameters.
        | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
          -- ^ Datatype, constructors.
        | DoesNotConstructAnElementOf QName Type -- ^ constructor, type
        | DifferentArities
            -- ^ Varying number of arguments for a function.
        | WrongHidingInLHS
            -- ^ The left hand side of a function definition has a hidden argument
            --   where a non-hidden was expected.
        | WrongHidingInLambda Type
            -- ^ Expected a non-hidden function and found a hidden lambda.
        | WrongHidingInApplication Type
            -- ^ A function is applied to a hidden argument where a non-hidden was expected.
        | WrongNamedArgument (NamedArg A.Expr)
            -- ^ A function is applied to a hidden named argument it does not have.
        | WrongIrrelevanceInLambda Type
            -- ^ Expected a relevant function and found an irrelevant lambda.
        | WrongInstanceDeclaration
            -- ^ A term is declared as an instance but it’s not allowed
        | HidingMismatch Hiding Hiding
            -- ^ The given hiding does not correspond to the expected hiding.
        | RelevanceMismatch Relevance Relevance
            -- ^ The given relevance does not correspond to the expected relevane.
        | NotInductive Term
          -- ^ The term does not correspond to an inductive data type.
        | UninstantiatedDotPattern A.Expr
        | IlltypedPattern A.Pattern Type
        | IllformedProjectionPattern A.Pattern
        | CannotEliminateWithPattern (NamedArg A.Pattern) Type
        | TooManyArgumentsInLHS Type
        | WrongNumberOfConstructorArguments QName Nat Nat
        | ShouldBeEmpty Type [DeBruijnPattern]
        | ShouldBeASort Type
            -- ^ The given type should have been a sort.
        | ShouldBePi Type
            -- ^ The given type should have been a pi.
        | ShouldBeRecordType Type
        | ShouldBeRecordPattern DeBruijnPattern
        | NotAProjectionPattern (NamedArg A.Pattern)
        | NotAProperTerm
        | SetOmegaNotValidType
        | InvalidTypeSort Sort
            -- ^ This sort is not a type expression.
        | InvalidType Term
            -- ^ This term is not a type expression.
        | FunctionTypeInSizeUniv Term
            -- ^ This term, a function type constructor, lives in
            --   @SizeUniv@, which is not allowed.
        | SplitOnIrrelevant A.Pattern (Dom Type)
        | DefinitionIsIrrelevant QName
        | VariableIsIrrelevant Name
--        | UnequalLevel Comparison Term Term  -- UNUSED
        | UnequalTerms Comparison Term Term Type
        | UnequalTypes Comparison Type Type
--      | UnequalTelescopes Comparison Telescope Telescope -- UNUSED
        | UnequalRelevance Comparison Term Term
            -- ^ The two function types have different relevance.
        | UnequalHiding Term Term
            -- ^ The two function types have different hiding.
        | UnequalSorts Sort Sort
        | UnequalBecauseOfUniverseConflict Comparison Term Term
        | HeterogeneousEquality Term Type Term Type
            -- ^ We ended up with an equality constraint where the terms
            --   have different types.  This is not supported.
        | NotLeqSort Sort Sort
        | MetaCannotDependOn MetaId [Nat] Nat
            -- ^ The arguments are the meta variable, the parameters it can
            --   depend on and the paratemeter that it wants to depend on.
        | MetaOccursInItself MetaId
        | GenericError String
        | GenericDocError Doc
        | BuiltinMustBeConstructor String A.Expr
        | NoSuchBuiltinName String
        | DuplicateBuiltinBinding String Term Term
        | NoBindingForBuiltin String
        | NoSuchPrimitiveFunction String
        | ShadowedModule C.Name [A.ModuleName]
        | BuiltinInParameterisedModule String
        | IllegalLetInTelescope C.TypedBinding
        | NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
        | AbsurdPatternRequiresNoRHS [NamedArg A.Pattern]
        | TooFewFields QName [C.Name]
        | TooManyFields QName [C.Name]
        | DuplicateFields [C.Name]
        | DuplicateConstructors [C.Name]
        | WithOnFreeVariable A.Expr Term
        | UnexpectedWithPatterns [A.Pattern]
        | WithClausePatternMismatch A.Pattern Pattern
        | FieldOutsideRecord
        | ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
    -- Coverage errors
    -- TODO: Remove some of the constructors in this section, now that
    -- the SplitError constructor has been added?
        | IncompletePatternMatching Term [Elim] -- can only happen if coverage checking is switched off
        | CoverageFailure QName [[NamedArg DeBruijnPattern]]
        | UnreachableClauses QName [[NamedArg DeBruijnPattern]]
        | CoverageCantSplitOn QName Telescope Args Args
        | CoverageCantSplitIrrelevantType Type
        | CoverageCantSplitType Type
        | CoverageNoExactSplit QName Clause
        | WithoutKError Type Term Term
        | UnifyConflict ConHead ConHead
        | UnifyCycle Int Term
        | UnifyIndicesNotVars Type Term Term Args
        | UnificationRecursiveEq Type Int Term
        | UnificationStuck Telescope [Term] [Term]
        | SplitError SplitError
    -- Positivity errors
        | TooManyPolarities QName Integer
    -- Import errors
        | LocalVsImportedModuleClash ModuleName
        | SolvedButOpenHoles
          -- ^ Some interaction points (holes) have not been filled by user.
          --   There are not 'UnsolvedMetas' since unification solved them.
          --   This is an error, since interaction points are never filled
          --   without user interaction.
        | CyclicModuleDependency [C.TopLevelModuleName]
        | FileNotFound C.TopLevelModuleName [AbsolutePath]
        | OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
        | AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
        | ModuleNameUnexpected C.TopLevelModuleName C.TopLevelModuleName
          -- ^ Found module name, expected module name.
        | ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath]
        | ClashingFileNamesFor ModuleName [AbsolutePath]
        | ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath
          -- ^ Module name, file from which it was loaded, file which
          -- the include path says contains the module.
    -- Scope errors
        | BothWithAndRHS
        | NotInScope [C.QName]
        | NoSuchModule C.QName
        | AmbiguousName C.QName [A.QName]
        | AmbiguousModule C.QName [A.ModuleName]
        | UninstantiatedModule C.QName
        | ClashingDefinition C.QName A.QName
        | ClashingModule A.ModuleName A.ModuleName
        | ClashingImport C.Name A.QName
        | ClashingModuleImport C.Name A.ModuleName
        | PatternShadowsConstructor A.Name A.QName
        | ModuleDoesntExport C.QName [C.ImportedName]
        | DuplicateImports C.QName [C.ImportedName]
        | InvalidPattern C.Pattern
        | RepeatedVariablesInPattern [C.Name]
    -- Concrete to Abstract errors
        | NotAModuleExpr C.Expr
            -- ^ The expr was used in the right hand side of an implicit module
            --   definition, but it wasn't of the form @m Delta@.
        | NotAnExpression C.Expr
        | NotAValidLetBinding D.NiceDeclaration
        | NotValidBeforeField D.NiceDeclaration
        | NothingAppliedToHiddenArg C.Expr
        | NothingAppliedToInstanceArg C.Expr
    -- Pattern synonym errors
        | BadArgumentsToPatternSynonym A.QName
        | TooFewArgumentsToPatternSynonym A.QName
        | UnusedVariableInPatternSynonym
    -- Operator errors
        | NoParseForApplication [C.Expr]
        | AmbiguousParseForApplication [C.Expr] [C.Expr]
        | NoParseForLHS LHSOrPatSyn C.Pattern
        | AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
        | OperatorInformation [NotationSection] TypeError
        | OperatorChangeMessage TypeError
{- UNUSED
        | NoParseForPatternSynonym C.Pattern
        | AmbiguousParseForPatternSynonym C.Pattern [C.Pattern]
-}
    -- Usage errors
    -- Implicit From Scope errors
        | IFSNoCandidateInScope Type
    -- Reflection errors
        | UnquoteFailed UnquoteError
        | DeBruijnIndexOutOfScope Nat Telescope [Name]
    -- Safe flag errors
        | SafeFlagPostulate C.Name
        | SafeFlagPragma [String]
        | SafeFlagNonTerminating
        | SafeFlagTerminating
        | SafeFlagPrimTrustMe
        | SafeFlagNoPositivityCheck
        | SafeFlagPolarity
    -- Language option errors
        | NeedOptionCopatterns
        | NeedOptionRewriting
    -- Failure associated to warnings
        | NonFatalErrors [TCWarning]
    -- Instance search errors
        | InstanceSearchDepthExhausted Term Type Int
          deriving (Typeable, Show)

-- | Distinguish error message when parsing lhs or pattern synonym, resp.
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, Show)

-- instance Show TypeError where
--   show _ = "<TypeError>" -- TODO: more info?

#if !MIN_VERSION_transformers(0,4,1)
instance Error TypeError where
  strMsg = GenericError
#endif

-- | Type-checking errors.

data TCErr
  = TypeError
    { tcErrState   :: TCState
        -- ^ The state in which the error was raised.
    , tcErrClosErr :: Closure TypeError
        -- ^ The environment in which the error as raised plus the error.
    }
  | Exception Range Doc
  | IOException Range E.IOException
  | PatternErr
      -- ^ The exception which is usually caught.
      --   Raised for pattern violations during unification ('assignV')
      --   but also in other situations where we want to backtrack.
  deriving (Typeable)

instance Error TCErr where
  strMsg = Exception noRange . text . strMsg

instance Show TCErr where
    show (TypeError _ e) = show (envRange $ clEnv e) ++ ": " ++ show (clValue e)
    show (Exception r d) = show r ++ ": " ++ render d
    show (IOException r e) = show r ++ ": " ++ show e
    show PatternErr{}  = "Pattern violation (you shouldn't see this)"

instance HasRange TCErr where
    getRange (TypeError _ cl)  = envRange $ clEnv cl
    getRange (Exception r _)   = r
    getRange (IOException r _) = r
    getRange PatternErr{}      = noRange

instance E.Exception TCErr

-----------------------------------------------------------------------------
-- * The reduce monad
-----------------------------------------------------------------------------

-- | Environment of the reduce monad.
data ReduceEnv = ReduceEnv
  { redEnv :: TCEnv    -- ^ Read only access to environment.
  , redSt  :: TCState  -- ^ Read only access to state (signature, metas...).
  }

mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedEnv f s = s { redEnv = f (redEnv s) }

mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedSt f s = s { redSt = f (redSt s) }

mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv
            -> ReduceEnv
mapRedEnvSt f g (ReduceEnv e s) = ReduceEnv (f e) (g s)

newtype ReduceM a = ReduceM { unReduceM :: ReduceEnv -> a }
--  deriving (Functor, Applicative, Monad)

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
fmapReduce f (ReduceM m) = ReduceM $ \ e -> f $! m e
{-# INLINE fmapReduce #-}

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
apReduce (ReduceM f) (ReduceM x) = ReduceM $ \ e -> f e $! x e
{-# INLINE apReduce #-}

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
bindReduce (ReduceM m) f = ReduceM $ \ e -> unReduceM (f $! m e) e
{-# INLINE bindReduce #-}

instance Functor ReduceM where
  fmap = fmapReduce

instance Applicative ReduceM where
  pure x = ReduceM (const x)
  (<*>) = apReduce

instance Monad ReduceM where
  return = pure
  (>>=) = bindReduce
  (>>) = (*>)

instance ReadTCState ReduceM where
  getTCState = ReduceM redSt

runReduceM :: ReduceM a -> TCM a
runReduceM m = do
  e <- ask
  s <- get
  return $! unReduceM m (ReduceEnv e s)

runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
runReduceF f = do
  e <- ask
  s <- get
  return $ \x -> unReduceM (f x) (ReduceEnv e s)

instance MonadReader TCEnv ReduceM where
  ask = ReduceM redEnv
  local f (ReduceM m) = ReduceM (m . mapRedEnv f)

---------------------------------------------------------------------------
-- * Type checking monad transformer
---------------------------------------------------------------------------

newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }

-- TODO: make dedicated MonadTCEnv and MonadTCState service classes

instance MonadIO m => MonadReader TCEnv (TCMT m) where
  ask = TCM $ \s e -> return e
  local f (TCM m) = TCM $ \s e -> m s (f e)

instance MonadIO m => MonadState TCState (TCMT m) where
  get   = TCM $ \s _ -> liftIO (readIORef s)
  put s = TCM $ \r _ -> liftIO (writeIORef r s)

type TCM = TCMT IO

class ( Applicative tcm, MonadIO tcm
      , MonadReader TCEnv tcm
      , MonadState TCState tcm
      ) => MonadTCM tcm where
    liftTCM :: TCM a -> tcm a

instance MonadIO m => ReadTCState (TCMT m) where
  getTCState = get

instance MonadError TCErr (TCMT IO) where
  throwError = liftIO . E.throwIO
  catchError m h = TCM $ \r e -> do
    oldState <- liftIO (readIORef r)
    unTCM m r e `E.catch` \err -> do
      -- Reset the state, but do not forget changes to the persistent
      -- component. Not for pattern violations.
      case err of
        PatternErr -> return ()
        _          ->
          liftIO $ do
            newState <- readIORef r
            writeIORef r $ oldState { stPersistentState = stPersistentState newState }
      unTCM (h err) r e

-- | Parse monad

runPM :: PM a -> TCM a
runPM m = do
  (res, ws) <- runPMIO m
  mapM_ (warning . ParseWarning) ws
  case res of
    Left  e -> throwError (Exception (getRange e) (pretty e))
    Right a -> return a

-- | Interaction monad.

type IM = TCMT (Haskeline.InputT IO)

runIM :: IM a -> TCM a
runIM = mapTCMT (Haskeline.runInputT Haskeline.defaultSettings)

instance MonadError TCErr IM where
  throwError = liftIO . E.throwIO
  catchError m h = mapTCMT liftIO $ runIM m `catchError` (runIM . h)

-- | Preserve the state of the failing computation.
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \r e ->
  unTCM m r e
  `E.catch` \err -> unTCM (h err) r e

-- | Execute a finalizer even when an exception is thrown.
--   Does not catch any errors.
--   In case both the regular computation and the finalizer
--   throw an exception, the one of the finalizer is propagated.
finally_ :: TCM a -> TCM b -> TCM a
finally_ m f = do
    x <- m `catchError_` \ err -> f >> throwError err
    _ <- f
    return x

{-# SPECIALIZE INLINE mapTCMT :: (forall a. IO a -> IO a) -> TCM a -> TCM a #-}
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
mapTCMT f (TCM m) = TCM $ \s e -> f (m s e)

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \r e -> do
  s <- liftIO $ readIORef r
  return (f s e)

{-# RULES "liftTCM/id" liftTCM = id #-}
instance MonadIO m => MonadTCM (TCMT m) where
    liftTCM = mapTCMT liftIO

instance MonadTCM tcm => MonadTCM (MaybeT tcm) where
  liftTCM = lift . liftTCM

instance MonadTCM tcm => MonadTCM (ListT tcm) where
  liftTCM = lift . liftTCM

instance
#if !MIN_VERSION_transformers(0,4,1)
  (Error err, MonadTCM tcm)
#else
  MonadTCM tcm
#endif
  => MonadTCM (ExceptT err tcm) where
  liftTCM = lift . liftTCM

instance (Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) where
  liftTCM = lift . liftTCM

{- The following is not possible since MonadTCM needs to be a
-- MonadState TCState and a MonadReader TCEnv

instance (MonadTCM tcm) => MonadTCM (StateT s tcm) where
  liftTCM = lift . liftTCM

instance (MonadTCM tcm) => MonadTCM (ReaderT r tcm) where
  liftTCM = lift . liftTCM
-}

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

-- We want a special monad implementation of fail.
instance MonadIO m => Monad (TCMT m) where
    return = pure
    (>>=)  = bindTCMT
    (>>)   = (*>)
    fail   = internalError

-- One goal of the definitions and pragmas below is to inline the
-- monad operations as much as possible. This doesn't seem to have a
-- large effect on the performance of the normal executable, but (at
-- least on one machine/configuration) it has a massive effect on the
-- performance of the profiling executable [1], and reduces the time
-- attributed to bind from over 90% to about 25%.
--
-- [1] When compiled with -auto-all and run with -p: roughly 750%
-- faster for one example.

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

bindTCMT :: MonadIO 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 :: MonadIO 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 MonadIO m => Functor (TCMT m) where
  fmap = fmapTCMT

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

instance MonadIO m => Applicative (TCMT m) where
  pure  = returnTCMT
  (<*>) = apTCMT

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
{-# INLINE apTCMT #-}

instance MonadIO m => MonadIO (TCMT m) where
  liftIO m = TCM $ \s e -> do
               let r = envRange e
               liftIO $ wrap r $ do
                 x <- m
                 x `seq` return x
    where
      wrap r m = E.catch m (handleIOException r)

      handleIOException r e = E.throwIO $ IOException r e

-- | We store benchmark statistics in an IORef.
--   This enables benchmarking pure computation, see
--   "Agda.Benchmarking".
instance MonadBench Phase TCM where
  getBenchmark = liftIO $ getBenchmark
  putBenchmark = liftIO . putBenchmark
  finally = finally_

instance Null (TCM Doc) where
  empty = return empty
  null = __IMPOSSIBLE__

-- | Short-cutting disjunction forms a monoid.
instance Semigroup (TCM Any) where
  ma <> mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb)

instance Monoid (TCM Any) where
  mempty = return mempty
  mappend = (<>)

patternViolation :: TCM a
patternViolation = throwError PatternErr

internalError :: MonadTCM tcm => String -> tcm a
internalError s = typeError $ InternalError s

genericError :: MonadTCM tcm => String -> tcm a
genericError = typeError . GenericError

{-# SPECIALIZE genericDocError :: Doc -> TCM a #-}
genericDocError :: MonadTCM tcm => Doc -> tcm a
genericDocError = typeError . GenericDocError

{-# SPECIALIZE typeError :: TypeError -> TCM a #-}
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError err = liftTCM $ throwError =<< typeError_ err

{-# SPECIALIZE typeError_ :: TypeError -> TCM TCErr #-}
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
typeError_ err = liftTCM $ TypeError <$> get <*> buildClosure err

{-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-}
warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
warning_ w = liftTCM $ TCWarning <$> get <*> buildClosure w

{-# SPECIALIZE warning :: Warning -> TCM () #-}
warning :: MonadTCM tcm => Warning -> tcm ()
warning w = do
  tcwarn <- warning_ w
  stTCWarnings %= (tcwarn :)

-- | Running the type checking monad (most general form).
{-# SPECIALIZE runTCM :: TCEnv -> TCState -> TCM a -> IO (a, TCState) #-}
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM e s m = do
  r <- liftIO $ newIORef s
  a <- unTCM m r e
  s <- liftIO $ readIORef r
  return (a, s)

-- | Running the type checking monad on toplevel (with initial state).
runTCMTop :: TCM a -> IO (Either TCErr a)
runTCMTop m = (Right <$> runTCMTop' m) `E.catch` (return . Left)

runTCMTop' :: MonadIO m => TCMT m a -> m a
runTCMTop' m = do
  r <- liftIO $ newIORef initState
  unTCM m r initEnv

-- | 'runSafeTCM' runs a safe 'TCM' action (a 'TCM' action which cannot fail)
--   in the initial environment.

runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
runSafeTCM m st = runTCM initEnv st m `E.catch` (\ (e :: TCErr) -> __IMPOSSIBLE__)
-- runSafeTCM m st = either__IMPOSSIBLE__ return <$> do
--     -- Errors must be impossible.
--     runTCM $ do
--         put st
--         a <- m
--         st <- get
--         return (a, st)

-- | Runs the given computation in a separate thread, with /a copy/ of
-- the current state and environment.
--
-- Note that Agda sometimes uses actual, mutable state. If the
-- computation given to @forkTCM@ tries to /modify/ this state, then
-- bad things can happen, because accesses are not mutually exclusive.
-- The @forkTCM@ function has been added mainly to allow the thread to
-- /read/ (a snapshot of) the current state in a convenient way.
--
-- Note also that exceptions which are raised in the thread are not
-- propagated to the parent, so the thread should not do anything
-- important.

forkTCM :: TCM a -> TCM ()
forkTCM m = do
  s <- get
  e <- ask
  liftIO $ void $ C.forkIO $ void $ runTCM e s m


-- | Base name for extended lambda patterns
extendedLambdaName :: String
extendedLambdaName = ".extendedlambda"

-- | Name of absurdLambda definitions.
absurdLambdaName :: String
absurdLambdaName = ".absurdlambda"

-- | Check whether we have an definition from an absurd lambda.
isAbsurdLambdaName :: QName -> Bool
isAbsurdLambdaName = (absurdLambdaName ==) . prettyShow . qnameName

---------------------------------------------------------------------------
-- * KillRange instances
---------------------------------------------------------------------------

instance KillRange Signature where
  killRange (Sig secs defs rews) = killRange2 Sig secs defs rews

instance KillRange Sections where
  killRange = fmap killRange

instance KillRange Definitions where
  killRange = fmap killRange

instance KillRange RewriteRuleMap where
  killRange = fmap killRange

instance KillRange Section where
  killRange (Section tel) = killRange1 Section tel

instance KillRange Definition where
  killRange (Defn ai name t pols occs displ mut compiled inst copy ma def) =
    killRange11 Defn ai name t pols occs displ mut compiled inst copy ma def
    -- TODO clarify: Keep the range in the defName field?

instance KillRange CtxId where
  killRange (CtxId x) = killRange1 CtxId x

instance KillRange NLPat where
  killRange (PVar x y z) = killRange3 PVar x y z
  killRange (PWild)    = PWild
  killRange (PDef x y) = killRange2 PDef x y
  killRange (PLam x y) = killRange2 PLam x y
  killRange (PPi x y)  = killRange2 PPi x y
  killRange (PBoundVar x y) = killRange2 PBoundVar x y
  killRange (PTerm x)  = killRange1 PTerm x

instance KillRange NLPType where
  killRange (NLPType s a) = killRange2 NLPType s a

instance KillRange RewriteRule where
  killRange (RewriteRule q gamma f es rhs t) =
    killRange6 RewriteRule q gamma f es rhs t

instance KillRange CompiledRepresentation where
  killRange = id


instance KillRange EtaEquality where
  killRange = id

instance KillRange ExtLamInfo where
  killRange = id

instance KillRange FunctionFlag where
  killRange = id

instance KillRange Defn where
  killRange def =
    case def of
      Axiom -> Axiom
      AbstractDefn -> __IMPOSSIBLE__ -- only returned by 'getConstInfo'!
      Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat ->
        killRange13 Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat
      Datatype a b c d e f g h i j   -> killRange10 Datatype a b c d e f g h i j
      Record a b c d e f g h i j k   -> killRange11 Record a b c d e f g h i j k
      Constructor a b c d e f        -> killRange6 Constructor a b c d e f
      Primitive a b c d              -> killRange4 Primitive a b c d

instance KillRange MutualId where
  killRange = id

instance KillRange c => KillRange (FunctionInverse' c) where
  killRange NotInjective = NotInjective
  killRange (Inverse m)  = Inverse $ killRangeMap m

instance KillRange TermHead where
  killRange SortHead     = SortHead
  killRange PiHead       = PiHead
  killRange (ConsHead q) = ConsHead $ killRange q

instance KillRange Projection where
  killRange (Projection a b c d e) = killRange5 Projection a b c d e

instance KillRange ProjLams where
  killRange = id

instance KillRange a => KillRange (Open a) where
  killRange = fmap killRange

instance KillRange a => KillRange (Local a) where
  killRange (Local a b) = killRange2 Local a b
  killRange (Global a)  = killRange1 Global a

instance KillRange DisplayForm where
  killRange (Display n es dt) = killRange3 Display n es dt

instance KillRange Polarity where
  killRange = id

instance KillRange DisplayTerm where
  killRange dt =
    case dt of
      DWithApp dt dts es -> killRange3 DWithApp dt dts es
      DCon q ci dts     -> killRange3 DCon q ci dts
      DDef q dts        -> killRange2 DDef q dts
      DDot v            -> killRange1 DDot v
      DTerm v           -> killRange1 DTerm v