Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Type checking state

data TCState Source




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.

data PreScopeState Source




stPreTokens :: CompressedFile

Highlighting info for tokens (but not those tokens for which highlighting exists in stSyntaxInfo).

stPreInteractionPoints :: InteractionPoints
stPreImports :: Signature

Imported declared identifiers. Those most not be serialized!

stPreImportedModules :: Set ModuleName
stPreModuleToSource :: ModuleToSource
stPreVisitedModules :: VisitedModules
stPreScope :: ScopeInfo
stPrePatternSyns :: PatternSynDefns

Pattern synonyms of the current file. Serialized.

stPrePatternSynImports :: 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
stPreHaskellImports :: Set String

Imports that should be generated by the compiler (this includes imports from imported modules).

stPreFreshInteractionId :: InteractionId
stPreFreshNameId :: NameId

data PostScopeState Source




stPostSyntaxInfo :: CompressedFile

Highlighting info.

stPostDisambiguatedNames :: !DisambiguatedNames

Disambiguation carried out by the type checker. Maps position of first name character to disambiguated QName for each AmbiguousQName already passed by the type checker.

stPostMetaStore :: MetaStore
stPostInteractionPoints :: InteractionPoints
stPostAwakeConstraints :: Constraints
stPostSleepingConstraints :: Constraints
stPostDirty :: Bool

Dirty when a constraint is added, used to prevent pointer update. Currently unused.

stPostOccursCheckDefs :: Set QName

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.

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.

stPostMutualBlocks :: Map MutualId (Set QName)
stPostLocalBuiltins :: BuiltinThings PrimFun
stPostFreshMetaId :: MetaId
stPostFreshMutualId :: MutualId
stPostFreshCtxId :: CtxId
stPostFreshProblemId :: ProblemId
stPostFreshInt :: Int

data PersistentTCState Source

A part of the state which is not reverted when an error is thrown or the state is reset.




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.

initPersistentState :: PersistentTCState Source

Empty persistent state.

initPreScopeState :: PreScopeState Source

Empty state of type checker.

st-prefixed lenses

Fresh things

fresh :: (HasFresh i, MonadState TCState m) => m i Source

freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name Source

freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name Source

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

class FreshName a where Source

Create a fresh name from a.


freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name Source

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source

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

type SourceToModule = Map AbsolutePath TopLevelModuleName Source

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


data ModuleInfo Source




miInterface :: Interface
miWarnings :: Bool

True if warnings were encountered when the module was type checked.

data Interface Source




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 AtTopLevel and 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
iBuiltin :: BuiltinThings (String, QName)
iHaskellImports :: Set String

Haskell imports listed in (transitively) imported modules are not included here.

iHighlighting :: HighlightingInfo
iPragmaOptions :: [OptionsPragma]

Pragma options set in the file.

iPatternSyns :: PatternSynDefns

iFullHash :: Interface -> Hash Source

Combines the source hash and the (full) hashes of the imported modules.



flipCmp :: CompareDirection -> CompareDirection Source

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

Open things

data Open a Source

A thing tagged with the context it came from.




openThingCtxIds :: [CtxId]
openThing :: a


data Judgement a Source

Parametrized since it is used without MetaId when creating a new meta.




jMetaId :: a
jMetaType :: Type


jMetaId :: a
jMetaType :: Type

Meta variables

data MetaVariable Source




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?

data Frozen Source

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



Do not instantiate.


data MetaInstantiation Source


InstV [Arg String] Term

solved by term (abstracted over some free variables)

InstS Term

solved by Lam .. Sort s




open, to be instantiated as "implicit from scope"

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

data TypeCheckingProblem Source


CheckExpr Expr Type 
CheckArgs ExpandHidden ExpandInstances Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term) 
CheckLambda (Arg ([WithHiding Name], Maybe Type)) 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 Expr.

newtype MetaPriority Source

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.


MetaPriority Int 

data MetaInfo Source

MetaInfo is cloned from one meta to the next during pruning.




miClosRange :: Closure Range
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.

type MetaNameSuggestion = String Source

Name suggestion for meta variable. Empty string means no suggestion.

data NamedMeta Source

For printing, we couple a meta with its name suggestion.

Interaction meta variables

data InteractionPoint Source

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.




ipRange :: Range

The position of the interaction point.

ipMeta :: Maybe MetaId

