    {-# LANGUAGE CPP, ExistentialQuantification, FlexibleContexts, Rank2Types,
                 TypeSynonymInstances, MultiParamTypeClasses, FlexibleInstances,
                 UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
      #-}
    module Agda.TypeChecking.Monad.Base where

    import Control.Exception as E
    import Control.Monad.Error
    import Control.Monad.State
    import Control.Monad.Reader
    import Control.Applicative
    import Data.Map as Map
    import Data.Set as Set
    import Data.Generics
    import Data.Foldable
    import Data.Traversable
    import System.Time

    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.Internal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    import Agda.Interaction.Exceptions
    import {-# SOURCE #-} Agda.Interaction.FindFile
    import Agda.Interaction.Options
    import qualified Agda.Interaction.Highlighting.Range as R
    import Agda.Interaction.Highlighting.Precise (HighlightingInfo)

    import Agda.Utils.FileName
    import Agda.Utils.Fresh
    import Agda.Utils.Monad
    import Agda.Utils.Trace

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

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

    data TCState =
        TCSt { stFreshThings       :: FreshThings
    	 , stMetaStore	       :: MetaStore
    	 , stInteractionPoints :: InteractionPoints
    	 , stConstraints       :: Constraints
    	 , stSignature	       :: Signature
    	 , stImports	       :: Signature
    	 , stImportedModules   :: Set ModuleName
             , stModuleToSource    :: ModuleToSource
    	 , stVisitedModules    :: VisitedModules
    	 , stDecodedModules    :: DecodedModules
             , stCurrentModule     :: Maybe ModuleName
               -- ^ The current module is available after it has been type
               -- checked.
    	 , stScope	       :: ScopeInfo
    	 , stPersistentOptions :: CommandLineOptions
               -- ^ Options which apply to all files, unless overridden.
    	 , stPragmaOptions     :: CommandLineOptions
               -- ^ Options applying to the current file. @OPTIONS@
               -- pragmas only affect this field.
    	 , stStatistics	       :: Statistics
    	 , stTrace	       :: CallTrace
    	     -- ^ record what is happening (for error msgs)
    	 , stMutualBlocks      :: Map MutualId (Set QName)
    	 , stLocalBuiltins     :: BuiltinThings PrimFun
             , stImportedBuiltins  :: BuiltinThings PrimFun
             , stHaskellImports    :: Set String
               -- ^ Imports that should be generated by the compiler (this
               -- includes imports from imported modules).
    	 }

    data FreshThings =
    	Fresh { fMeta	     :: MetaId
    	      , fInteraction :: InteractionId
    	      , fMutual	     :: MutualId
    	      , fName	     :: NameId
    	      , fCtx	     :: CtxId
                  , fInteger     :: Integer
                    -- ^ Can be used for various things.
    	      }
        deriving (Show)

    initState :: TCState
    initState =
        TCSt { stFreshThings       = Fresh 0 0 0 (NameId 0 0) 0 0
    	 , stMetaStore	       = Map.empty
    	 , stInteractionPoints = Map.empty
    	 , stConstraints       = []
    	 , stSignature	       = emptySignature
    	 , stImports	       = emptySignature
    	 , stImportedModules   = Set.empty
             , stModuleToSource    = Map.empty
    	 , stVisitedModules    = Map.empty
    	 , stDecodedModules    = Map.empty
             , stCurrentModule     = Nothing
    	 , stScope	       = emptyScopeInfo
    	 , stPersistentOptions = defaultOptions
    	 , stPragmaOptions     = defaultOptions
    	 , stStatistics	       = Map.empty
    	 , stTrace	       = noTrace
    	 , stMutualBlocks      = Map.empty
    	 , stLocalBuiltins     = Map.empty
    	 , stImportedBuiltins  = Map.empty
             , stHaskellImports    = Set.empty
    	 }

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

    instance HasFresh MetaId FreshThings where
        nextFresh s = (i, s { fMeta = i + 1 })
    	where
    	    i = fMeta s

    instance HasFresh MutualId FreshThings where
        nextFresh s = (i, s { fMutual = i + 1 })
    	where
    	    i = fMutual s

    instance HasFresh InteractionId FreshThings where
        nextFresh s = (i, s { fInteraction = i + 1 })
    	where
    	    i = fInteraction s

    instance HasFresh NameId FreshThings where
        nextFresh s = (i, s { fName = succ i })
    	where
    	    i = fName s

    instance HasFresh CtxId FreshThings where
        nextFresh s = (i, s { fCtx = succ i })
    	where
    	    i = fCtx s

    instance HasFresh Integer FreshThings where
        nextFresh s = (i, s { fInteger = succ i })
    	where
    	    i = fInteger s

    instance HasFresh i FreshThings => HasFresh i TCState where
        nextFresh s = (i, s { stFreshThings = f })
    	where
    	    (i,f) = nextFresh $ stFreshThings s

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

    data ModuleInfo = ModuleInfo
      { miInterface  :: Interface
      , miWarnings   :: Bool
        -- ^ 'True' if warnings were encountered when the module was type
        -- checked.
      , miTimeStamp  :: ClockTime
        -- ^ The modification time stamp of the interface file when the
        -- interface was read or written. Alternatively, if warnings were
        -- encountered (in which case there may not be any up-to-date
        -- interface file), the time at which the interface was produced
        -- (approximately).
      }

    -- 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, ClockTime)

    data Interface = Interface
    	{ iImportedModules :: [ModuleName]
            , iModuleName      :: ModuleName
    	, iScope	   :: Map ModuleName Scope
            , iInsideScope     :: ScopeInfo
    	, iSignature	   :: Signature
    	, iBuiltin	   :: BuiltinThings String
            , iHaskellImports  :: Set String
                                  -- ^ Haskell imports listed in
                                  -- (transitively) imported modules are
                                  -- not included here.
            , iHighlighting    :: HighlightingInfo
    	}
        deriving (Typeable, Data, Show)

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

    data Closure a = Closure { clSignature  :: Signature
    			 , clEnv	:: TCEnv
    			 , clScope	:: ScopeInfo
    			 , clTrace	:: CallTrace
    			 , clValue	:: a
    			 }
        deriving (Typeable, Data)

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

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

    buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
    buildClosure x = liftTCM $ do
        env   <- ask
        sig   <- gets stSignature
        scope <- gets stScope
        trace <- gets stTrace
        return $ Closure sig env scope trace x

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

    type ConstraintClosure = Closure Constraint

    data Constraint = ValueCmp Comparison Type Term Term
    		| TypeCmp Comparison Type Type
                    | TelCmp Comparison Telescope Telescope
    		| SortCmp Comparison Sort Sort
    		| UnBlock MetaId
    		| Guarded Constraint Constraints
                    | IsEmpty Type
      deriving (Typeable, Show)

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

    type Constraints = [ConstraintClosure]

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

    -- | A thing tagged with the context it came from.
    data Open a = OpenThing [CtxId] a
        deriving (Typeable, Data, Show)

    ---------------------------------------------------------------------------
    -- * Judgements
    ---------------------------------------------------------------------------

    data Judgement t a
    	= HasType a t
    	| IsSort  a
        deriving (Typeable, Data)

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

    instance Functor (Judgement t) where
        fmap f (HasType x t) = HasType (f x) t
        fmap f (IsSort  x)	 = IsSort (f x)

    instance Foldable (Judgement t) where
        foldr f z (HasType x _) = f x z
        foldr f z (IsSort  x)   = f x z

    instance Traversable (Judgement t) where
        traverse f (HasType x t) = flip HasType t <$> f x
        traverse f (IsSort  x)   = IsSort <$> f x

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

    data MetaVariable =
    	MetaVar	{ mvInfo	  :: MetaInfo
    		, mvPriority	  :: MetaPriority -- ^ some metavariables are more eager to be instantiated
    		, mvJudgement	  :: Judgement Type MetaId
    		, mvInstantiation :: MetaInstantiation
    		, mvListeners	  :: Set MetaId	  -- ^ metavariables interested in what happens to this guy
    		}
        deriving (Typeable)

    data MetaInstantiation
    	= InstV Term
    	| InstS Term  -- should be Lam .. Sort s
    	| Open
    	| BlockedConst Term
            | PostponedTypeCheckingProblem (Closure (A.Expr, Type, TCM Bool))
        deriving (Typeable)

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

    newtype MetaPriority = MetaPriority Int
        deriving (Eq, Ord, Show)

    -- | TODO: Not so nice.
    type MetaInfo = Closure Range

    type MetaStore = Map MetaId MetaVariable

    instance HasRange MetaVariable where
        getRange m = getRange $ getMetaInfo m

    instance SetRange MetaVariable where
      setRange r (MetaVar mi p j inst ls) = MetaVar (mi {clValue = r}) p j inst ls

    normalMetaPriority :: MetaPriority
    normalMetaPriority = MetaPriority 0

    lowMetaPriority :: MetaPriority
    lowMetaPriority = MetaPriority (-10)

    highMetaPriority :: MetaPriority
    highMetaPriority = MetaPriority 10

    getMetaInfo :: MetaVariable -> MetaInfo
    getMetaInfo = 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

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

    type InteractionPoints = Map InteractionId MetaId

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

    instance Show InteractionId where
        show (InteractionId x) = "?" ++ show x

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

    data Signature = Sig
          { sigSections    :: Sections
          , sigDefinitions :: Definitions
          }
      deriving (Typeable, Data, Show)

    type Sections	 = Map ModuleName Section
    type Definitions = Map QName Definition

    data Section = Section
          { secTelescope :: Telescope
          , secFreeVars  :: Nat	    -- ^ This is the number of parameters when
    				    --	 we're inside the section and 0
    				    --	 outside. It's used to know how much of
    				    --	 the context to apply function from the
    				    --	 section to when translating from
    				    --	 abstract to internal syntax.
          }
      deriving (Typeable, Data, Show)

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

    data DisplayForm = Display Nat [Term] DisplayTerm
    		-- ^ The three arguments are:
    		--
    		--   * @n@: number of free variables;
    		--
    		--   * Patterns for arguments, one extra free var which
    		--     represents pattern vars. There should @n@ of them.
    		--
    		--   * Display form. @n@ free variables.
      deriving (Typeable, Data, Show)

    data DisplayTerm = DWithApp [DisplayTerm] Args
    		 | DTerm Term
      deriving (Typeable, Data, Show)

    defaultDisplayForm :: QName -> [Open DisplayForm]
    defaultDisplayForm c = []

    data Definition = Defn { defName     :: QName
    		       , defType     :: Type	-- type of the lifted definition
    		       , defDisplay  :: [Open DisplayForm]
    		       , defMutual   :: MutualId
    		       , theDef	     :: Defn
    		       }
        deriving (Typeable, Data, Show)

    type HaskellCode = String
    type HaskellType = String

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

    data Polarity = Covariant | Contravariant | Invariant
      deriving (Typeable, Data, Show, Eq)

    -- | 'Positive' means strictly positive and 'Negative' means not strictly
    -- positive.
    data Occurrence = Positive | Negative | Unused
      deriving (Typeable, Data, Show, Eq, Ord)

    data Defn = Axiom
                { axHsDef   :: Maybe HaskellRepresentation
                }
    	  | Function
                { funClauses        :: [Clause]
                , funInv            :: FunctionInverse
                , funPolarity       :: [Polarity]
                , funArgOccurrences :: [Occurrence]
                , funAbstr          :: IsAbstract
                , funDelayed        :: Delayed
                  -- ^ Are the clauses of this definition delayed?
                }
    	  | Datatype
                { dataPars           :: Nat           -- nof parameters
    	    , dataIxs            :: Nat           -- nof indices
                , dataInduction      :: Induction  -- data or codata?
                , dataClause         :: (Maybe Clause) -- this might be in an instantiated module
                , dataCons           :: [QName]        -- constructor names
                , dataSort           :: Sort
                , dataPolarity       :: [Polarity]
                , dataArgOccurrences :: [Occurrence]
                , dataHsType         :: Maybe HaskellType
                , dataAbstr          :: IsAbstract
                }
    	  | Record
                { recPars           :: Nat
                , recClause         :: Maybe Clause
                , recCon            :: Maybe QName          -- ^ Constructor name.
                , recConType        :: Type                 -- ^ The record constructor's type.
                , recFields         :: [(Hiding, A.QName)]
                , recTel            :: Telescope
                , recPolarity       :: [Polarity]
                , recArgOccurrences :: [Occurrence]
                , recAbstr          :: IsAbstract
                }
    	  | Constructor
                { conPars   :: Nat         -- nof parameters
    	    , conSrcCon :: QName       -- original constructor (this might be in a module instance)
    	    , conData   :: QName       -- name of datatype or record type
                , conHsCode :: Maybe (HaskellType, HaskellCode) -- used by the compiler
    	    , conAbstr  :: IsAbstract
                , conInd    :: Induction   -- ^ Inductive or coinductive?
                }
    	  | Primitive
                { primAbstr :: IsAbstract
                , primName  :: String
                , primClauses :: Maybe [Clause]
                  -- ^ 'Nothing' for primitive functions, @'Just'
                  -- something@ for builtin functions.
                }
                -- ^ Primitive or builtin functions.
        deriving (Typeable, Data, Show)

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

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

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

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

    -- | Used to specify whether something should be delayed.
    data Delayed = Delayed | NotDelayed
      deriving (Typeable, Data, Show, Eq)

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

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

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

    data FunctionInverse = NotInjective
                         | Inverse (Map TermHead Clause)
      deriving (Typeable, Data, Show)

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

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

    newtype MutualId = MutId Int
      deriving (Typeable, Data, Eq, Ord, Show, Num)

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

    type Statistics = Map String Int

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

    type CallTrace = Trace (Closure Call)

    noTrace :: CallTrace
    noTrace = TopLevel []

    data Call = CheckClause Type A.Clause (Maybe Clause)
    	  | forall a. CheckPattern A.Pattern Telescope Type (Maybe a)
    	  | CheckLetBinding A.LetBinding (Maybe ())
    	  | InferExpr A.Expr (Maybe (Term, Type))
    	  | CheckExpr A.Expr Type (Maybe Term)
    	  | CheckDotPattern A.Expr Term (Maybe Constraints)
    	  | CheckPatternShadowing A.Clause (Maybe ())
    	  | IsTypeCall A.Expr Sort (Maybe Type)
    	  | IsType_ A.Expr (Maybe Type)
    	  | InferVar Name (Maybe (Term, Type))
    	  | InferDef Range QName (Maybe (Term, Type))
    	  | CheckArguments Range [NamedArg A.Expr] Type Type (Maybe (Args, Type, Constraints))
    	  | CheckDataDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
    	  | CheckRecDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
    	  | CheckConstructor QName Telescope Sort A.Constructor (Maybe ())
    	  | CheckFunDef Range Name [A.Clause] (Maybe ())
    	  | CheckPragma Range A.Pragma (Maybe ())
    	  | CheckPrimitive Range Name A.Expr (Maybe ())
              | CheckSectionApplication Range ModuleName A.Telescope ModuleName [NamedArg A.Expr] (Maybe ())
    	  | ScopeCheckExpr C.Expr (Maybe A.Expr)
    	  | ScopeCheckDeclaration D.NiceDeclaration (Maybe [A.Declaration])
    	  | ScopeCheckLHS C.Name C.Pattern (Maybe A.LHS)
    	  | ScopeCheckDefinition D.NiceDefinition (Maybe A.Definition)
    	  | forall a. TermFunDef Range Name [A.Clause] (Maybe a)
    	  | forall a. SetRange Range (Maybe a)	-- ^ used by 'setCurrentRange'
                -- actually, 'a' is Agda.Termination.TermCheck.CallGraph
                -- but I was to lazy to import the stuff here --Andreas,2007-5-29

        deriving (Typeable)

    -- Dummy instance
    instance Data Call where
      dataTypeOf _  = mkDataType "Call" []
      toConstr   x  = mkConstr (dataTypeOf x) "Dummy" [] Prefix
      gunfold k z _ = __IMPOSSIBLE__

    instance HasRange a => HasRange (Trace a) where
        getRange (TopLevel _)      = noRange
        getRange (Current c par _ _)
          | r == noRange = getRange par
          | otherwise    = r
          where r = getRange c

    instance HasRange a => HasRange (ParentCall a) where
      getRange NoParent = noRange
      getRange (Parent c par _)
        | r == noRange = getRange par
        | otherwise	   = r
        where r = getRange c

    instance HasRange Call where
        getRange (CheckClause _ c _)                   = getRange c
        getRange (CheckPattern p _ _ _)                = getRange p
        getRange (InferExpr e _)                       = getRange e
        getRange (CheckExpr e _ _)                     = getRange e
        getRange (CheckLetBinding b _)                 = getRange b
        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 (ScopeCheckExpr e _)                  = getRange e
        getRange (ScopeCheckDeclaration d _)           = getRange d
        getRange (ScopeCheckLHS _ p _)                 = getRange p
        getRange (ScopeCheckDefinition d _)            = getRange d
        getRange (CheckDotPattern e _ _)               = getRange e
        getRange (CheckPatternShadowing c _)           = getRange c
        getRange (TermFunDef i _ _ _)                  = getRange i
        getRange (SetRange r _)                        = r
        getRange (CheckSectionApplication r _ _ _ _ _) = r

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

    type BuiltinThings pf = Map String (Builtin pf)

    data Builtin pf
    	= Builtin Term
    	| Prim pf
        deriving (Typeable, Data, Show)

    instance Functor Builtin where
        fmap f (Builtin t) = Builtin t
        fmap f (Prim x)    = Prim $ f x

    instance Foldable Builtin where
        foldr f z (Builtin t) = z
        foldr f z (Prim x)    = f x z

    instance Traversable Builtin where
        traverse f (Builtin t) = pure $ Builtin t
        traverse f (Prim x)    = Prim <$> f x

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

    data TCEnv =
        TCEnv { envContext             :: Context
    	  , envLetBindings         :: LetBindings
    	  , envCurrentModule       :: ModuleName
              , 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
    	  , 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.
              , envReplace             :: Bool
                    -- ^ Coinductive constructor applications @c args@ get
                    -- replaced by a function application @f tel@, where
                    -- tel corresponds to the current telescope and @f@ is
                    -- defined as @f tel = c args@. The initial occurrence
                    -- of @c@ in the body of @f@ should not be replaced by
                    -- yet another function application, though. To avoid
                    -- that this happens the @envReplace@ flag is set to
                    -- 'False' when @f@ is checked.
              , envDisplayFormsEnabled :: Bool
                    -- ^ Sometimes we want to disable display forms.
              , envReifyInteractionPoints :: Bool
                    -- ^ should we try to recover interaction points when reifying?
                    --   disabled when generating types for with functions
    	  }
        deriving (Typeable, Data)

    initEnv :: TCEnv
    initEnv = TCEnv { envContext	         = []
    		, envLetBindings         = Map.empty
    		, envCurrentModule       = noModuleName
                    , envAnonymousModules    = []
    		, envImportPath          = []
    		, envMutualBlock         = Nothing
    		, envAbstractMode        = AbstractMode
                    , envReplace             = True
                    , envDisplayFormsEnabled = True
                    , envReifyInteractionPoints = True
    		}

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

    type Context	  = [ContextEntry]
    data ContextEntry = Ctx { ctxId	   :: CtxId
    			, ctxEntry :: Arg (Name, Type)
    			}
      deriving (Typeable, Data)

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

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

    type LetBindings = Map Name (Open (Term, 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, Data)

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

    -- Occurence of a name in a datatype definition
    data Occ = OccCon { occDatatype	:: QName
    	          , occConstructor :: QName
    	          , occPosition	:: OccPos
    	          }
             | OccClause { occFunction :: QName
                         , occClause   :: Int
                         , occPosition :: OccPos
                         }

    data OccPos = NonPositively | ArgumentTo Nat QName

    data TypeError
    	= InternalError String
    	| NotImplemented String
    	| NotSupported String
            | CompilationError String
    	| TerminationCheckFailed [([QName], [R.Range])]
              -- ^ Parameterised on functions which failed to termination
              --   check (grouped if they are mutual), along with ranges
              --   for problematic call sites.
    	| PropMustBeSingleton
    	| DataMustEndInSort Term
    	| 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
            | DoesNotConstructAnElementOf QName Term -- ^ constructor, type
    	| DifferentArities
    	    -- ^ Varying number of arguments for a function.
    	| WrongHidingInLHS Type
    	    -- ^ 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.
    	| DependentPatternMatchingOnCodata
    	| NotInductive Term
              -- ^ The term does not correspond to an inductive data type.
    	| UninstantiatedDotPattern A.Expr
    	| IlltypedPattern A.Pattern Type
    	| TooManyArgumentsInLHS Nat Type
    	| WrongNumberOfConstructorArguments QName Nat Nat
    	| ShouldBeEmpty Type [Pattern]
    	| ShouldBeASort Type
    	    -- ^ The given type should have been a sort.
    	| ShouldBePi Type
    	    -- ^ The given type should have been a pi.
    	| ShouldBeRecordType Type
    	| NotAProperTerm
    	| UnequalTerms Comparison Term Term Type
    	| UnequalTypes Comparison Type Type
    	| UnequalTelescopes Comparison Telescope Telescope
    	| UnequalHiding Type Type
    	    -- ^ The two function types have different hiding.
    	| UnequalSorts Sort Sort
    	| 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
            | BuiltinMustBeConstructor String A.Expr
    	| NoSuchBuiltinName String
    	| DuplicateBuiltinBinding String Term Term
    	| NoBindingForBuiltin String
    	| NoSuchPrimitiveFunction String
            | ShadowedModule [A.ModuleName]
    	| BuiltinInParameterisedModule String
    	| NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
    	| AbsurdPatternRequiresNoRHS [NamedArg A.Pattern]
    	| TooFewFields QName [C.Name]
    	| TooManyFields QName [C.Name]
    	| DuplicateFields [C.Name]
    	| DuplicateConstructors [C.Name]
    	| UnexpectedWithPatterns [A.Pattern]
    	| WithClausePatternMismatch A.Pattern Pattern
            | FieldOutsideRecord
            | ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
        -- Coverage errors
    	| IncompletePatternMatching Term Args -- can only happen if coverage checking is switched off
            | CoverageFailure QName [[Arg Pattern]]
            | UnreachableClauses QName [[Arg Pattern]]
            | CoverageCantSplitOn QName
            | CoverageCantSplitType Type
        -- Positivity errors
    	| NotStrictlyPositive QName [Occ]
        -- Import errors
    	| LocalVsImportedModuleClash ModuleName
    	| UnsolvedMetas [Range]
    	| UnsolvedConstraints Constraints
    	| CyclicModuleDependency [C.TopLevelModuleName]
    	| FileNotFound C.TopLevelModuleName [AbsolutePath]
            | OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
            | AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
    	| 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]
    	| 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
    	| NothingAppliedToHiddenArg C.Expr
        -- Operator errors
    	| NoParseForApplication [C.Expr]
    	| AmbiguousParseForApplication [C.Expr] [C.Expr]
    	| NoParseForLHS C.Pattern
    	| AmbiguousParseForLHS C.Pattern [C.Pattern]
        -- Usage errors
              deriving (Typeable)

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

    instance Error TypeError where
        noMsg  = strMsg ""
        strMsg = GenericError

    -- | Type-checking errors.

    data TCErr' = TypeError TCState (Closure TypeError)
    	    | Exception Range String
                | IOException Range E.IOException
    	    | PatternErr  TCState -- ^ for pattern violations
    	    | AbortAssign TCState -- ^ used to abort assignment to meta when there are instantiations
      deriving (Typeable)

    -- | Type-checking errors, potentially paired with relevant syntax
    -- highlighting information.

    data TCErr =
      TCErr { errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
              -- ^ The 'ModuleToSource' can be used to map the module
              -- names in the 'HighlightingInfo' to file names.
            , errError        :: TCErr'
            }
      deriving (Typeable)

    instance Error TCErr where
        noMsg  = strMsg ""
        strMsg = TCErr Nothing . Exception noRange . strMsg

    instance Show TCErr where
      show = show . errError

    instance Show TCErr' where
        show (TypeError _ e) = show (getRange $ clTrace e) ++ ": " ++ show (clValue e)
        show (Exception r s) = show r ++ ": " ++ s
        show (IOException r e) = show r ++ ": " ++ show e
        show (PatternErr _)  = "Pattern violation (you shouldn't see this)"
        show (AbortAssign _) = "Abort assignment (you shouldn't see this)"

    instance HasRange TCErr' where
        getRange (TypeError _ cl)  = getRange $ clTrace cl
        getRange (Exception r _)   = r
        getRange (IOException r _) = r
        getRange (PatternErr s)    = getRange $ stTrace s
        getRange (AbortAssign s)   = getRange $ stTrace s

    instance HasRange TCErr where
        getRange = getRange . errError

    instance Exception TCErr

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

    newtype TCMT m a = TCM { unTCM :: StateT TCState
    			          (ReaderT TCEnv m) a
    		       }
        deriving ( MonadState TCState
                 , MonadReader TCEnv
                 )

    type TCM = TCMT IO

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

    instance MonadError TCErr (TCMT IO) where
      throwError = liftIO . throwIO
      catchError m h = TCM $ StateT $ \s -> ReaderT $ \e ->
        runReaderT (runStateT (unTCM m) s) e
        `E.catch` \err -> runReaderT (runStateT (unTCM (h err)) s) e

    mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
    mapTCMT f = TCM . mapStateT (mapReaderT f) . unTCM

    pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
    pureTCM f = TCM $ StateT $ \s -> ReaderT $ \e -> return (f s e, s)

    instance MonadIO m => MonadTCM (TCMT m) where
        liftTCM = mapTCMT liftIO

    instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where
      liftTCM = lift . liftTCM

    instance MonadTrans TCMT where
        lift = TCM . lift . lift

    -- We want a special monad implementation of fail.
    instance MonadIO m => Monad (TCMT m) where
        return  = TCM . return
    --     m >>= k = TCM $ unTCM m >>= unTCM . k
        m >>= k = TCM $ StateT $ \s -> ReaderT $ \e -> do
                    (x, s') <- runReaderT (runStateT (unTCM m) s) e
                    runReaderT (runStateT (unTCM (k x)) s') e
        fail    = internalError

    instance MonadIO m => Functor (TCMT m) where
        fmap = liftM

    instance MonadIO m => Applicative (TCMT m) where
        pure = return
        (<*>) = ap

    instance MonadIO m => MonadIO (TCMT m) where
      liftIO m = TCM $ do r <- gets $ getRange . stTrace
                          liftIO $ wrap r $ do
                            x <- m
                            x `seq` return x
        where
          wrap r m = failOnException handleException
                   $ E.catch m (handleIOException r)

          handleIOException r e = throwIO $ TCErr Nothing $ IOException r e
          handleException   r s = throwIO $ TCErr Nothing $ Exception r s

    patternViolation :: MonadTCM tcm => tcm a
    patternViolation = liftTCM $ do
        s <- get
        throwError $ TCErr Nothing $ PatternErr s

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

    typeError :: MonadTCM tcm => TypeError -> tcm a
    typeError err = liftTCM $ do
        cl <- buildClosure err
        s  <- get
        throwError $ TCErr Nothing $ TypeError s cl

    -- | Running the type checking monad
    runTCM :: TCMT IO a -> IO (Either TCErr a)
    runTCM m = (Right <$> runTCM' m) `E.catch` (return . Left)

    runTCM' :: Monad m => TCMT m a -> m a
    runTCM' m = flip runReaderT initEnv
              $ flip evalStateT initState
              $ unTCM m