HORIZON HASKELLDocslts/ghc-10.0.xfc4e5982026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · fc4e598 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Monad.Base

  • 179 types
  • 14 classes
  • 459 values
  • PackageAgda-2.8.0.2
  • Exports671
  • LanguageHaskell2010
  • LicenceMIT
  • SourceBase.hs
valuefinally_ :: TCM a -> TCM b -> TCM a
#

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.

valueforkTCM :: TCM () -> TCM ()
#

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.

datadata AbstractMode
#

Constructors

Instances5Eq, Show, Generic, NFData, Rep
datadata AllowedReduction
#

Controlling reduce.

Constructors

Instances10Bounded, Enum, Eq, Ord, Show, Ix, …
datadata AxiomData
#

Constructors

Instances4Show, Generic, NFData, Rep
newtypenewtype BlockT (m :: Type -> Type) a
#

Constructors

Instances18MonadTrans, Monad, Functor, MonadFail, Applicative, MonadIO, …
datadata Builtin pf
#

Constructors

Instances10Functor, Foldable, Traversable, Show, Generic, NFData, …
datadata BuiltinSort
#
Instances7Eq, Show, Generic, NFData, KillRange, EmbPrj, …
datadata Call
#
Instances6Generic, NFData, Pretty, HasRange, PrettyTCM, Rep
datadata CallInfo
#

Information about a call.

Constructors

Instances7Show, Generic, NFData, Pretty, HasRange, PrettyTCM, …
datadata Candidate
#

A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.

Instances16Eq, Ord, Show, Generic, NFData, Subst, …
datadata CandidateKind
#
Instances6Eq, Ord, Show, Generic, NFData, Rep
datadata CannotQuote
#

Extra information for error CannotQuote.

Constructors

Instances4Show, Generic, NFData, Rep
newtypenewtype CheckpointId
#

Constructors

Instances12Enum, Eq, Integral, Num, Ord, Real, …
datadata Closure a
#
Instances18Functor, Foldable, Show, Generic, NFData, LensTCEnv, …
datadata CompKit
#
Instances9Eq, Ord, Show, Generic, NFData, KillRange, …
datadata CompareAs
#

We can either compare two terms at a given type, or compare two types without knowing (or caring about) their sorts.

Constructors

Instances19Show, Generic, NFData, Pretty, IsSizeType, Subst, …
datadata CompilerPragma
#

The backends are responsible for parsing their own pragmas.

Instances8Eq, Show, Generic, NFData, HasRange, KillRange, …
datadata Constraint
#

Constructors

Instances19Show, Generic, NFData, HasRange, Subst, PrettyTCM, …
datadata ConstructorData
#