The meta variable, if any, holding the type etc.

type InteractionPoints = Map InteractionId InteractionPoint Source

Data structure managing the interaction points.


data Section Source




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.

data DisplayForm Source

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




dfFreeVars :: Nat

Number n of free variables in dfRHS.

dfPats :: [Term]

Left hand side patterns, where var 0 stands for a pattern variable. There should be n occurrences of var0 in dfPats.

dfRHS :: DisplayTerm

Right hand side, with n free variables.

data DisplayTerm Source

A structured presentation of a Term for reification into Syntax.


DWithApp DisplayTerm [DisplayTerm] Args

(f vs | ws) us. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Args are additional arguments us (possible in case the with-application is of function type).

DCon ConHead [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term


DTerm Term


defaultDisplayForm :: QName -> [Open DisplayForm] Source

By default, we have no display form.

data NLPat Source

Non-linear (non-constructor) first-order pattern.


PVar !Int

Matches anything (modulo non-linearity).


Matches anything (e.g. irrelevant terms).

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom (Type' NLPat)) (Abs (Type' NLPat))

Matches (x : A) → B

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

data RewriteRule Source

Rewrite rules can be added independently from function clauses.




rewName :: QName

Name of rewrite rule q : Γ → lhs ≡ rhs where is the rewrite relation.

rewContext :: Telescope


rewLHS :: NLPat

Γ ⊢ lhs : t.

rewRHS :: Term

Γ ⊢ rhs : t.

rewType :: Type

Γ ⊢ t.


Show RewriteRule Source 
KillRange RewriteRule Source 
KillRange RewriteRuleMap Source 
Abstract RewriteRule Source

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Apply RewriteRule Source 
PrettyTCM RewriteRule Source 
EmbPrj RewriteRule Source 
InstantiateFull RewriteRule Source 

data Definition Source




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.

