Agda.TypeChecking.Monad.Base

Contents

• Type checking state
• st-prefixed lenses
• Fresh things
  • Managing file names
  • Interface
  • Closure
  • Constraints
• Open things
• Judgements
  • Meta variables
  • Interaction meta variables
  • Signature
  • Injectivity
  • Mutual blocks
  • Statistics
  • Trace
  • Instance table
  • Builtin things
• Highlighting levels
• Type checking environment
  • Context
  • Let bindings
  • Abstract mode
  • Insertion of implicit arguments
• Type checking errors
• The reduce monad
• Type checking monad transformer
• KillRange instances

Synopsis

• data TCState = TCSt {
  • stPreScopeState :: !PreScopeState
  • stPostScopeState :: !PostScopeState
  • stPersistentState :: !PersistentTCState
  }
• class Monad m => ReadTCState m where
• data PreScopeState = PreScopeState {
  • stPreTokens :: CompressedFile
  • stPreImports :: Signature
  • stPreImportedModules :: Set ModuleName
  • stPreModuleToSource :: ModuleToSource
  • stPreVisitedModules :: VisitedModules
  • stPreScope :: ScopeInfo
  • stPrePatternSyns :: PatternSynDefns
  • stPrePatternSynImports :: PatternSynDefns
  • stPrePragmaOptions :: PragmaOptions
  • stPreImportedBuiltins :: BuiltinThings PrimFun
  • stPreHaskellImports :: Set String
  • stPreHaskellImportsUHC :: Set String
  • stPreHaskellCode :: [String]
  • stPreFreshInteractionId :: !InteractionId
  }
• type DisambiguatedNames = IntMap QName
• data PostScopeState = PostScopeState {
  • stPostSyntaxInfo :: CompressedFile
  • stPostDisambiguatedNames :: !DisambiguatedNames
  • stPostMetaStore :: MetaStore
  • stPostInteractionPoints :: InteractionPoints
  • stPostAwakeConstraints :: Constraints
  • stPostSleepingConstraints :: Constraints
  • stPostDirty :: Bool
  • stPostOccursCheckDefs :: Set QName
  • stPostSignature :: Signature
  • stPostImportsDisplayForms :: !DisplayForms
  • stPostImportedDisplayForms :: !DisplayForms
  • stPostCurrentModule :: Maybe ModuleName
  • stPostInstanceDefs :: TempInstanceTable
  • stPostStatistics :: Statistics
  • stPostMutualBlocks :: Map MutualId (Set QName)
  • stPostLocalBuiltins :: BuiltinThings PrimFun
  • stPostFreshMetaId :: MetaId
  • stPostFreshMutualId :: MutualId
  • stPostFreshCtxId :: CtxId
  • stPostFreshProblemId :: ProblemId
  • stPostFreshInt :: Int
  • stPostFreshNameId :: NameId
  }
• data PersistentTCState = PersistentTCSt {
  • stDecodedModules :: DecodedModules
  • stPersistentOptions :: CommandLineOptions
  • stInteractionOutputCallback :: InteractionOutputCallback
  • stBenchmark :: !Benchmark
  • stAccumStatistics :: !Statistics
  • stLoadedFileCache :: !(Maybe LoadedFileCache)
  }
• data LoadedFileCache = LoadedFileCache {
  • lfcCached :: !CachedTypeCheckLog
  • lfcCurrent :: !CurrentTypeCheckLog
  }
• type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
• type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
• data TypeCheckAction
  • = EnterSection !ModuleInfo !ModuleName ![TypedBindings]
  • | LeaveSection !ModuleName
  • | Decl !Declaration
  • | Pragmas !PragmaOptions
