{-# 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.Int
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.TypeChecking.CompiledClause

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.Permutation

#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     :: PragmaOptions
           -- ^ Options applying to the current file. @OPTIONS@
           -- pragmas only affect this field.
	 , stStatistics	       :: Statistics
	 , 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     = optPragmaOptions $ defaultOptions
	 , stStatistics	       = Map.empty
	 , 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
        , iPragmaOptions   :: [OptionsPragma]
                              -- ^ Pragma options set in the file.
	}
    deriving (Typeable, Data, Show)

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

data Closure a = Closure { clSignature  :: Signature
			 , clEnv	:: TCEnv
			 , clScope	:: ScopeInfo
			 , 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
    return $ Closure sig env scope x

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

type ConstraintClosure = Closure Constraint

data Constraint = ValueCmp Comparison Type Term Term
                | ArgsCmp [Polarity] Type Args Args
		| TypeCmp Comparison Type Type
                | TelCmp Comparison Telescope Telescope
		| SortCmp Comparison Sort Sort
                | LevelCmp Comparison Term Term
		| 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
                , 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 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 perm j inst ls) =
    MetaVar (mi {clValue = r}) p perm 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
  { defRelevance :: Relevance -- ^ Some defs can be irrelevant (but not hidden).
  , 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
type EpicCode    = 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
            , axEpDef   :: Maybe EpicCode
            }
	  | Function
            { funClauses        :: [Clauses]
            , funCompiled       :: CompiledClauses
            , funInv            :: FunctionInverse
            , funPolarity       :: [Polarity]
            , funArgOccurrences :: [Occurrence]
            , funAbstr          :: IsAbstract
            , funDelayed        :: Delayed
              -- ^ Are the clauses of this definition delayed?
            , funProjection     :: Maybe Int
              -- ^ Is it a record projection?
              --   If yes, then return the 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.
            }
	  | 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            :: QName                -- ^ Constructor name.
            , recNamedCon       :: Bool
            , recConType        :: Type                 -- ^ The record constructor's type.
            , recFields         :: [Arg A.QName]
            , recTel            :: Telescope
            , recPolarity       :: [Polarity]
            , recArgOccurrences :: [Occurrence]
            , recEtaEquality    :: Bool
            , 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?
            }
            -- ^ Note that, currently, the sharp constructor is
            --   represented as a definition ('Def'), but if you look
            --   up the name you will get a @Constructor@.
	  | Primitive
            { primAbstr :: IsAbstract
            , primName  :: String
            , primClauses :: Maybe [Clauses]
              -- ^ 'Nothing' for primitive functions, @'Just'
              -- something@ for builtin functions.
            , primCompiled :: Maybe CompiledClauses
            }
            -- ^ Primitive or builtin functions.
    deriving (Typeable, Data, Show)

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

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

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

data IsReduced = NotReduced | Reduced (Blocked ())
data MaybeReduced a = MaybeRed
  { isReduced     :: IsReduced
  , ignoreReduced :: a
  }

instance Functor MaybeReduced where
  fmap f (MaybeRed r x) = MaybeRed r (f x)

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

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

reduced :: Blocked a -> MaybeReduced a
reduced b = MaybeRed (Reduced $ fmap (const ()) b) (ignoreBlocking b)

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

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

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

-- | 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 Int32
  deriving (Typeable, Data, Eq, Ord, Show, Num)

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

type Statistics = Map String Int

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

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 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.
          , envIrrelevant          :: Bool
                -- ^ Are we checking an irrelevant argument?
                -- Then top-level irrelevant declarations are enabled.
          , 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
          , envEtaContractImplicit :: Bool
                -- ^ it's safe to eta contract implicit lambdas as long as we're
                --   not going to reify and retypecheck (like when doing with
                --   abstraction)
          , envRange :: Range
          , envCall  :: Maybe (Closure Call)
                -- ^ what we're doing at the moment
	  }
    deriving (Typeable, Data)

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

---------------------------------------------------------------------------
-- ** 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, Arg 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
        | IndicesNotConstructorApplications [Arg Term] -- ^ Indices.
        | IndexVariablesNotDistinct [Arg Term] -- ^ Indices.
        | IndexFreeInParameter Nat [Arg Term] -- ^ Index (a variable), parameters.
        | 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.
	| 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
        | SplitOnIrrelevant A.Pattern (Arg Type)
        | DefinitionIsIrrelevant QName
        | VariableIsIrrelevant Name
        | UnequalLevel Comparison Term Term
	| UnequalTerms Comparison Term Term Type
	| UnequalTypes Comparison Type Type
	| UnequalTelescopes Comparison Telescope Telescope
	| UnequalRelevance Type Type
	    -- ^ The two function types have different relevance.
	| 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]
        | 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
	| 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 (envRange $ clEnv 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)  = envRange $ clEnv cl
    getRange (Exception r _)   = r
    getRange (IOException r _) = r
    getRange (PatternErr s)    = noRange
    getRange (AbortAssign s)   = noRange

instance HasRange TCErr where
    getRange = getRange . errError

instance Exception TCErr

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

newtype TCMT m a = TCM { unTCM :: TCState -> TCEnv -> m (a, TCState) }

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

instance MonadIO m => MonadState TCState (TCMT m) where
  get   = TCM $ \s _ -> return (s, s)
  put s = TCM $ \_ _ -> return ((), 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 MonadError TCErr (TCMT IO) where
  throwError = liftIO . throwIO
  catchError m h = TCM $ \s e ->
    unTCM m s e `E.catch` \err -> unTCM (h err) s e

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \s e ->
  unTCM m s e
  `E.catch` \err -> unTCM (h err) (error "catchError_") e

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 :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \s 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 m = TCM $ \s _ -> m >>= \x -> return (x, s)

-- We want a special monad implementation of fail.
{-# SPECIALIZE instance Monad TCM #-}
instance MonadIO m => Monad (TCMT m) where
    return x = TCM $ \s _ -> return (x, s)
    m >>= k = TCM $ \s e -> do
                (x, s') <- unTCM m s e
                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 $ \s e ->
              do let r = envRange e
                 liftIO $ wrap r $ do
                 x <- m
                 x `seq` return (x, s)
    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 = liftM fst (unTCM m initState initEnv)