defDisplay :: [Open DisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe QName

Just q when this definition is an instance of class q

theDef :: Defn

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source

Create a definition with sensible defaults.

data Polarity Source

Polarity for equality and subtype checking.







no information (mixed variance)



data Projection Source

Additional information for projection Functions.




projProper :: Maybe QName

Nothing if only projection-like, Just q if record projection, where q is the original projection name (current name could be from module app).

projFromType :: QName

Type projected from. Record type if projProper = Just{}.

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.

projDropPars :: Term

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.

projArgInfo :: ArgInfo

The info of the principal (record) argument.

data Defn Source






funClauses :: [Clause]
funCompiled :: Maybe CompiledClauses

Nothing while function is still type-checked. Just cc after type and coverage checking and translation to case trees.

funInv :: FunctionInverse
funMutual :: [QName]

Mutually recursive functions, datas and records. 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.

funStatic :: Bool

Should calls to this function be normalised at compile-time?

funCopy :: Bool

Has this function been created by a module instantiation?

funTerminates :: Maybe Bool

Has this function been termination checked? Did it pass?

funExtLam :: Maybe (Int, Int)

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?



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, datas and records. Does not include this data type.

dataAbstr :: IsAbstract


recPars :: Nat

Number of parameters.

recClause :: Maybe Clause
recConHead :: ConHead

Constructor name and fields.

recNamedCon :: Bool
recConType :: Type

The record constructor's type. (Includes record parameters.)

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, datas and records. Does not include this record.

recEtaEquality :: Bool

Eta-expand at this record type. False for unguarded recursive records and coinductive records.

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. Implies recEtaEquality = False. Projections are not size-preserving.

recAbstr :: IsAbstract


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?


Primitive or builtin functions.


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.

emptyFunction :: Defn Source

A template for creating Function definitions, with sensible defaults.

isEmptyFunction :: Defn -> Bool Source

Checking whether we are dealing with a function yet to be defined.

newtype Fields Source


Fields [(Name, Type)] 


data Simplification Source

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 Reduced no yes Source


data IsReduced Source

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.


Reduced (Blocked ()) 

data AllowedReduction Source

Controlling reduce.



(Projection and) projection-like functions may be reduced.


Functions which are not projections may be reduced.


Reduce Level terms.


Functions that have not passed termination checking.

allReductions :: AllowedReductions Source

Not quite all reductions (skip non-terminating reductions)

defDelayed :: Definition -> Delayed Source

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool Source

Has the definition failed the termination checker?

defCopy :: Definition -> Bool Source

Is the definition just a copy created by a module instantiation?

defAbstract :: Definition -> IsAbstract Source

Beware when using this function on a def obtained with getConstInfo q! If the identifier q is abstract, getConstInfo will turn its def into an Axiom and you always get ConcreteDef, paradoxically. Use it in IgnoreAbstractMode, like this: a ignoreAbstractMode $ defAbstract <$ getConstInfo q


Mutual blocks



Instance table

type InstanceTable = Map QName [QName] Source

The instance table is a Map associating to every name of recorddata typepostulate its list of instances

type TempInstanceTable = (InstanceTable, [QName]) Source

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.

Builtin things

data BuiltinDescriptor Source


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.

Highlighting levels

data HighlightingLevel Source

How much highlighting should be sent to the user interface?



This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

data HighlightingMethod Source

How should highlighting be sent to the user interface?



Via stdout.


Both via files and via stdout.

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source

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

Type checking environment

data TCEnv Source




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 :: [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?

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.

envColors :: [Color]
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
envHighlightingRange :: Range

Interactive highlighting uses this range rather than envRange.

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 :: Integer

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

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.

envReifyUnquoted :: Bool

The rules for translating internal to abstract syntax are slightly different when the internal term comes from an unquote.


MonadReader TCEnv ReduceM Source 
MonadReader TCEnv TerM 
MonadReader TCEnv Unify 
MonadIO m => MonadReader TCEnv (TCMT m) Source 


type Context = [ContextEntry] Source

The Context is a stack of ContextEntrys.

data ContextEntry Source




ctxId :: CtxId
ctxEntry :: Dom (Name, Type)

Let bindings

Abstract mode

data AbstractMode Source



Abstract things in the current module can be accessed.


No abstract things can be accessed.


All abstract things can be accessed.

Insertion of implicit arguments

data ExpandHidden Source



Add implicit arguments in the end until type is no longer hidden Pi.


Do not append implicit arguments.

Type checking errors

data CallInfo Source

Information about a call.




callInfoTarget :: QName

Target function name.

callInfoRange :: Range

Range of the target function.

callInfoCall :: Closure Term

To be formatted representation of the call.


data TerminationError Source

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




termErrFunctions :: [QName]

The functions which failed to check. (May not include automatically generated functions.)

termErrCalls :: [CallInfo]

The problematic call sites.

data SplitError Source

Error when splitting a pattern variable into possible constructor patterns.


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



cantSplitConName :: QName


cantSplitTel :: Telescope

Context for indices.

cantSplitConIdx :: Args

Inferred indices (from type of constructor).

cantSplitGivenIdx :: Args

Expected indices (from checking pattern).

GenericSplitError String 

data TypeError Source


InternalError String 
NotImplemented String 
NotSupported String 
CompilationError String 
TerminationCheckFailed [TerminationError] 
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]


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


Varying number of arguments for a function.


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

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.

ColorMismatch [Color] [Color]

The given color does not correspond to the expected color.

NotInductive Term

The term does not correspond to an inductive data type.

UninstantiatedDotPattern Expr 
IlltypedPattern Pattern Type 
IllformedProjectionPattern Pattern 
CannotEliminateWithPattern (NamedArg Pattern) Type 
TooManyArgumentsInLHS 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 
ShouldBeRecordPattern Pattern 
NotAProjectionPattern (NamedArg Pattern) 
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 Pattern (Dom Type) 
DefinitionIsIrrelevant QName 
VariableIsIrrelevant Name 
UnequalTerms Comparison Term Term Type 
UnequalTypes Comparison Type Type 
UnequalRelevance Comparison Term Term

The two function types have different relevance.

UnequalHiding Term Term

The two function types have different hiding.

UnequalColors Term Term

The two function types have different color.

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 Expr 
NoSuchBuiltinName String 
DuplicateBuiltinBinding String Term Term 
NoBindingForBuiltin String 
NoSuchPrimitiveFunction String 
ShadowedModule Name [ModuleName] 
BuiltinInParameterisedModule String 
IllegalLetInTelescope TypedBinding 
NoRHSRequiresAbsurdPattern [NamedArg Pattern] 
AbsurdPatternRequiresNoRHS [NamedArg Pattern] 
TooFewFields QName [Name] 
TooManyFields QName [Name] 
DuplicateFields [Name] 
DuplicateConstructors [Name] 
WithOnFreeVariable Expr 
UnexpectedWithPatterns [Pattern] 
WithClausePatternMismatch Pattern Pattern 
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] 
IncompletePatternMatching Term [Elim] 
CoverageFailure QName [[Arg Pattern]] 
UnreachableClauses QName [[Arg Pattern]] 
CoverageCantSplitOn QName Telescope Args Args 
CoverageCantSplitIrrelevantType Type 
CoverageCantSplitType Type 
WithoutKError Type Term Term 
SplitError SplitError 
NotStrictlyPositive QName [Occ] 
LocalVsImportedModuleClash ModuleName 
UnsolvedMetas [Range] 
UnsolvedConstraints Constraints 