• initPersistentState :: PersistentTCState
• initPreScopeState :: PreScopeState
• initPostScopeState :: PostScopeState
• initState :: TCState
• stTokens :: Lens' CompressedFile TCState
• stImports :: Lens' Signature TCState
• stImportedModules :: Lens' (Set ModuleName) TCState
• stModuleToSource :: Lens' ModuleToSource TCState
• stVisitedModules :: Lens' VisitedModules TCState
• stScope :: Lens' ScopeInfo TCState
• stPatternSyns :: Lens' PatternSynDefns TCState
• stPatternSynImports :: Lens' PatternSynDefns TCState
• stPragmaOptions :: Lens' PragmaOptions TCState
• stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
• stHaskellImports :: Lens' (Set String) TCState
• stHaskellImportsUHC :: Lens' (Set String) TCState
• stHaskellCode :: Lens' [String] TCState
• stFreshInteractionId :: Lens' InteractionId TCState
• stFreshNameId :: Lens' NameId TCState
• stSyntaxInfo :: Lens' CompressedFile TCState
• stDisambiguatedNames :: Lens' DisambiguatedNames TCState
• stMetaStore :: Lens' MetaStore TCState
• stInteractionPoints :: Lens' InteractionPoints TCState
• stAwakeConstraints :: Lens' Constraints TCState
• stSleepingConstraints :: Lens' Constraints TCState
• stDirty :: Lens' Bool TCState
• stOccursCheckDefs :: Lens' (Set QName) TCState
• stSignature :: Lens' Signature TCState
• stImportsDisplayForms :: Lens' DisplayForms TCState
• stImportedDisplayForms :: Lens' DisplayForms TCState
• stCurrentModule :: Lens' (Maybe ModuleName) TCState
• stInstanceDefs :: Lens' TempInstanceTable TCState
• stStatistics :: Lens' Statistics TCState
• stMutualBlocks :: Lens' (Map MutualId (Set QName)) TCState
• stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
• stFreshMetaId :: Lens' MetaId TCState
• stFreshMutualId :: Lens' MutualId TCState
• stFreshCtxId :: Lens' CtxId TCState
• stFreshProblemId :: Lens' ProblemId TCState
• stFreshInt :: Lens' Int TCState
• stBuiltinThings :: TCState -> BuiltinThings PrimFun
• class Enum i => HasFresh i where
• nextFresh :: HasFresh i => TCState -> (i, TCState)
• fresh :: (HasFresh i, MonadState TCState m) => m i
• newtype ProblemId = ProblemId Nat
• freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name
• freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name
• freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name
• class FreshName a where
• type ModuleToSource = Map TopLevelModuleName AbsolutePath
• type SourceToModule = Map AbsolutePath TopLevelModuleName
• sourceToModule :: TCM SourceToModule
• data ModuleInfo = ModuleInfo {
  • miInterface :: Interface
  • miWarnings :: Bool
  }
• type VisitedModules = Map TopLevelModuleName ModuleInfo
• type DecodedModules = Map TopLevelModuleName Interface
• data Interface = Interface {
  • iSourceHash :: Hash
  • iImportedModules :: [(ModuleName, Hash)]
  • iModuleName :: ModuleName
  • iScope :: Map ModuleName Scope
  • iInsideScope :: ScopeInfo
  • iSignature :: Signature
  • iDisplayForms :: DisplayForms
  • iBuiltin :: BuiltinThings (String, QName)
  • iHaskellImports :: Set String
  • iHaskellImportsUHC :: Set String
  • iHaskellCode :: [String]
  • iHighlighting :: HighlightingInfo
  • iPragmaOptions :: [OptionsPragma]
  • iPatternSyns :: PatternSynDefns
  }
• iFullHash :: Interface -> Hash
• data Closure a = Closure {
  • clSignature :: Signature
  • clEnv :: TCEnv
  • clScope :: ScopeInfo
  • clValue :: a
  }
• buildClosure :: a -> TCM (Closure a)
• type Constraints = [ProblemConstraint]
• data ProblemConstraint = PConstr {
  • constraintProblems :: [ProblemId]
  • theConstraint :: Closure Constraint
  }
• data Constraint
  • = ValueCmp Comparison Type Term Term
  • | ElimCmp [Polarity] Type Term [Elim] [Elim]
  • | TypeCmp Comparison Type Type
  • | TelCmp Type Type Comparison Telescope Telescope
  • | SortCmp Comparison Sort Sort
  • | LevelCmp Comparison Level Level
  • | UnBlock MetaId
  • | Guarded Constraint ProblemId
  • | IsEmpty Range Type
  • | CheckSizeLtSat Term
  • | FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])
• data Comparison
  • = CmpEq
  • | CmpLeq
• data CompareDirection
  • = DirEq
  • | DirLeq
  • | DirGeq
• fromCmp :: Comparison -> CompareDirection
• flipCmp :: CompareDirection -> CompareDirection
• dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
• data Open a = OpenThing {
  • openThingCtxIds :: [CtxId]
  • openThing :: a
  }
• data Judgement a
  • = HasType {
    • jMetaId :: a
    • jMetaType :: Type
    }
  • | IsSort {
    • jMetaId :: a
    • jMetaType :: Type
    }