Constructors

  • ConstructorData
    • _conPars :: Int

      Number of parameters.

    • _conArity :: Int

      Number of arguments (excluding 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
    • _conComp :: CompKit

      Cubical composition.

    • _conProj :: Maybe [QName]

      Projections. Nothing if not yet computed.

    • _conForced :: [IsForced]

      Which arguments are forced (i.e. determined by the type of the constructor)? Either this list is empty (if the forcing analysis isn't run), or its length is conArity.

    • _conErased :: Maybe [Bool]

      Which arguments are erased at runtime (computed during compilation to treeless)? True means erased, False means retained. Nothing if no erasure analysis has been performed yet. The length of the list is conArity.

    • _conErasure :: !Bool

      Was --erasure in effect when the constructor was defined? (This can affect the constructor's type.)

    • _conInline :: !Bool

      Shall we translate the constructor on the root of the rhs into copattern matching on the lhs? Activated by INLINE pragma.

Instances5Show, Generic, NFData, Pretty, Rep

Information we have constructored in the middle of disambiguating a constructor.

Constructors

Instances3Generic, NFData, Rep
datadata DataOrRecSigData
#
Instances5Show, Generic, NFData, Pretty, Rep
datadata DatatypeData
#

Constructors

Instances5Show, Generic, NFData, Pretty, Rep
datadata Definition
#

Constructors

Instances17Show, Generic, NFData, Pretty, Apply, KillRange, …
datadata Defn
#

Constructors

Instances12Show, Generic, NFData, Pretty, Apply, KillRange, …
datadata DisambiguatedName
#

Name disambiguation for the sake of highlighting.

Instances4Generic, NFData, Hilite, Rep
datadata DisplayForm
#

A DisplayForm is in essence a rewrite rule q ts --> dt for a defined symbol (could be a constructor as well) q. The right hand side is a DisplayTerm which is used to reify to a more readable Abstract.Syntax.

The patterns ts are just terms, but the first dfPatternVars variables are pattern variables that matches any term.

Constructors

  • Display
    • dfPatternVars :: Nat

      Number n of pattern variables in dfPats.

    • dfPats :: Elims

      Left hand side patterns, the n first free variables are pattern variables, any variables above n are fixed and only match that particular variable. This happens when you have display forms inside parameterised modules that match on the module parameters. The ArgInfo is ignored in these patterns.

    • dfRHS :: DisplayTerm

      Right hand side.

Instances15Show, Generic, NFData, Pretty, ChaseDisplayForms, Subst, …
datadata DisplayTerm
#

A structured presentation of a Term for reification into Abstract.Syntax.

Constructors

Instances20Show, Generic, NFData, Pretty, ChaseDisplayForms, Subst, …
datadata DoGeneralize
#

Constructors

  • YesGeneralizeVar

    Generalize because it is a generalizable variable.

  • YesGeneralizeMeta

    Generalize because it is a metavariable and we're currently checking the type of a generalizable variable (this should get the default modality).

  • NoGeneralize

    Don't generalize.

Instances8Eq, Ord, Show, Generic, NFData, KillRange, …
datadata EtaEquality
#

Should a record type admit eta-equality?

Constructors

Instances9Eq, Show, Generic, NFData, KillRange, CopatternMatchingAllowed, …
datadata ExecError
#

Error when trying to call an external executable during reflection.

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata ExpandHidden
#

Constructors

  • ExpandLast

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

  • DontExpandLast

    Do not append implicit arguments.

  • ReallyDontExpandLast

    Makes doExpandLast have no effect. Used to avoid implicit insertion of arguments to metavariables.

Instances4Eq, Generic, NFData, Rep
datadata ExtLamInfo
#

Additional information for extended lambdas.

Constructors

  • ExtLamInfo
    • extLamModule :: ModuleName

      For complicated reasons the scope checker decides the QName of a pattern lambda, and thus its module. We really need to decide the module during type checking though, since if the lambda appears in a refined context the module picked by the scope checker has very much the wrong parameters.

    • extLamAbsurd :: Bool

      Was this definition created from an absurd lambda λ ()?

    • extLamSys :: !Maybe System
Instances9Show, Generic, NFData, Apply, KillRange, NamesIn, …
datadata ForeignCode
#
Instances5Show, Generic, NFData, EmbPrj, Rep
newtypenewtype ForeignCodeStack
#

Foreign code fragments are stored in reversed order to support efficient appending: head points to the latest pragma in module.

Instances5Show, Generic, NFData, EmbPrj, Rep
datadata Frozen
#

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

Constructors

Instances5Eq, Show, Generic, NFData, Rep
datadata FunctionData
#

Constructors

Instances5Show, Generic, NFData, Pretty, Rep
datadata FunctionFlag
#

Constructors

  • FunStatic

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

  • FunInline

    Should calls to this function be inlined by the compiler?

  • FunMacro

    Is this function a macro?

  • FunFirstOrder

    Is this function INJECTIVE_FOR_INFERENCE? Indicates whether the first-order shortcut should be applied to the definition.

  • FunErasure

    Was --erasure in effect when the function was defined? (This can affect the type of a projection.)

  • FunAbstract

    Is the function abstract?

  • FunProj

    Is this function a descendant of a field (typically, a projection)?

Instances13Bounded, Enum, Eq, Ord, Show, Ix, …
datadata FunctionInverse' c
#
Instances13Functor, Apply, InstantiateFull, DropArgs, Abstract, Show, …
datadata GHCBackendError
#

Errors raised by the GHC backend.

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata GeneralizedValue
#

The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.

Instances4Show, Generic, NFData, Rep
classclass Enum i => HasFresh i where
#

Methods

Instances8HasFresh, …
newtypenewtype IPBoundary' t
#
Instances16Functor, Foldable, Traversable, Show, Generic, NFData, …
datadata IPClause
#

Which clause is an interaction point located in?

Constructors

Instances4Eq, Generic, NFData, Rep
Instances5Show, Generic, NFData, EmbPrj, Rep
Instances4Show, Generic, NFData, Rep
datadata InductionAndEta
#
Instances4Show, Generic, NFData, Rep
datadata InstanceInfo
#

Information about an instance definition.

Constructors

Instances6Show, Generic, NFData, KillRange, EmbPrj, Rep
datadata InstanceTable
#

Records information about the instances in the signature. Does not deal with local instances.

Constructors

  • InstanceTable
    • _itableTree :: DiscrimTree QName

      The actual discrimination tree for looking up instances with

    • _itableCounts :: Map QName Int

      For profiling, we store the number of instances on a per-class basis. This lets us compare the result from the discrimination tree with all the instances in scope, thus informing us how many validity checks were skipped.

Instances9Show, Generic, Semigroup, Monoid, NFData, Null, …
datadata Instantiation
#

Meta-variable instantiations.

Constructors

Instances6Show, Generic, NFData, InstantiateFull, EmbPrj, Rep
datadata InteractionError
#

Errors raised in --interaction mode.

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep

Callback fuction to call when there is a response to give to the interactive frontend.

Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.

Typical InteractionOutputCallback functions:

  • Convert the response into a String representation and print it on standard output (suitable for inter-process communication).

  • Put the response into a mutable variable stored in the closure of the InteractionOutputCallback function. (suitable for intra-process communication).

datadata InteractionPoint
#

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.

Constructors

Instances7Eq, Generic, NFData, HasTag, Rep, Tag, …
datadata Interface
#

Constructors

Instances7Show, Generic, NFData, Pretty, InstantiateFull, EmbPrj, …
Instances4Show, Generic, NFData, Rep
datadata IsAmbiguous
#

Boolean flag whether a name is ambiguous.

Instances5Show, Generic, NFData, EmbPrj, Rep
datadata IsForced
#

Information about whether an argument is forced by the type of a function.

Instances9Eq, Show, Generic, NFData, PrettyTCM, KillRange, …
datadata JSBackendError
#

Errors raised by the JS backend.

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata Judgement a
#

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

Constructors

Instances8Show, Generic, NFData, Pretty, PrettyTCM, InstantiateFull, …
datadata LHSOrPatSyn
#

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

Instances8Bounded, Enum, Eq, Show, Generic, NFData, …
datadata LetBinding
#
Instances7Show, Generic, NFData, Subst, InstantiateFull, Rep, …
datadata Listener
#
Instances5Eq, Ord, Generic, NFData, Rep
datadata LoadedFileCache
#
Instances3Generic, NFData, Rep
datadata MetaInfo
#

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

Constructors

Instances11Generic, NFData, HasRange, SetRange, LensIsAbstract, LensModalPolarity, …
datadata MetaInstantiation
#

Solution status of meta.

Constructors

Instances4Generic, NFData, Pretty, Rep
newtypenewtype MetaPriority
#

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

Higher value means higher priority to be instantiated.

Constructors

Instances4Eq, Ord, Show, NFData
datadata MetaVariable
#

Information about local meta-variables.

Constructors

Instances9Generic, NFData, HasRange, SetRange, LensModality, LensQuantity, …

Extra information for MissingTypeSignature error.

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata ModuleCheckMode
#

Distinguishes between type-checked and scope-checked interfaces when stored in the map of VisitedModules.

Instances8Bounded, Enum, Eq, Ord, Show, Generic, …
datadata ModuleInfo
#

Constructors

Instances3Generic, NFData, Rep
classclass Monad m => MonadBlock (m :: Type -> Type) where
#

Methods

  • patternViolation :: Blocker -> m a

    `patternViolation b` aborts the current computation

  • catchPatternErr :: (Blocker -> m a) -> m a -> m a

    `catchPatternErr handle m` runs m, handling pattern violations with handle (doesn't roll back the state)

Instances7MonadBlock, …
classclass Monad m => MonadFresh i (m :: Type -> Type) where
#

Methods

Instances12MonadFresh, …
classclass (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce (m :: Type -> Type) where
#

Methods

Instances17MonadReduce, …
classclass Monad m => MonadStConcreteNames (m :: Type -> Type) where
#

A monad that has read and write access to the stConcreteNames part of the TCState. Basically, this is a synonym for `MonadState ConcreteNames m` (which cannot be used directly because of the limitations of Haskell's typeclass system).

Instances9MonadStConcreteNames, …
classclass Monad m => MonadTCEnv (m :: Type -> Type) where
#

MonadTCEnv made into its own dedicated service class. This allows us to use MonadReader for ReaderT extensions of TCM.

Methods

Instances19MonadTCEnv, …
classclass (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM (tcm :: Type -> Type) where
#

Embedding a TCM computation.

Methods

Instances14MonadTCM, …
classclass Monad m => MonadTCState (m :: Type -> Type) where
#

MonadTCState made into its own dedicated service class. This allows us to use MonadState for StateT extensions of TCM.

Methods

Instances14MonadTCState, …
datadata MutualBlock
#

A mutual block of names in the signature.

Constructors

Instances6Eq, Show, Generic, NFData, Null, Rep
newtypenewtype MutualId
#

Constructors

Instances10Enum, Eq, Num, Ord, Show, NFData, …
  • Enum MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Eq MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Num MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Ord MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Show MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • NFData MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Pretty MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • HasFresh MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • KillRange MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • EmbPrj MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
datadata NLPSort
#
Instances19Show, Generic, NFData, Subst, PrettyTCM, Free, …
datadata NLPType
#
Instances19Show, Generic, NFData, Subst, PrettyTCM, Free, …
datadata NLPat
#

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

Constructors

Instances31Show, Generic, NFData, DeBruijn, Subst, Free, …
datadata NegativeUnification
#
Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata NumGeneralizableArgs
#

Constructors

Instances6Show, NFData, Apply, KillRange, Abstract, EmbPrj
datadata OpaqueBlock
#

A block of opaque definitions.

Constructors

Instances8Eq, Show, Generic, NFData, Hashable, Pretty, …
datadata Open a
#

A thing tagged with the context it came from. Also keeps the substitution from previous checkpoints. This lets us handle the case when an open thing was created in a context that we have since exited. Remember which module it's from to make sure we don't get confused by checkpoints from other files.

Instances14Functor, Foldable, Traversable, Decoration, Show, Generic, …
datadata Overapplied
#

Flag to indicate whether the meta is overapplied in the constraint. A meta is overapplied if it has more arguments than the size of the telescope in its creation environment (as stored in MetaInfo).

Instances5Eq, Show, Generic, NFData, Rep
datadata PersistentTCState
#

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

Constructors

Instances7Generic, NFData, LensCommandLineOptions, LensIncludePaths, LensPersistentVerbosity, LensSafeMode, …
datadata PostScopeState
#

Constructors

Instances3Generic, NFData, Rep
datadata PreScopeState
#

Constructors

Instances4Generic, NFData, LensPragmaOptions, Rep
datadata PrimFun
#
Instances6Generic, NFData, Apply, NamesIn, Abstract, Rep
datadata PrimitiveData
#

Constructors

Instances5Show, Generic, NFData, Pretty, Rep
datadata PrimitiveSortData
#
Instances5Show, Generic, NFData, Pretty, Rep

Constructors

Instances3Generic, NFData, Rep
datadata ProblemConstraint
#
Instances12Show, Generic, NFData, HasRange, PrettyTCM, Reify, …
newtypenewtype ProjLams
#

Abstractions to build projection function (dropping parameters).

Instances10Show, Generic, NFData, Pretty, Null, Apply, …
datadata Projection
#

Additional information for projection Functions.

Constructors

  • Projection
    • projProper :: Maybe QName

      Nothing if only projection-like, Just r if record projection. The r is the name of the record type projected from. This field is updated by module application.

    • projOrig :: QName

      The original projection name (current name could be from module application).

    • projFromType :: Arg QName

      Type projected from. Original record type if projProper = Just{}. Also stores ArgInfo of the principal argument. This field is unchanged by module application.

    • 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 == Left _.

    • projLams :: ProjLams

      Term t to be be applied to record parameters and record value. The parameters will be dropped. In case of a proper projection, a postfix projection application will be created: t = pars r -> r .p (Invariant: the number of abstractions equals projIndex.) In case of a projection-like function, just the function symbol is returned as Def: t = pars -> f.

Instances9Show, Generic, NFData, Pretty, Apply, KillRange, …

Indicates the reason behind a function having not been marked projection-like.

Constructors

  • MaybeProjection

    Projection-likeness analysis has not run on this function yet. It may do so in the future.

  • NeverProjection

    The user has requested that this function be not be marked projection-like. The analysis may already have run on this function, but the results have been discarded, and it will not be run again.

Instances9Bounded, Enum, Show, Generic, NFData, Pretty, …
classclass Monad m => ReadTCState (m :: Type -> Type) where
#

Methods

Instances19ReadTCState, …
datadata RecordData
#

Constructors

Instances5Show, Generic, NFData, Pretty, Rep
datadata ReduceDefs
#
Instances3Generic, NFData, Rep
datadata ReduceEnv
#

Environment of the reduce monad.

Constructors

newtypenewtype ReduceM a
#

Constructors

Instances14Monad, Functor, MonadFail, Applicative, HasOptions, MonadReduce, …
datadata RemoteMetaVariable
#

Information about remote meta-variables.

Remote meta-variables are meta-variables originating in other modules. These meta-variables are always instantiated. We do not retain all the information about a local meta-variable when creating an interface:

  • The mvPriority field is not needed, because the meta-variable cannot be instantiated.

  • The mvFrozen field is not needed, because there is no point in freezing instantiated meta-variables.

  • The mvListeners field is not needed, because no meta-variable should be listening to this one.

  • The mvTwin field is not needed, because the meta-variable has already been instantiated.

  • The mvPermutation is currently removed, but could be retained if it turns out to be useful for something.

  • The only part of the mvInfo field that is kept is the miModality field. The miMetaOccursCheck and miGeneralizable fields are omitted, because the meta-variable has already been instantiated. The Range that is part of the miClosRange field and the miNameSuggestion field are omitted because instantiated meta-variables are typically not presented to users. Finally the Closure part of the miClosRange field is omitted because it can be large (at least if we ignore potential sharing).

Instances10Show, Generic, NFData, LensModalPolarity, LensModality, LensQuantity, …
datadata RewriteRule
#

Rewrite rules can be added independently from function clauses.

Constructors

Instances15Show, Generic, NFData, Subst, PrettyTCM, Apply, …
datadata RunMetaOccursCheck
#
Instances6Eq, Ord, Show, Generic, NFData, Rep
newtypenewtype Section
#
Instances9Eq, Show, NFData, Pretty, KillRange, NamesIn, …
  • Eq SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
  • Show SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • NFData SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Pretty SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • KillRange SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • KillRange SectionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • NamesIn SectionDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
  • InstantiateFull SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
  • EmbPrj SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
datadata SessionTCState
#

A part of the state that grows monotonically over the whole Agda session. Never reset.

Constructors

Instances3Generic, NFData, Rep
datadata Signature
#
Instances8Show, Generic, NFData, Null, KillRange, InstantiateFull, …
datadata Simplification
#

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?

Instances8Eq, Show, Generic, Semigroup, Monoid, NFData, …
datadata SplitError
#

Error when splitting a pattern variable into possible constructor patterns.

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata System
#

An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).

Constructors

Instances12Show, Generic, NFData, Apply, KillRange, NamesIn, …
datadata TCEnv
#

Constructors

Instances6Generic, NFData, LensTCEnv, LensIsAbstract, LensIsOpaque, Rep
datadata TCErr
#

Type-checking errors.

Constructors

Instances23Show, Exception, NFData, HasRange, MonadError, Pretty, …
newtypenewtype TCMT (m :: Type -> Type) a
#

The type checking monad transformer. Adds readonly TCEnv and mutable TCState.

Constructors

Instances42MonadTrans, MonadBench, MonadBlock, MonadStConcreteNames, MonadConstraint, MonadAddContext, …
datadata TCState
#

Constructors

Instances10Show, Generic, NFData, LensPragmaOptions, LensCommandLineOptions, LensIncludePaths, …
datadata TCWarning
#

Constructors

Instances13Eq, Ord, Show, Generic, NFData, HasRange, …

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.

datadata TermHead
#
Instances9Eq, Ord, Show, Generic, NFData, Pretty, …
datadata TerminationError
#

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

Constructors

Instances4Show, Generic, NFData, Rep
datadata TypeCheckAction
#

A complete log for a module will look like this:

Instances3Generic, NFData, Rep
datadata TypeCheckingProblem
#

Constructors

Instances4Generic, NFData, PrettyTCM, Rep
datadata TypeError
#

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata UnificationFailure
#

Constructors

Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata UnquoteError
#
Instances5Show, Generic, NFData, PrettyTCM, Rep
datadata UnquoteFlags
#
Instances3Generic, NFData, Rep
datadata Warning
#

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

Constructors

Instances6Show, Generic, NFData, PrettyTCM, EmbPrj, Rep
datadata WhyCheckModality
#

Why are we performing a modality check?

Constructors

  • ConstructorType

    Because --without-K is enabled, so the types of data constructors must be usable at the context's modality.

  • IndexedClause

    Because --without-K is enabled, so the result type of clauses must be usable at the context's modality.

  • IndexedClauseArg Name Name

    Because --without-K is enabled, so any argument (second name) which mentions a dotted argument (first name) must have a type which is usable at the context's modality.

  • GeneratedClause

    Because we double-check the --cubical-compatible clauses. This is an internal error!

Instances4Show, Generic, NFData, Rep

Reason for why the instance type is invalid.

Constructors

  • ImproperInstHead

    The type isn't headed by a local, a definition, or a postulate (e.g. it's a universe)

  • ImproperInstTele

    The type we're looking for has a visible argument

Instances4Show, Generic, NFData, Rep
datadata WhyNotAHaskellType
#
Instances4Show, Generic, NFData, Rep
datadata CannotQuoteTerm
#
Instances6Bounded, Enum, Show, Generic, NFData, Rep
datadata ErasedDatatypeReason
#

The reason for an ErasedDatatype error.

Constructors

Instances6Bounded, Enum, Show, Generic, NFData, Rep
datadata NotAValidLetBinding
#
Instances6Bounded, Enum, Show, Generic, NFData, Rep
Instances6Bounded, Enum, Show, Generic, NFData, Rep

Things not allowed in dot patterns.

Instances6Bounded, Enum, Show, Generic, NFData, Rep
newtypenewtype FileId
#

Unique identifier of a file.

Instances10Enum, Eq, Num, Ord, Show, Generic, …
classclass Monad m => MonadFileId (m :: Type -> Type) where
#

Methods

Instances6MonadFileId
classclass (Functor m, Applicative m, Monad m) => HasOptions (m :: Type -> Type) where
#

Methods

Instances19HasOptions, …
datadata RecordFieldWarning
#
Instances5Show, Generic, NFData, EmbPrj, Rep
datadata UselessPublicReason
#
Instances7Bounded, Enum, Show, Generic, NFData, EmbPrj, …

Orphan instances

13 instances