Some interaction points (holes) have not be 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 [TopLevelModuleName] 
FileNotFound TopLevelModuleName [AbsolutePath] 
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName 
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] 
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] 
ClashingFileNamesFor ModuleName [AbsolutePath] 
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath

Module name, file from which it was loaded, file which the include path says contains the module. Scope errors

NotInScope [QName] 
NoSuchModule QName 
AmbiguousName QName [QName] 
AmbiguousModule QName [ModuleName] 
UninstantiatedModule QName 
ClashingDefinition QName QName 
ClashingModule ModuleName ModuleName 
ClashingImport Name QName 
ClashingModuleImport Name ModuleName 
PatternShadowsConstructor Name QName 
ModuleDoesntExport QName [ImportedName] 
DuplicateImports QName [ImportedName] 
InvalidPattern Pattern 
RepeatedVariablesInPattern [Name] 
NotAModuleExpr 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 Expr 
NotAValidLetBinding NiceDeclaration 
NothingAppliedToHiddenArg Expr 
NothingAppliedToInstanceArg Expr 
BadArgumentsToPatternSynonym QName 
TooFewArgumentsToPatternSynonym QName 
NoParseForApplication [Expr] 
AmbiguousParseForApplication [Expr] [Expr] 
NoParseForLHS LHSOrPatSyn Pattern 
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] 
IFSNoCandidateInScope Type 
UnquoteFailed UnquoteError 
SafeFlagPostulate Name 
SafeFlagPragma [String] 


data LHSOrPatSyn Source

Distinguish error message when parsing lhs or pattern synonym, resp.



The reduce monad

data ReduceEnv Source

Environment of the reduce monad.




redEnv :: TCEnv

Read only access to environment.

redSt :: TCState

Read only access to state (signature, metas...).

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source

Type checking monad transformer

newtype TCMT m a Source




unTCM :: IORef TCState -> TCEnv -> m a


MonadTrans TCMT Source 
MonadError TCErr IM Source 
MonadBench Phase TCM Source

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

MonadIO m => MonadState TCState (TCMT m) Source 
MonadIO m => MonadReader TCEnv (TCMT m) Source 
MonadError TCErr (TCMT IO) Source 
MonadIO m => Monad (TCMT m) Source 
MonadIO m => Functor (TCMT m) Source 
MonadIO m => Applicative (TCMT m) Source 
Monoid (TCM Any) Source

Short-cutting disjunction forms a monoid.

MonadIO m => MonadIO (TCMT m) Source 
Null (TCM Doc) Source 
MonadIO m => MonadTCM (TCMT m) Source 
MonadIO m => HasBuiltins (TCMT m) Source 
MonadIO m => HasOptions (TCMT m) Source 
HasConstInfo (TCMT IO) Source 

type TCM = TCMT IO Source

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where Source


liftTCM :: TCM a -> tcm a Source


type IM = TCMT (InputT IO) Source

Interaction monad.

runIM :: IM a -> TCM a Source

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a Source

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.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a Source

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a Source

returnTCMT :: MonadIO m => a -> TCMT m a Source

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b Source

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b Source

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b Source

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b Source

internalError :: MonadTCM tcm => String -> tcm a Source

genericError :: MonadTCM tcm => String -> tcm a Source

typeError :: MonadTCM tcm => TypeError -> tcm a Source

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) Source

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a Source

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source

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

forkTCM :: TCM a -> TCM () Source

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.

extendedLambdaName :: String Source

Base name for extended lambda patterns

absurdLambdaName :: String Source

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool Source

Check whether we have an definition from an absurd lambda.

KillRange instances