• data MetaVariable = MetaVar {
  • mvInfo :: MetaInfo
  • mvPriority :: MetaPriority
  • mvPermutation :: Permutation
  • mvJudgement :: Judgement MetaId
  • mvInstantiation :: MetaInstantiation
  • mvListeners :: Set Listener
  • mvFrozen :: Frozen
  }
• data Listener
  • = EtaExpand MetaId
  • | CheckConstraint Nat ProblemConstraint
• data Frozen
  • = Frozen
  • | Instantiable
• data MetaInstantiation
  • = InstV [Arg String] Term
  • | InstS Term
  • | Open
  • | OpenIFS
  • | BlockedConst Term
  • | PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
• data TypeCheckingProblem
  • = CheckExpr Expr Type
  • | CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term)
  • | CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type
  • | UnquoteTactic Term Term Type
• newtype MetaPriority = MetaPriority Int
• data RunMetaOccursCheck
  • = RunMetaOccursCheck
  • | DontRunMetaOccursCheck
• data MetaInfo = MetaInfo {
  • miClosRange :: Closure Range
  • miMetaOccursCheck :: RunMetaOccursCheck
  • miNameSuggestion :: MetaNameSuggestion
  }
• type MetaNameSuggestion = String
• data NamedMeta = NamedMeta {
  • nmSuggestion :: MetaNameSuggestion
  • nmid :: MetaId
  }
• type MetaStore = Map MetaId MetaVariable
• normalMetaPriority :: MetaPriority
• lowMetaPriority :: MetaPriority
• highMetaPriority :: MetaPriority
• getMetaInfo :: MetaVariable -> Closure Range
• getMetaScope :: MetaVariable -> ScopeInfo
• getMetaEnv :: MetaVariable -> TCEnv
• getMetaSig :: MetaVariable -> Signature
• getMetaRelevance :: MetaVariable -> Relevance
• data InteractionPoint = InteractionPoint {
  • ipRange :: Range
  • ipMeta :: Maybe MetaId
  }
• type InteractionPoints = Map InteractionId InteractionPoint
• data Signature = Sig {
  • _sigSections :: Sections
  • _sigDefinitions :: Definitions
  • _sigRewriteRules :: RewriteRuleMap
  }
• sigSections :: Lens' Sections Signature
• sigDefinitions :: Lens' Definitions Signature
• sigRewriteRules :: Lens' RewriteRuleMap Signature
• type Sections = Map ModuleName Section
• type Definitions = HashMap QName Definition
• type RewriteRuleMap = HashMap QName RewriteRules
• type DisplayForms = HashMap QName [Open DisplayForm]
• data Section = Section {
  • _secTelescope :: Telescope
  }
• secTelescope :: Lens' Telescope Section
• emptySignature :: Signature
• data DisplayForm = Display {
  • dfFreeVars :: Nat
  • dfPats :: [Term]
  • dfRHS :: DisplayTerm
  }
• data DisplayTerm
  • = DWithApp DisplayTerm [DisplayTerm] Args
  • | DCon ConHead [Arg DisplayTerm]
  • | DDef QName [Elim' DisplayTerm]
  • | DDot Term
  • | DTerm Term
• defaultDisplayForm :: QName -> [Open DisplayForm]
• defRelevance :: Definition -> Relevance
• data NLPat
  • = PVar (Maybe CtxId) !Int
  • | PWild
  • | PDef QName PElims
  • | PLam ArgInfo (Abs NLPat)
  • | PPi (Dom (Type' NLPat)) (Abs (Type' NLPat))
  • | PBoundVar !Int PElims
  • | PTerm Term
• type PElims = [Elim' NLPat]
• type RewriteRules = [RewriteRule]
• data RewriteRule = RewriteRule {
  • rewName :: QName
  • rewContext :: Telescope
  • rewLHS :: NLPat
  • rewRHS :: Term
  • rewType :: Type
  }
• data Definition = Defn {
  • defArgInfo :: ArgInfo
  • defName :: QName
  • defType :: Type
  • defPolarity :: [Polarity]
  • defArgOccurrences :: [Occurrence]
  • defDisplay :: [Open DisplayForm]
  • defMutual :: MutualId
  • defCompiledRep :: CompiledRepresentation
  • defInstance :: Maybe QName
  • defCopy :: Bool
  • theDef :: Defn
  }
• defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
• type HaskellCode = String
• type HaskellType = String
• type EpicCode = String
• type JSCode = Exp
• data HaskellRepresentation
  • = HsDefn HaskellType HaskellCode
  • | HsType HaskellType
• data HaskellExport = HsExport HaskellType String
• data CoreRepresentation
  • = CrDefn CoreExpr
  • | CrType CoreType
  • | CrConstr CoreConstr
• data Polarity
  • = Covariant
  • | Contravariant
  • | Invariant
  • | Nonvariant
• data CompiledRepresentation = CompiledRep {
  • compiledHaskell :: Maybe HaskellRepresentation
  • exportHaskell :: Maybe HaskellExport
  • compiledEpic :: Maybe EpicCode
  • compiledJS :: Maybe JSCode
  • compiledCore :: Maybe CoreRepresentation
  }
• noCompiledRep :: CompiledRepresentation
• data ExtLamInfo = ExtLamInfo {
  • extLamNumHidden :: Int
  • extLamNumNonHid :: Int
  }
• data Projection = Projection {
  • projProper :: Maybe QName
  • projFromType :: QName
  • projIndex :: Int
  • projDropPars :: Term
  • projArgInfo :: ArgInfo
  }
• data EtaEquality
  • = Specified !Bool
  • | Inferred !Bool
• etaEqualityToBool :: EtaEquality -> Bool
• setEtaEquality :: EtaEquality -> Bool -> EtaEquality
• data Defn
  • = Axiom
  • | Function {
    • funClauses :: [Clause]
    • funCompiled :: Maybe CompiledClauses
    • funTreeless :: Maybe Compiled
    • funInv :: FunctionInverse
    • funMutual :: [QName]
    • funAbstr :: IsAbstract
    • funDelayed :: Delayed
    • funProjection :: Maybe Projection
    • funStatic :: Bool
    • funInline :: Bool
    • funSmashable :: Bool
    • funTerminates :: Maybe Bool
    • funExtLam :: Maybe ExtLamInfo
    • funWith :: Maybe QName
    • funCopatternLHS :: Bool
    }
  • | Datatype {
    • dataPars :: Nat
    • dataSmallPars :: Permutation
    • dataNonLinPars :: Drop Permutation
    • dataIxs :: Nat
    • dataInduction :: Induction
    • dataClause :: Maybe Clause
    • dataCons :: [QName]
    • dataSort :: Sort
    • dataMutual :: [QName]
    • dataAbstr :: IsAbstract
    }
  • | Record {
    • recPars :: Nat
    • recClause :: Maybe Clause
    • recConHead :: ConHead
    • recNamedCon :: Bool
    • recConType :: Type
    • recFields :: [Arg QName]
    • recTel :: Telescope
    • recMutual :: [QName]
    • recEtaEquality' :: EtaEquality
    • recInduction :: Maybe Induction
    • recRecursive :: Bool
    • recAbstr :: IsAbstract
    }
  • | Constructor {
    • conPars :: Nat
    • conSrcCon :: ConHead
    • conData :: QName
    • conAbstr :: IsAbstract
    • conInd :: Induction
    }
  • | Primitive {
    • primAbstr :: IsAbstract
    • primName :: String
    • primClauses :: [Clause]
    • primCompiled :: Maybe CompiledClauses
    }
• recEtaEquality :: Defn -> Bool
• emptyFunction :: Defn
• isEmptyFunction :: Defn -> Bool
• isCopatternLHS :: [Clause] -> Bool
• recCon :: Defn -> QName
• defIsRecord :: Defn -> Bool
• defIsDataOrRecord :: Defn -> Bool
• newtype Fields = Fields [(Name, Type)]
• data Simplification
  • = YesSimplification
  • | NoSimplification
• data Reduced no yes
  • = NoReduction no
  • | YesReduction Simplification yes
• data IsReduced
  • = NotReduced
  • | Reduced (Blocked ())
• data MaybeReduced a = MaybeRed {
  • isReduced :: IsReduced
  • ignoreReduced :: a
  }
• type MaybeReducedArgs = [MaybeReduced (Arg Term)]
• type MaybeReducedElims = [MaybeReduced Elim]
• notReduced :: a -> MaybeReduced a
• reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
• data AllowedReduction
  • = ProjectionReductions
  • | InlineReductions
  • | CopatternReductions
  • | FunctionReductions
  • | LevelReductions
  • | NonTerminatingReductions
• type AllowedReductions = [AllowedReduction]
• allReductions :: AllowedReductions
• data PrimFun = PrimFun {
  • primFunName :: QName
  • primFunArity :: Arity
  • primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
  }
• defClauses :: Definition -> [Clause]
• defCompiled :: Definition -> Maybe CompiledClauses
• defParameters :: Definition -> Maybe Nat
• defJSDef :: Definition -> Maybe JSCode
• defEpicDef :: Definition -> Maybe EpicCode
• defCoreDef :: Definition -> Maybe CoreRepresentation
• defDelayed :: Definition -> Delayed
• defNonterminating :: Definition -> Bool
• defAbstract :: Definition -> IsAbstract
• type FunctionInverse = FunctionInverse' Clause
• data FunctionInverse' c
  • = NotInjective
  • | Inverse (Map TermHead c)
• data TermHead
  • = SortHead
  • | PiHead
  • | ConsHead QName
• newtype MutualId = MutId Int32
• type Statistics = Map String Integer
• data Call
  • = CheckClause Type SpineClause
  • | CheckPattern Pattern Telescope Type
  • | CheckLetBinding LetBinding
  • | InferExpr Expr
  • | CheckExprCall Expr Type
  • | CheckDotPattern Expr Term
  • | CheckPatternShadowing SpineClause
  • | CheckProjection Range QName Type
  • | IsTypeCall Expr Sort
  • | IsType_ Expr
  • | InferVar Name
  • | InferDef Range QName
  • | CheckArguments Range [NamedArg Expr] Type Type
  • | CheckDataDef Range Name [LamBinding] [Constructor]
  • | CheckRecDef Range Name [LamBinding] [Constructor]
  • | CheckConstructor QName Telescope Sort Constructor
  • | CheckFunDef Range Name [Clause]
  • | CheckPragma Range Pragma
  • | CheckPrimitive Range Name Expr
  • | CheckIsEmpty Range Type
  • | CheckWithFunctionType Expr
  • | CheckSectionApplication Range ModuleName ModuleApplication
  • | ScopeCheckExpr Expr
  • | ScopeCheckDeclaration NiceDeclaration
  • | ScopeCheckLHS QName Pattern
  • | NoHighlighting
  • | ModuleContents
  • | SetRange Range
• type InstanceTable = Map QName [QName]
• type TempInstanceTable = (InstanceTable, [QName])
• data BuiltinDescriptor
  • = BuiltinData (TCM Type) [String]
  • | BuiltinDataCons (TCM Type)
  • | BuiltinPrim String (Term -> TCM ())
  • | BuiltinPostulate Relevance (TCM Type)
  • | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
• data BuiltinInfo = BuiltinInfo {
  • builtinName :: String
  • builtinDesc :: BuiltinDescriptor
  }
• type BuiltinThings pf = Map String (Builtin pf)
• data Builtin pf
  • = Builtin Term
  • | Prim pf
• data HighlightingLevel
  • = None
  • | NonInteractive
  • | Interactive
• data HighlightingMethod
  • = Direct
  • | Indirect
• ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
• data TCEnv = TCEnv {
  • envContext :: Context
  • envLetBindings :: LetBindings
  • envCurrentModule :: ModuleName
  • envCurrentPath :: Maybe AbsolutePath
  • envAnonymousModules :: [(ModuleName, Nat)]
  • envImportPath :: [TopLevelModuleName]
  • envMutualBlock :: Maybe MutualId
  • envTerminationCheck :: TerminationCheck ()
  • envSolvingConstraints :: Bool
  • envCheckingWhere :: Bool
  • envAssignMetas :: Bool
  • envActiveProblems :: [ProblemId]
  • envAbstractMode :: AbstractMode
  • envRelevance :: Relevance
  • envDisplayFormsEnabled :: Bool
  • envReifyInteractionPoints :: Bool
  • envEtaContractImplicit :: Bool
  • envRange :: Range
  • envHighlightingRange :: Range
  • envCall :: Maybe (Closure Call)
  • envHighlightingLevel :: HighlightingLevel
  • envHighlightingMethod :: HighlightingMethod
  • envModuleNestingLevel :: Integer
  • envAllowDestructiveUpdate :: Bool
  • envExpandLast :: ExpandHidden
  • envAppDef :: Maybe QName
  • envSimplification :: Simplification
  • envAllowedReductions :: AllowedReductions
  • envCompareBlocked :: Bool
  • envPrintDomainFreePi :: Bool
  • envInsideDotPattern :: Bool
  }
• initEnv :: TCEnv
• disableDestructiveUpdate :: TCM a -> TCM a
• type Context = [ContextEntry]
• data ContextEntry = Ctx {
  • ctxId :: CtxId
  • ctxEntry :: Dom (Name, Type)
  }
• newtype CtxId = CtxId Nat
• type LetBindings = Map Name (Open (Term, Dom Type))
• data AbstractMode
  • = AbstractMode
  • | ConcreteMode
  • | IgnoreAbstractMode
• data ExpandHidden
  • = ExpandLast
  • | DontExpandLast
• data ExplicitToInstance
  • = ExplicitToInstance
  • | ExplicitStayExplicit
• data Candidate = Candidate {
  • candidateTerm :: Term
  • candidateType :: Type
  • candidateEti :: ExplicitToInstance
  }
• data Occ
  • = OccCon {
    • occDatatype :: QName
    • occConstructor :: QName
    • occPosition :: OccPos
    }
  • | OccClause {
    • occFunction :: QName
    • occClause :: Int
    • occPosition :: OccPos
    }
• data OccPos
  • = NonPositively
  • | ArgumentTo Nat QName
• data CallInfo = CallInfo {
  • callInfoTarget :: QName
  • callInfoRange :: Range
  • callInfoCall :: Closure Term
  }
• data TerminationError = TerminationError {
  • termErrFunctions :: [QName]
  • termErrCalls :: [CallInfo]
  }
• data SplitError
  • = NotADatatype (Closure Type)
  • | IrrelevantDatatype (Closure Type)
  • | CoinductiveDatatype (Closure Type)
  • | CantSplit {
    • cantSplitConName :: QName
    • cantSplitTel :: Telescope
    • cantSplitConIdx :: Args
    • cantSplitGivenIdx :: Args
    }
  • | GenericSplitError String
• data UnquoteError
  • = BadVisibility String (Arg Term)
  • | ConInsteadOfDef QName String String
  • | DefInsteadOfCon QName String String
  • | NonCanonical String Term
  • | BlockedOnMeta TCState MetaId
  • | UnquotePanic String
• data TypeError
  • = InternalError String
  • | NotImplemented String
  • | NotSupported String
  • | CompilationError String
  • | TerminationCheckFailed [TerminationError]
  • | PropMustBeSingleton
  • | DataMustEndInSort Term
  • | ShouldEndInApplicationOfTheDatatype Type
  • | ShouldBeAppliedToTheDatatypeParameters Term Term
  • | ShouldBeApplicationOf Type QName
  • | ConstructorPatternInWrongDatatype QName QName
  • | IndicesNotConstructorApplications [Arg Term]
  • | IndexVariablesNotDistinct [Nat] [Arg Term]
  • | IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
  • | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
  • | DoesNotConstructAnElementOf QName Type
  • | DifferentArities
  • | WrongHidingInLHS
  • | WrongHidingInLambda Type
  • | WrongHidingInApplication Type
  • | WrongNamedArgument (NamedArg Expr)
  • | WrongIrrelevanceInLambda Type
  • | WrongInstanceDeclaration
  • | HidingMismatch Hiding Hiding
  • | RelevanceMismatch Relevance Relevance
  • | NotInductive Term
  • | UninstantiatedDotPattern Expr
  • | IlltypedPattern Pattern Type
  • | IllformedProjectionPattern Pattern
  • | CannotEliminateWithPattern (NamedArg Pattern) Type
  • | TooManyArgumentsInLHS Type
  • | WrongNumberOfConstructorArguments QName Nat Nat
  • | ShouldBeEmpty Type [Pattern]
  • | ShouldBeASort Type
  • | ShouldBePi Type
  • | ShouldBeRecordType Type
  • | ShouldBeRecordPattern Pattern
  • | NotAProjectionPattern (NamedArg Pattern)
  • | NotAProperTerm
  • | SetOmegaNotValidType
  • | InvalidTypeSort Sort
  • | InvalidType Term
  • | FunctionTypeInSizeUniv Term
  • | SplitOnIrrelevant Pattern (Dom Type)
  • | DefinitionIsIrrelevant QName
  • | VariableIsIrrelevant Name
  • | UnequalTerms Comparison Term Term Type
  • | UnequalTypes Comparison Type Type
  • | UnequalRelevance Comparison Term Term
  • | UnequalHiding Term Term
  • | UnequalSorts Sort Sort
  • | UnequalBecauseOfUniverseConflict Comparison Term Term
  • | HeterogeneousEquality Term Type Term Type
  • | NotLeqSort Sort Sort
  • | MetaCannotDependOn MetaId [Nat] Nat
  • | 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
  • | FieldOutsideRecord
  • | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
  • | IncompletePatternMatching Term [Elim]
  • | CoverageFailure QName [[Arg DeBruijnPattern]]
  • | UnreachableClauses QName [[Arg DeBruijnPattern]]
  • | CoverageCantSplitOn QName Telescope Args Args
  • | CoverageCantSplitIrrelevantType Type
  • | CoverageCantSplitType Type
  • | CoverageNoExactSplit QName Clause
  • | WithoutKError Type Term Term
  • | UnifyConflict ConHead ConHead
  • | UnifyCycle Int Term
  • | UnifyIndicesNotVars Type Term Term Args
  • | UnificationRecursiveEq Type Int Term
  • | UnificationStuck Telescope [Term] [Term]
  • | SplitError SplitError
  • | NotStrictlyPositive QName [Occ]
  • | LocalVsImportedModuleClash ModuleName
  • | UnsolvedMetas [Range]
  • | UnsolvedConstraints Constraints
  • | SolvedButOpenHoles
  • | CyclicModuleDependency [TopLevelModuleName]
  • | FileNotFound TopLevelModuleName [AbsolutePath]
  • | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
  • | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
  • | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
  • | ClashingFileNamesFor ModuleName [AbsolutePath]
  • | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
  • | BothWithAndRHS
  • | 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
  • | NotAnExpression Expr
  • | NotAValidLetBinding NiceDeclaration
  • | NothingAppliedToHiddenArg Expr
  • | NothingAppliedToInstanceArg Expr
  • | BadArgumentsToPatternSynonym QName
  • | TooFewArgumentsToPatternSynonym QName
  • | UnusedVariableInPatternSynonym
  • | NoParseForApplication [Expr]
  • | AmbiguousParseForApplication [Expr] [Expr]
  • | NoParseForLHS LHSOrPatSyn Pattern
  • | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
  • | OperatorInformation [NotationSection] TypeError
  • | OperatorChangeMessage TypeError
  • | IFSNoCandidateInScope Type
  • | UnquoteFailed UnquoteError
  • | SafeFlagPostulate Name
  • | SafeFlagPragma [String]
  • | SafeFlagNonTerminating
  • | SafeFlagTerminating
  • | SafeFlagPrimTrustMe
  • | SafeFlagNoPositivityCheck
  • | NeedOptionCopatterns
  • | NeedOptionRewriting
• data LHSOrPatSyn
  • = IsLHS
  • | IsPatSyn
• data TCErr
  • = TypeError TCState (Closure TypeError)
  • | Exception Range Doc
  • | IOException Range IOException
  • | PatternErr
• data ReduceEnv = ReduceEnv {
  • redEnv :: TCEnv
  • redSt :: TCState
  }
• mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
• mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
• mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
• newtype ReduceM a = ReduceM {
  • unReduceM :: ReduceEnv -> a
  }
• runReduceM :: ReduceM a -> TCM a
• runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
• newtype TCMT m a = TCM {
  • unTCM :: IORef TCState -> TCEnv -> m a
  }
• type TCM = TCMT IO
• class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
• type IM = TCMT (InputT IO)
• runIM :: IM a -> TCM a
• catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
• finally_ :: TCM a -> TCM b -> TCM a
• mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
• pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
• returnTCMT :: MonadIO m => a -> TCMT m a
• bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
• thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
• fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
• apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
• patternViolation :: TCM a
• internalError :: MonadTCM tcm => String -> tcm a
• genericError :: MonadTCM tcm => String -> tcm a
• typeError :: MonadTCM tcm => TypeError -> tcm a
• typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
• runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
• runTCMTop :: TCM a -> IO (Either TCErr a)
• runTCMTop' :: MonadIO m => TCMT m a -> m a
• runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
• forkTCM :: TCM a -> TCM ()
• extendedLambdaName :: String
• absurdLambdaName :: String
• isAbsurdLambdaName :: QName -> Bool

Type checking state

st-prefixed lenses

Fresh things

Managing file names

Interface

Closure

Constraints

Open things

Judgements

Meta variables

Interaction meta variables

Signature