Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Monad.Base

Contents

Orphan instances

Synopsis

data Constraint
- = ValueCmp Comparison CompareAs Term Term
- | ValueCmpOnFace Comparison Term Type Term Term
- | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
- | SortCmp Comparison Sort Sort
- | LevelCmp Comparison Level Level
- | HasBiggerSort Sort
- | HasPTSRule (Dom Type) (Abs Sort)
- | CheckDataSort QName Sort
- | CheckMetaInst MetaId
- | CheckType Type
- | UnBlock MetaId
- | IsEmpty Range Type
- | CheckSizeLtSat Term
- | FindInstance MetaId (Maybe [Candidate])
- | ResolveInstanceHead QName
- | CheckFunDef DefInfo QName [Clause] TCErr
- | UnquoteTactic Term Term Type
- | CheckLockedVars Term Type (Arg Term) Type
- | UsableAtModality WhyCheckModality (Maybe Sort) Modality Term
data TypeError
- = InternalError String
- | NotImplemented String
- | NotSupported String
- | CompilationError String
- | PropMustBeSingleton
- | DataMustEndInSort Term
- | ShouldEndInApplicationOfTheDatatype Type
- | ShouldBeAppliedToTheDatatypeParameters Term Term
- | ShouldBeApplicationOf Type QName
- | ConstructorPatternInWrongDatatype QName QName
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName (List1 QName)
- | DoesNotConstructAnElementOf QName Type
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongHidingInProjection QName
- | IllegalHidingInPostfixProjection (NamedArg Expr)
- | WrongNamedArgument (NamedArg Expr) [NamedName]
- | WrongIrrelevanceInLambda
- | WrongQuantityInLambda
- | WrongCohesionInLambda
- | QuantityMismatch Quantity Quantity
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | UninstantiatedDotPattern Expr
- | ForcedConstructorNotInstantiated Pattern
- | IllformedProjectionPatternAbstract Pattern
- | IllformedProjectionPatternConcrete Pattern
- | CannotEliminateWithPattern (Maybe Blocker) (NamedArg Pattern) Type
- | CannotEliminateWithProjection (Arg Type) Bool QName
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [DeBruijnPattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBePath Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern DeBruijnPattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | InvalidTypeSort Sort
- | InvalidType Term
- | SplitOnCoinductive
- | SplitOnIrrelevant (Dom Type)
- | SplitOnUnusableCohesion (Dom Type)
- | SplitOnNonVariable Term Type
- | SplitOnNonEtaRecord QName
- | SplitOnAbstract QName
- | SplitOnUnchecked QName
- | SplitOnPartial (Dom Type)
- | SplitInProp DataOrRecordE
- | DefinitionIsIrrelevant QName
- | DefinitionIsErased QName
- | ProjectionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | VariableIsErased Name
- | VariableIsOfUnusableCohesion Name Cohesion
- | UnequalLevel Comparison Level Level
- | UnequalTerms Comparison Term Term CompareAs
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalQuantity Comparison Term Term
- | UnequalCohesion Comparison Term Term
- | UnequalFiniteness Comparison Term Term
- | UnequalHiding Term Term
- | UnequalSorts Sort Sort
- | UnequalBecauseOfUniverseConflict Comparison Term Term
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId Nat
- | MetaOccursInItself MetaId
- | MetaIrrelevantSolution MetaId Term
- | MetaErasedSolution MetaId Term
- | GenericError String
- | GenericDocError Doc
- | SortOfSplitVarError (Maybe Blocker) Doc
- | BuiltinMustBeConstructor BuiltinId Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding BuiltinId Term Term
- | NoBindingForBuiltin BuiltinId
- | NoBindingForPrimitive PrimitiveId
- | NoSuchPrimitiveFunction String
- | DuplicatePrimitiveBinding PrimitiveId QName QName
- | WrongArgInfoForPrimitive PrimitiveId ArgInfo ArgInfo
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule BuiltinId
- | IllegalDeclarationInDataDefinition [Declaration]
- | IllegalLetInTelescope TypedBinding
- | IllegalPatternInTelescope Binder
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | TooManyFields QName [Name] [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | DuplicateOverlapPragma QName OverlapMode OverlapMode
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
- | IllTypedPatternAfterWithAbstraction Pattern
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | GeneralizeCyclicDependency
- | GeneralizeUnsolvedMeta
- | ReferencesFutureVariables Term (NonEmpty Int) (Arg Term) Int
- | DoesNotMentionTicks Term Type (Arg Term)
- | MismatchedProjectionsError QName QName
- | AttributeKindNotEnabled String String String
- | InvalidProjectionParameter (NamedArg Expr)
- | TacticAttributeNotAllowed
- | CannotRewriteByNonEquation Type
- | MacroResultTypeMismatch Type
- | NamedWhereModuleInRefinedContext [Term] [String]
- | CubicalPrimitiveNotFullyApplied QName
- | TooManyArgumentsToLeveledSort QName
- | TooManyArgumentsToUnivOmega QName
- | ComatchingDisabledForRecord QName
- | BuiltinMustBeIsOne Term
- | IncorrectTypeForRewriteRelation Term IncorrectTypeForRewriteRelationReason
- | UnexpectedParameter LamBinding
- | NoParameterOfName ArgName
- | UnexpectedModalityAnnotationInParameter LamBinding
- | ExpectedBindingForParameter (Dom Type) (Abs Type)
- | UnexpectedTypeSignatureForParameter (List1 (NamedArg Binder))
- | SortDoesNotAdmitDataDefinitions QName Sort
- | SortCannotDependOnItsIndex QName Type
- | UnusableAtModality WhyCheckModality Modality Term
- | SplitError SplitError
- | ImpossibleConstructor QName NegativeUnification
- | TooManyPolarities QName Int
- | RecursiveRecordNeedsInductivity QName
- | CannotSolveSizeConstraints (List1 (ProblemConstraint, HypSizeConstraint)) Doc
- | ContradictorySizeConstraint (ProblemConstraint, HypSizeConstraint)
- | EmptyTypeOfSizes Term
- | FunctionTypeInSizeUniv Term
- | LibraryError LibErrors
- | LocalVsImportedModuleClash ModuleName
- | SolvedButOpenHoles
- | CyclicModuleDependency [TopLevelModuleName]
- | FileNotFound TopLevelModuleName [AbsolutePath]
- | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
- | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
- | ModuleNameUnexpected TopLevelModuleName TopLevelModuleName
- | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
- | ClashingFileNamesFor ModuleName [AbsolutePath]
- | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
- | InvalidFileName AbsolutePath InvalidFileNameReason
- | BothWithAndRHS
- | AbstractConstructorNotInScope QName
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName AmbiguousNameReason
- | AmbiguousModule QName (List1 ModuleName)
- | AmbiguousField Name [ModuleName]
- | AmbiguousConstructor QName [QName]
- | ClashingDefinition QName QName (Maybe NiceDeclaration)
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | DefinitionInDifferentModule QName
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | GeneralizeNotSupportedHere QName
- | GeneralizedVarInLetOpenedModule QName
- | MultipleFixityDecls [(Name, [Fixity'])]
- | MultiplePolarityPragmas [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | AsPatternInPatternSynonym
- | DotPatternInPatternSynonym
- | BadArgumentsToPatternSynonym AmbiguousQName
- | TooFewArgumentsToPatternSynonym AmbiguousQName
- | CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn))
- | IllegalInstanceVariableInPatternSynonym Name
- | PatternSynonymArgumentShadowsConstructorOrPatternSynonym LHSOrPatSyn Name (List1 AbstractName)
- | UnusedVariableInPatternSynonym Name
- | UnboundVariablesInPatternSynonym [Name]
- | NoParseForApplication (List2 Expr)
- | AmbiguousParseForApplication (List2 Expr) (List1 Expr)
- | NoParseForLHS LHSOrPatSyn [Pattern] Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | AmbiguousProjection QName [QName]
- | AmbiguousOverloadedProjection (List1 QName) Doc
- | OperatorInformation [NotationSection] TypeError
- | InstanceNoCandidate Type [(Term, TCErr)]
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NeedOptionProp
- | NeedOptionTwoLevel
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
- | TriedToCopyConstrainedPrim QName
- | CustomBackendError String Doc
data Comparison
- = CmpEq
- | CmpLeq
data ModuleInfo = ModuleInfo {
- miInterface :: Interface
- miWarnings :: [TCWarning]
- miPrimitive :: Bool
- miMode :: ModuleCheckMode
}
data Definition = Defn {
- defArgInfo :: ArgInfo
- defName :: QName
- defType :: Type
- defPolarity :: [Polarity]
- defArgOccurrences :: [Occurrence]
- defArgGeneralizable :: NumGeneralizableArgs
- defGeneralizedParams :: [Maybe Name]
- defDisplay :: [LocalDisplayForm]
- defMutual :: MutualId
- defCompiledRep :: CompiledRepresentation
- defInstance :: Maybe InstanceInfo
- defCopy :: Bool
- defMatchable :: Set QName
- defNoCompilation :: Bool
- defInjective :: Bool
- defCopatternLHS :: Bool
- defBlocked :: Blocked_
- defLanguage :: !Language
- theDef :: Defn
}
data Builtin pf
- = Builtin Term
- | Prim pf
- | BuiltinRewriteRelations (Set QName)
data System = System {
- systemTel :: Telescope
- systemClauses :: [(Face, Term)]
}
type TCM = TCMT IO
newtype ReduceM a = ReduceM {
- unReduceM :: ReduceEnv -> a
}
data HighlightingLevel
- = None
- | NonInteractive
- | Interactive
data HighlightingMethod
- = Direct
- | Indirect
data Polarity
- = Covariant
- | Contravariant
- | Invariant
- | Nonvariant
data Open a = OpenThing {
- openThingCheckpoint :: CheckpointId
- openThingCheckpointMap :: Map CheckpointId Substitution
- openThingModule :: ModuleNameHash
- openThing :: a
}
data MetaInfo = MetaInfo {
- miClosRange :: Closure Range
- miModality :: Modality
- miMetaOccursCheck :: RunMetaOccursCheck
- miNameSuggestion :: MetaNameSuggestion
- miGeneralizable :: Arg DoGeneralize
}
type Constraints = [ProblemConstraint]
data WarningsAndNonFatalErrors = WarningsAndNonFatalErrors {
- tcWarnings :: [TCWarning]
- nonFatalErrors :: [TCWarning]
}
data Signature = Sig {
- _sigSections :: Sections
- _sigDefinitions :: Definitions
- _sigRewriteRules :: RewriteRuleMap
- _sigInstances :: InstanceTable
}
data Warning
- = NicifierIssue DeclarationWarning
- | TerminationIssue [TerminationError]
- | UnreachableClauses QName [Range]
- | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
- | CoverageNoExactSplit QName [Clause]
- | InlineNoExactSplit QName Clause
- | NotStrictlyPositive QName (Seq OccursWhere)
- | ConstructorDoesNotFitInData QName Sort Sort TCErr
- | CoinductiveEtaRecord QName
- | UnsolvedMetaVariables [Range]
- | UnsolvedInteractionMetas [Range]
- | UnsolvedConstraints Constraints
- | InteractionMetaBoundaries [Range]
- | CantGeneralizeOverSorts [MetaId]
- | AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
- | OldBuiltin BuiltinId BuiltinId
- | BuiltinDeclaresIdentifier BuiltinId
- | DuplicateRecordDirective RecordDirective
- | EmptyRewritePragma
- | EmptyWhere
- | IllformedAsClause String
- | InvalidCharacterLiteral Char
- | ClashesViaRenaming NameOrModule [Name]
- | UselessPatternDeclarationForRecord String
- | UselessPragma Range Doc
- | UselessPublic
- | UselessHiding [ImportedName]
- | UselessInline QName
- | WrongInstanceDeclaration
- | InstanceWithExplicitArg QName
- | InstanceNoOutputTypeName Doc
- | InstanceArgWithExplicitArg Doc
- | InversionDepthReached QName
- | NoGuardednessFlag QName
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagWithoutKFlagPrimEraseEquality
- | WithoutKFlagPrimEraseEquality
- | ConflictingPragmaOptions String String
- | OptionWarning OptionWarning
- | ParseWarning ParseWarning
- | LibraryWarning LibWarning
- | DeprecationWarning String String String
- | UserWarning Text
- | DuplicateUsing (List1 ImportedName)
- | FixityInRenamingModule (List1 Range)
- | ModuleDoesntExport QName [Name] [Name] [ImportedName]
- | InfectiveImport Doc
- | CoInfectiveImport Doc
- | ConfluenceCheckingIncompleteBecauseOfMeta QName
- | ConfluenceForCubicalNotSupported
- | IllegalRewriteRule QName IllegalRewriteRuleReason
- | RewriteNonConfluent Term Term Term Doc
- | RewriteMaybeNonConfluent Term Term [Doc]
- | RewriteAmbiguousRules Term Term Term
- | RewriteMissingRule Term Term Term
- | PragmaCompileErased BackendName QName
- | PragmaCompileList
- | PragmaCompileMaybe
- | NoMain TopLevelModuleName
- | NotInScopeW [QName]
- | UnsupportedIndexedMatch Doc
- | AsPatternShadowsConstructorOrPatternSynonym LHSOrPatSyn
- | PatternShadowsConstructor Name QName
- | PlentyInHardCompileTimeMode QωOrigin
- | RecordFieldWarning RecordFieldWarning
- | MissingTypeSignatureForOpaque QName IsOpaque
- | NotAffectedByOpaque
- | UnfoldTransparentName QName
- | UselessOpaque
- | FaceConstraintCannotBeHidden ArgInfo
- | FaceConstraintCannotBeNamed NamedName
- | DuplicateInterfaceFiles AbsolutePath AbsolutePath
- | CustomBackendWarning String Doc
data TCErr
- = TypeError {
  - tcErrLocation :: CallStack
  - tcErrState :: TCState
  - tcErrClosErr :: Closure TypeError
  }
- | Exception Range Doc
- | IOException TCState Range IOException
- | PatternErr Blocker
data TCWarning = TCWarning {
- tcWarningLocation :: CallStack
- tcWarningRange :: Range
- tcWarning :: Warning
- tcWarningPrintedWarning :: Doc
- tcWarningCached :: Bool
}
data NamedMeta = NamedMeta {
- nmSuggestion :: MetaNameSuggestion
- nmid :: MetaId
}
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type Definitions = HashMap QName Definition
type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()
data IPFace' t = IPFace' {
- faceEqns :: [(t, t)]
- faceRHS :: t
}
class Monad m => MonadTCEnv m where
- askTC :: m TCEnv
- localTC :: (TCEnv -> TCEnv) -> m a -> m a
class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where
- liftTCM :: TCM a -> tcm a
class Monad m => MonadTCState m where
- getTC :: m TCState
- putTC :: TCState -> m ()
- modifyTC :: (TCState -> TCState) -> m ()
class Monad m => ReadTCState m where
- getTCState :: m TCState
- locallyTCState :: Lens' TCState a -> (a -> a) -> m b -> m b
- withTCState :: (TCState -> TCState) -> m a -> m a
newtype TCMT m a = TCM {
- unTCM :: IORef TCState -> TCEnv -> m a
}
data LHSOrPatSyn
- = IsLHS
- | IsPatSyn
data DisplayForm = Display {
- dfPatternVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
}
data Call
- = CheckClause Type SpineClause
- | CheckLHS SpineLHS
- | CheckPattern Pattern Telescope Type
- | CheckPatternLinearityType Name
- | CheckPatternLinearityValue Name
- | CheckLetBinding LetBinding
- | InferExpr Expr
- | CheckExprCall Comparison Expr Type
- | CheckDotPattern Expr Term
- | CheckProjection Range QName Type
- | IsTypeCall Comparison Expr Sort
- | IsType_ Expr
- | InferVar Name
- | InferDef QName
- | CheckArguments Range [NamedArg Expr] Type (Maybe Type)
- | CheckMetaSolution Range MetaId Type Term
- | CheckTargetType Range Type Type
- | CheckDataDef Range QName [LamBinding] [Constructor]
- | CheckRecDef Range QName [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckConArgFitsIn QName Bool Type Sort
- | CheckFunDefCall Range QName [Clause] Bool
- | CheckPragma Range Pragma
- | CheckPrimitive Range QName Expr
- | CheckIsEmpty Range Type
- | CheckConfluence QName QName
- | CheckModuleParameters ModuleName Telescope
- | CheckWithFunctionType Type
- | CheckSectionApplication Range Erased ModuleName ModuleApplication
- | CheckNamedWhere ModuleName
- | CheckIApplyConfluence Range QName Term Term Term Type
- | ScopeCheckExpr Expr
- | ScopeCheckDeclaration NiceDeclaration
- | ScopeCheckLHS QName Pattern
- | NoHighlighting
- | ModuleContents
- | SetRange Range
data Closure a = Closure {
- clSignature :: Signature
- clEnv :: TCEnv
- clScope :: ScopeInfo
- clModuleCheckpoints :: Map ModuleName CheckpointId
- clValue :: a
}
class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where
- liftReduce :: ReduceM a -> m a
type Statistics = Map String Integer
data CompilerPragma = CompilerPragma Range String
data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envCoverageCheck :: CoverageCheck
- envMakeCase :: Bool
- envSolvingConstraints :: Bool
- envCheckingWhere :: Bool
- envWorkingOnTypes :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: Set ProblemId
- envUnquoteProblem :: Maybe ProblemId
- envAbstractMode :: AbstractMode
- envRelevance :: Relevance
- envQuantity :: Quantity
- envHardCompileTimeMode :: Bool
- envSplitOnStrict :: Bool
- envDisplayFormsEnabled :: Bool
- envFoldLetBindings :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envReduceDefs :: ReduceDefs
- envReconstructed :: Bool
- envInjectivityDepth :: Int
- envCompareBlocked :: Bool
- envPrintDomainFreePi :: Bool
- envPrintMetasBare :: Bool
- envInsideDotPattern :: Bool
- envUnquoteFlags :: UnquoteFlags
- envInstanceDepth :: !Int
- envIsDebugPrinting :: Bool
- envPrintingPatternLambdas :: [QName]
- envCallByNeed :: Bool
- envCurrentCheckpoint :: CheckpointId
- envCheckpoints :: Map CheckpointId Substitution
- envGeneralizeMetas :: DoGeneralize
- envGeneralizedVars :: Map QName GeneralizedValue
- envActiveBackendName :: Maybe BackendName
- envConflComputingOverlap :: Bool
- envCurrentlyElaborating :: Bool
- envSyntacticEqualityFuel :: !(Maybe Int)
- envCurrentOpaqueId :: !(Maybe OpaqueId)
}
data Interface = Interface {
- iSourceHash :: !Hash
- iSource :: Text
- iFileType :: FileType
- iImportedModules :: [(TopLevelModuleName, Hash)]
- iModuleName :: ModuleName
- iTopLevelModuleName :: TopLevelModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iMetaBindings :: RemoteMetaStore
- iDisplayForms :: DisplayForms
- iUserWarnings :: Map QName Text
- iImportWarning :: Maybe Text
- iBuiltin :: BuiltinThings (PrimitiveId, QName)
- iForeignCode :: Map BackendName ForeignCodeStack
- iHighlighting :: HighlightingInfo
- iDefaultPragmaOptions :: [OptionsPragma]
- iFilePragmaOptions :: [OptionsPragma]
- iOptionsUsed :: PragmaOptions
- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]
- iPartialDefs :: Set QName
- iOpaqueBlocks :: Map OpaqueId OpaqueBlock
- iOpaqueNames :: Map QName OpaqueId
}
type MonadTCError m = (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
type BackendName = String
data TCState = TCSt {
- stPreScopeState :: !PreScopeState
- stPostScopeState :: !PostScopeState
- stPersistentState :: !PersistentTCState
}
type RewriteRules = [RewriteRule]
data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunArgOccurrences :: [Occurrence]
- primFunImplementation :: [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
}
data RunMetaOccursCheck
- = RunMetaOccursCheck
- | DontRunMetaOccursCheck
data CompareAs
- = AsTermsOf Type
- | AsSizes
- | AsTypes
data CompareDirection
- = DirEq
- | DirLeq
- | DirGeq
data MetaVariable = MetaVar {
- mvInfo :: MetaInfo
- mvPriority :: MetaPriority
- mvPermutation :: Permutation
- mvJudgement :: Judgement MetaId
- mvInstantiation :: MetaInstantiation
- mvListeners :: Set Listener
- mvFrozen :: Frozen
- mvTwin :: Maybe MetaId
}
data InstanceInfo = InstanceInfo {
- instanceClass :: QName
- instanceOverlap :: OverlapMode
}
class Monad m => MonadBlock m where
- patternViolation :: Blocker -> m a
- catchPatternErr :: (Blocker -> m a) -> m a -> m a
data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
data ProblemConstraint = PConstr {
- constraintProblems :: Set ProblemId
- constraintUnblocker :: Blocker
- theConstraint :: Closure Constraint
}
newtype Fields = Fields [(Name, Type)]
data ForeignCode = ForeignCode Range String
data LetBinding = LetBinding {
- letOrigin :: Origin
- letTerm :: Term
- letType :: Dom Type
}
newtype Section = Section {
- _secTelescope :: Telescope
}
data PreScopeState = PreScopeState {
- stPreTokens :: !HighlightingInfo
- stPreImports :: !Signature
- stPreImportedModules :: !(Set TopLevelModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPreGeneralizedVars :: !(Maybe (Set QName))
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreFreshInteractionId :: !InteractionId
- stPreImportedUserWarnings :: !(Map QName Text)
- stPreLocalUserWarnings :: !(Map QName Text)
- stPreWarningOnImport :: !(Maybe Text)
- stPreImportedPartialDefs :: !(Set QName)
- stPreProjectConfigs :: !(Map FilePath ProjectConfig)
- stPreAgdaLibFiles :: !(Map FilePath AgdaLibFile)
- stPreImportedMetaStore :: !RemoteMetaStore
- stPreCopiedNames :: !(HashMap QName QName)
- stPreNameCopies :: !(HashMap QName (HashSet QName))
}
data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !HighlightingInfo
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostOpenMetaStore :: !LocalMetaStore
- stPostSolvedMetaStore :: !LocalMetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
- stPostImportsDisplayForms :: !DisplayForms
- stPostForeignCode :: !(Map BackendName ForeignCodeStack)
- stPostCurrentModule :: !(Maybe (ModuleName, TopLevelModuleName))
- stPostPendingInstances :: !(Set QName)
- stPostTemporaryInstances :: !(Set QName)
- stPostConcreteNames :: !ConcreteNames
- stPostUsedNames :: !(Map RawName (DList RawName))
- stPostShadowingNames :: !(Map Name (DList RawName))
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostFreshOpaqueId :: !OpaqueId
- stPostAreWeCaching :: !Bool
- stPostPostponeInstanceSearch :: !Bool
- stPostConsideringInstance :: !Bool
- stPostInstantiateBlocking :: !Bool
- stPostLocalPartialDefs :: !(Set QName)
- stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
- stPostOpaqueIds :: Map QName OpaqueId
}
data PersistentTCState = PersistentTCSt {
- stDecodedModules :: !DecodedModules
- stPersistentTopLevelModuleNames :: !(BiMap RawTopLevelModuleName ModuleNameHash)
- stPersistentOptions :: CommandLineOptions
- stInteractionOutputCallback :: InteractionOutputCallback
- stBenchmark :: !Benchmark
- stAccumStatistics :: !Statistics
- stPersistLoadedFileCache :: !(Maybe LoadedFileCache)
- stPersistBackends :: [Backend_boot TCM]
}
type VisitedModules = Map TopLevelModuleName ModuleInfo
type BuiltinThings pf = Map SomeBuiltin (Builtin pf)
type DisplayForms = HashMap QName [LocalDisplayForm]
type RemoteMetaStore = HashMap MetaId RemoteMetaVariable
data DisambiguatedName = DisambiguatedName NameKind QName
type DisambiguatedNames = IntMap DisambiguatedName
type ConcreteNames = Map Name [Name]
type LocalMetaStore = Map MetaId MetaVariable
type InteractionPoints = BiMap InteractionId InteractionPoint
newtype CheckpointId = CheckpointId Int
newtype ForeignCodeStack = ForeignCodeStack {
- getForeignCodeStack :: [ForeignCode]
}
newtype MutualId = MutId Int32
data MutualBlock = MutualBlock {
- mutualInfo :: MutualInfo
- mutualNames :: Set QName
}
data OpaqueBlock = OpaqueBlock {
- opaqueId :: !OpaqueId
- opaqueUnfolding :: HashSet QName
- opaqueDecls :: HashSet QName
- opaqueParent :: Maybe OpaqueId
- opaqueRange :: Range
}
type DecodedModules = Map TopLevelModuleName ModuleInfo
data LoadedFileCache = LoadedFileCache {
- lfcCached :: !CachedTypeCheckLog
- lfcCurrent :: !CurrentTypeCheckLog
}
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data TypeCheckAction
- = EnterSection !Erased !ModuleName !Telescope
- | LeaveSection !ModuleName
- | Decl !Declaration
- | Pragmas !PragmaOptions
type TempInstanceTable = (InstanceTable, Set QName)
class Enum i => HasFresh i where
- freshLens :: Lens' TCState i
- nextFresh' :: i -> i
class Monad m => MonadFresh i m where
- fresh :: m i
class FreshName a where
- freshName_ :: MonadFresh NameId m => a -> m Name
class Monad m => MonadStConcreteNames m where
- runStConcreteNames :: StateT ConcreteNames m a -> m a
- useConcreteNames :: m ConcreteNames
- modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
data ModuleCheckMode
- = ModuleScopeChecked
- | ModuleTypeChecked
class LensClosure b a | b -> a where
- lensClosure :: Lens' b (Closure a)
class LensTCEnv a where
- lensTCEnv :: Lens' a TCEnv
data WhyCheckModality
- = ConstructorType
- | IndexedClause
- | IndexedClauseArg Name Name
- | GeneratedClause
data IsForced
- = Forced
- | NotForced
data Candidate = Candidate {
- candidateKind :: CandidateKind
- candidateTerm :: Term
- candidateType :: Type
- candidateOverlap :: OverlapMode
}
data Judgement a
- = HasType {
  - jMetaId :: a
  - jComparison :: Comparison
  - jMetaType :: Type
  }
- | IsSort {
  - jMetaId :: a
  - jMetaType :: Type
  }
data DoGeneralize
- = YesGeneralizeVar
- | YesGeneralizeMeta
- | NoGeneralize
data GeneralizedValue = GeneralizedValue {
- genvalCheckpoint :: CheckpointId
- genvalTerm :: Term
- genvalType :: Type
}
newtype MetaPriority = MetaPriority Int
data MetaInstantiation
- = InstV Instantiation
- | OpenMeta MetaKind
- | BlockedConst Term
- | PostponedTypeCheckingProblem (Closure TypeCheckingProblem)
data Listener
- = EtaExpand MetaId
- | CheckConstraint Nat ProblemConstraint
data Frozen
- = Frozen
- | Instantiable
data Instantiation = Instantiation {
- instTel :: [Arg String]
- instBody :: Term
}
data TypeCheckingProblem
- = CheckExpr Comparison Expr Type
- | CheckArgs Comparison ExpandHidden Range [NamedArg Expr] Type Type (ArgsCheckState CheckedTarget -> TCM Term)
- | CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (List1 QName) Args Type Int Term Type PrincipalArgTypeMetas
- | CheckLambda Comparison (Arg (List1 (WithHiding Name), Maybe Type)) Expr Type
- | DoQuoteTerm Comparison Term Type
data RemoteMetaVariable = RemoteMetaVariable {
- rmvInstantiation :: Instantiation
- rmvModality :: Modality
- rmvJudgement :: Judgement MetaId
}
data CheckedTarget
- = CheckedTarget (Maybe ProblemId)
- | NotCheckedTarget
data PrincipalArgTypeMetas = PrincipalArgTypeMetas {
- patmMetas :: Args
- patmRemainder :: Type
}
data ExpandHidden
- = ExpandLast
- | DontExpandLast
- | ReallyDontExpandLast
data ArgsCheckState a = ACState {
- acRanges :: [Maybe Range]
- acElims :: Elims
- acConstraints :: [Maybe (Abs Constraint)]
- acType :: Type
- acData :: a
}
data InteractionPoint = InteractionPoint {
- ipRange :: Range
- ipMeta :: Maybe MetaId
- ipSolved :: Bool
- ipClause :: IPClause
- ipBoundary :: IPBoundary
}
data IPClause
- = IPClause {
  - ipcQName :: QName
  - ipcClauseNo :: Int
  - ipcType :: Type
  - ipcWithSub :: Maybe Substitution
  - ipcClause :: SpineClause
  - ipcClosure :: Closure ()
  }
- | IPNoClause
type IPBoundary = IPBoundary' Term
data Overapplied
- = Overapplied
- | NotOverapplied
newtype IPBoundary' t = IPBoundary {
- getBoundary :: Map (IntMap Bool) t
}
type Sections = Map ModuleName Section
type RewriteRuleMap = HashMap QName RewriteRules
data InstanceTable = InstanceTable {
- _itableTree :: DiscrimTree QName
- _itableCounts :: Map QName Int
}
type LocalDisplayForm = Open DisplayForm
data DisplayTerm
- = DWithApp DisplayTerm [DisplayTerm] Elims
- | DCon ConHead ConInfo [Arg DisplayTerm]
- | DDef QName [Elim' DisplayTerm]
- | DDot' Term Elims
- | DTerm' Term Elims
data NLPat
- = PVar !Int [Arg Int]
- | PDef QName PElims
- | PLam ArgInfo (Abs NLPat)
- | PPi (Dom NLPType) (Abs NLPType)
- | PSort NLPSort
- | PBoundVar !Int PElims
- | PTerm Term
type PElims = [Elim' NLPat]
data NLPType = NLPType {
- nlpTypeSort :: NLPSort
- nlpTypeUnEl :: NLPat
}
data NLPSort
- = PUniv Univ NLPat
- | PInf Univ Integer
- | PSizeUniv
- | PLockUniv
- | PLevelUniv
- | PIntervalUniv
data RewriteRule = RewriteRule {
- rewName :: QName
- rewContext :: Telescope
- rewHead :: QName
- rewPats :: PElims
- rewRHS :: Term
- rewType :: Type
- rewFromClause :: Bool
}
data Defn
- = AxiomDefn AxiomData
- | DataOrRecSigDefn DataOrRecSigData
- | GeneralizableVar
- | AbstractDefn Defn
- | FunctionDefn FunctionData
- | DatatypeDefn DatatypeData
- | RecordDefn RecordData
- | ConstructorDefn ConstructorData
- | PrimitiveDefn PrimitiveData
- | PrimitiveSortDefn PrimitiveSortData
data NumGeneralizableArgs
- = NoGeneralizableArgs
- | SomeGeneralizableArgs !Int
type CompiledRepresentation = Map BackendName [CompilerPragma]
type Face = [(Term, Bool)]
data ExtLamInfo = ExtLamInfo {
- extLamModule :: ModuleName
- extLamAbsurd :: Bool
- extLamSys :: !(Maybe System)
}
data Projection = Projection {
- projProper :: Maybe QName
- projOrig :: QName
- projFromType :: Arg QName
- projIndex :: Int
- projLams :: ProjLams
}
newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
}
data EtaEquality
- = Specified {
  - theEtaEquality :: !HasEta
  }
- | Inferred {
  - theEtaEquality :: !HasEta
  }
data FunctionFlag
- = FunStatic
- | FunInline
- | FunMacro
- | FunFirstOrder
- | FunErasure
- | FunAbstract
- | FunProj
data CompKit = CompKit {
- nameOfHComp :: Maybe QName
- nameOfTransp :: Maybe QName
}
data AxiomData = AxiomData {
- _axiomConstTransp :: Bool
}
data DataOrRecSigData = DataOrRecSigData {
- _datarecPars :: Int
}
data FunctionData = FunctionData {
- _funClauses :: [Clause]
- _funCompiled :: Maybe CompiledClauses
- _funSplitTree :: Maybe SplitTree
- _funTreeless :: Maybe Compiled
- _funCovering :: [Clause]
- _funInv :: FunctionInverse
- _funMutual :: Maybe [QName]
- _funProjection :: Either ProjectionLikenessMissing Projection
- _funFlags :: SmallSet FunctionFlag
- _funTerminates :: Maybe Bool
- _funExtLam :: Maybe ExtLamInfo
- _funWith :: Maybe QName
- _funIsKanOp :: Maybe QName
- _funOpaque :: IsOpaque
}
data DatatypeData = DatatypeData {
- _dataPars :: Nat
- _dataIxs :: Nat
- _dataClause :: Maybe Clause
- _dataCons :: [QName]
- _dataSort :: Sort
- _dataMutual :: Maybe [QName]
- _dataAbstr :: IsAbstract
- _dataPathCons :: [QName]
- _dataTranspIx :: Maybe QName
- _dataTransp :: Maybe QName
}
data RecordData = RecordData {
- _recPars :: Nat
- _recClause :: Maybe Clause
- _recConHead :: ConHead
- _recNamedCon :: Bool
- _recFields :: [Dom QName]
- _recTel :: Telescope
- _recMutual :: Maybe [QName]
- _recEtaEquality' :: EtaEquality
- _recPatternMatching :: PatternOrCopattern
- _recInduction :: Maybe Induction
- _recTerminates :: Maybe Bool
- _recAbstr :: IsAbstract
- _recComp :: CompKit
}
data ConstructorData = ConstructorData {
- _conPars :: Int
- _conArity :: Int
- _conSrcCon :: ConHead
- _conData :: QName
- _conAbstr :: IsAbstract
- _conComp :: CompKit
- _conProj :: Maybe [QName]
- _conForced :: [IsForced]
- _conErased :: Maybe [Bool]
- _conErasure :: !Bool
- _conInline :: !Bool
}
data PrimitiveData = PrimitiveData {
- _primAbstr :: IsAbstract
- _primName :: PrimitiveId
- _primClauses :: [Clause]
- _primInv :: FunctionInverse
- _primCompiled :: Maybe CompiledClauses
- _primOpaque :: IsOpaque
}
data PrimitiveSortData = PrimitiveSortData {
- _primSortName :: BuiltinSort
- _primSortSort :: Sort
}
data ProjectionLikenessMissing
- = MaybeProjection
- | NeverProjection
type FunctionInverse = FunctionInverse' Clause
data BuiltinSort
- = SortUniv Univ
- | SortOmega Univ
- | SortIntervalUniv
- | SortLevelUniv
data FunctionInverse' c
- = NotInjective
- | Inverse (InversionMap c)
data Simplification
- = YesSimplification
- | NoSimplification
data IsReduced
- = NotReduced
- | Reduced (Blocked ())
data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
}
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
type MaybeReducedElims = [MaybeReduced Elim]
data AllowedReduction
- = ProjectionReductions
- | InlineReductions
- | CopatternReductions
- | FunctionReductions
- | RecursiveReductions
- | LevelReductions
- | TypeLevelReductions
- | UnconfirmedReductions
- | NonTerminatingReductions
type AllowedReductions = SmallSet AllowedReduction
data ReduceDefs
- = OnlyReduceDefs (Set QName)
- | DontReduceDefs (Set QName)
data PrimitiveImpl = PrimImpl Type PrimFun
type InversionMap c = Map TermHead [c]
data TermHead
- = SortHead
- | PiHead
- | ConsHead QName
- | VarHead Nat
- | UnknownHead
data BuiltinDescriptor
- = BuiltinData (TCM Type) [BuiltinId]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim PrimitiveId (Term -> TCM ())
- | BuiltinSort BuiltinSort
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
data BuiltinInfo = BuiltinInfo {
- builtinName :: BuiltinId
- builtinDesc :: BuiltinDescriptor
}
type LetBindings = Map Name (Open LetBinding)
data AbstractMode
- = AbstractMode
- | ConcreteMode
- | IgnoreAbstractMode
data UnquoteFlags = UnquoteFlags {
- _unquoteNormalise :: Bool
}
data CandidateKind
- = LocalCandidate
- | GlobalCandidate QName
data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
}
data IllegalRewriteRuleReason
- = LHSNotDefinitionOrConstructor
- | VariablesNotBoundByLHS IntSet
- | VariablesBoundMoreThanOnce IntSet
- | LHSReduces Term Term
- | HeadSymbolIsProjection QName
- | HeadSymbolIsProjectionLikeFunction QName
- | HeadSymbolIsTypeConstructor QName
- | HeadSymbolContainsMetas QName
- | ConstructorParametersNotGeneral ConHead Args
- | ContainsUnsolvedMetaVariables (Set MetaId)
- | BlockedOnProblems (Set ProblemId)
- | RequiresDefinitions (Set QName)
- | DoesNotTargetRewriteRelation
- | BeforeFunctionDefinition
- | BeforeMutualFunctionDefinition QName
- | DuplicateRewriteRule
data CallInfo = CallInfo {
- callInfoTarget :: QName
- callInfoCall :: Closure Term
}
data ErasedDatatypeReason
- = SeveralConstructors
- | NoErasedMatches
- | NoK
data SplitError
- = NotADatatype (Closure Type)
- | BlockedType Blocker (Closure Type)
- | ErasedDatatype ErasedDatatypeReason (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck {
  - cantSplitBlocker :: Maybe Blocker
  - cantSplitConName :: QName
  - cantSplitTel :: Telescope
  - cantSplitConIdx :: Args
  - cantSplitGivenIdx :: Args
  - cantSplitFailures :: [UnificationFailure]
  }
- | CosplitCatchall
- | CosplitNoTarget
- | CosplitNoRecordType (Closure Type)
- | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
- | GenericSplitError String
data UnificationFailure
- = UnifyIndicesNotVars Telescope Type Term Term Args
- | UnifyRecursiveEq Telescope Type Int Term
- | UnifyReflexiveEq Telescope Type Term
- | UnifyUnusableModality Telescope Type Int Term Modality
data NegativeUnification
- = UnifyConflict Telescope Term Term
- | UnifyCycle Telescope Int Term
data UnquoteError
- = BadVisibility String (Arg Term)
- | ConInsteadOfDef QName String String
- | DefInsteadOfCon QName String String
- | NonCanonical String Term
- | BlockedOnMeta TCState Blocker
- | PatLamWithoutClauses Term
- | UnquotePanic String
type DataOrRecordE = DataOrRecord' InductionAndEta
data IncorrectTypeForRewriteRelationReason
- = ShouldAcceptAtLeastTwoArguments
- | FinalTwoArgumentsNotVisible
- | TypeDoesNotEndInSort Type Telescope
data InvalidFileNameReason
- = DoesNotCorrespondToValidModuleName
- | RootNameModuleNotAQualifiedModuleName Text
data InductionAndEta = InductionAndEta {
- recordInduction :: Maybe Induction
- recordEtaEquality :: EtaEquality
}
data ReduceEnv = ReduceEnv {
- redEnv :: TCEnv
- redSt :: TCState
- redPred :: Maybe (MetaId -> ReduceM Bool)
}
newtype BlockT m a = BlockT {
- unBlockT :: ExceptT Blocker m a
}
pattern Function :: [Clause] -> Maybe CompiledClauses -> Maybe SplitTree -> Maybe Compiled -> [Clause] -> FunctionInverse -> Maybe [QName] -> Either ProjectionLikenessMissing Projection -> SmallSet FunctionFlag -> Maybe Bool -> Maybe ExtLamInfo -> Maybe QName -> Maybe QName -> IsOpaque -> Defn
pattern Constructor :: Int -> Int -> ConHead -> QName -> IsAbstract -> CompKit -> Maybe [QName] -> [IsForced] -> Maybe [Bool] -> Bool -> Bool -> Defn
pattern Datatype :: Nat -> Nat -> Maybe Clause -> [QName] -> Sort -> Maybe [QName] -> IsAbstract -> [QName] -> Maybe QName -> Maybe QName -> Defn
pattern Primitive :: IsAbstract -> PrimitiveId -> [Clause] -> FunctionInverse -> Maybe CompiledClauses -> IsOpaque -> Defn
pattern Record :: Nat -> Maybe Clause -> ConHead -> Bool -> [Dom QName] -> Telescope -> Maybe [QName] -> EtaEquality -> PatternOrCopattern -> Maybe Induction -> Maybe Bool -> IsAbstract -> CompKit -> Defn
pattern Axiom :: Bool -> Defn
pattern DDot :: Term -> DisplayTerm
pattern DTerm :: Term -> DisplayTerm
pattern PType :: NLPat -> NLPSort
pattern PProp :: NLPat -> NLPSort
pattern PSSet :: NLPat -> NLPSort
pattern DataOrRecSig :: Int -> Defn
pattern PrimitiveSort :: BuiltinSort -> Sort -> Defn
pattern SortProp :: BuiltinSort
pattern SortSet :: BuiltinSort
pattern SortStrictSet :: BuiltinSort
pattern SortPropOmega :: BuiltinSort
pattern SortSetOmega :: BuiltinSort
pattern SortStrictSetOmega :: BuiltinSort
typeError :: (HasCallStack, MonadTCError m) => TypeError -> m a
internalError :: (HasCallStack, MonadTCM tcm) => String -> tcm a
runReduceM :: ReduceM a -> TCM a
initState :: TCState
defaultInteractionOutputCallback :: InteractionOutputCallback
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
askR :: ReduceM ReduceEnv
defAbstract :: Definition -> IsAbstract
genericError :: (HasCallStack, MonadTCError m) => String -> m a
stModuleToSource :: Lens' TCState ModuleToSource
useTC :: ReadTCState m => Lens' TCState a -> m a
defOpaque :: Definition -> IsOpaque
initPersistentState :: PersistentTCState
initialMetaId :: MetaId
initPreScopeState :: PreScopeState
emptySignature :: Signature
initPostScopeState :: PostScopeState
stTokens :: Lens' TCState HighlightingInfo
stImports :: Lens' TCState Signature
stImportedModules :: Lens' TCState (Set TopLevelModuleName)
stVisitedModules :: Lens' TCState VisitedModules
stScope :: Lens' TCState ScopeInfo
stPatternSyns :: Lens' TCState PatternSynDefns
stPatternSynImports :: Lens' TCState PatternSynDefns
stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
stPragmaOptions :: Lens' TCState PragmaOptions
stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stForeignCode :: Lens' TCState (Map BackendName ForeignCodeStack)
stFreshInteractionId :: Lens' TCState InteractionId
stImportedUserWarnings :: Lens' TCState (Map QName Text)
stLocalUserWarnings :: Lens' TCState (Map QName Text)
getUserWarnings :: ReadTCState m => m (Map QName Text)
useR :: ReadTCState m => Lens' TCState a -> m a
stWarningOnImport :: Lens' TCState (Maybe Text)
stImportedPartialDefs :: Lens' TCState (Set QName)
stLocalPartialDefs :: Lens' TCState (Set QName)
getPartialDefs :: ReadTCState m => m (Set QName)
stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
stBackends :: Lens' TCState [Backend_boot TCM]
stProjectConfigs :: Lens' TCState (Map FilePath ProjectConfig)
stAgdaLibFiles :: Lens' TCState (Map FilePath AgdaLibFile)
stTopLevelModuleNames :: Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stImportedMetaStore :: Lens' TCState RemoteMetaStore
stCopiedNames :: Lens' TCState (HashMap QName QName)
stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
stFreshNameId :: Lens' TCState NameId
stFreshOpaqueId :: Lens' TCState OpaqueId
stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
stSyntaxInfo :: Lens' TCState HighlightingInfo
stDisambiguatedNames :: Lens' TCState DisambiguatedNames
stOpenMetaStore :: Lens' TCState LocalMetaStore
stSolvedMetaStore :: Lens' TCState LocalMetaStore
stInteractionPoints :: Lens' TCState InteractionPoints
stAwakeConstraints :: Lens' TCState Constraints
stSleepingConstraints :: Lens' TCState Constraints
stDirty :: Lens' TCState Bool
stOccursCheckDefs :: Lens' TCState (Set QName)
stSignature :: Lens' TCState Signature
stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
stImportsDisplayForms :: Lens' TCState DisplayForms
stImportedDisplayForms :: Lens' TCState DisplayForms
stCurrentModule :: Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stInstanceDefs :: Lens' TCState TempInstanceTable
sigInstances :: Lens' Signature InstanceTable
stTemporaryInstances :: Lens' TCState (Set QName)
stInstanceTree :: Lens' TCState (DiscrimTree QName)
itableTree :: Lens' InstanceTable (DiscrimTree QName)
stConcreteNames :: Lens' TCState ConcreteNames
stUsedNames :: Lens' TCState (Map RawName (DList RawName))
stShadowingNames :: Lens' TCState (Map Name (DList RawName))
stStatistics :: Lens' TCState Statistics
stTCWarnings :: Lens' TCState [TCWarning]
stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stFreshMetaId :: Lens' TCState MetaId
stFreshMutualId :: Lens' TCState MutualId
stFreshProblemId :: Lens' TCState ProblemId
stFreshCheckpointId :: Lens' TCState CheckpointId
stFreshInt :: Lens' TCState Int
stAreWeCaching :: Lens' TCState Bool
stPostponeInstanceSearch :: Lens' TCState Bool
stConsideringInstance :: Lens' TCState Bool
stInstantiateBlocking :: Lens' TCState Bool
stBuiltinThings :: TCState -> BuiltinThings PrimFun
unionBuiltin :: Builtin a -> Builtin a -> Builtin a
nextFresh :: HasFresh i => TCState -> (i, TCState)
freshName :: MonadFresh NameId m => Range -> String -> m Name
freshNoName :: MonadFresh NameId m => Range -> m Name
freshNoName_ :: MonadFresh NameId m => m Name
freshRecordName :: MonadFresh NameId m => m Name
stateTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m (r, a)) -> m r
iFullHash :: Interface -> Hash
intSignature :: Lens' Interface Signature
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
fromCmp :: Comparison -> CompareDirection
flipCmp :: CompareDirection -> CompareDirection
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
suffixNameSuggestion :: MetaNameSuggestion -> ArgName -> MetaNameSuggestion
getMetaInfo :: MetaVariable -> Closure Range
normalMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
getMetaScope :: MetaVariable -> ScopeInfo
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
metaFrozen :: Lens' MetaVariable Frozen
_mvInfo :: Lens' MetaVariable MetaInfo
aModeToDef :: AbstractMode -> Maybe IsAbstract
aDefToMode :: IsAbstract -> AbstractMode
sigSections :: Lens' Signature Sections
sigDefinitions :: Lens' Signature Definitions
sigRewriteRules :: Lens' Signature RewriteRuleMap
secTelescope :: Lens' Section Telescope
defaultDisplayForm :: QName -> [LocalDisplayForm]
lensTheDef :: Lens' Definition Defn
defaultDefn :: ArgInfo -> QName -> Type -> Language -> Defn -> Definition
noCompiledRep :: CompiledRepresentation
jsBackendName :: BackendName
ghcBackendName :: BackendName
modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
projDropPars :: Projection -> ProjOrigin -> Term
projArgInfo :: Projection -> ArgInfo
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
emptyCompKit :: CompKit
defaultAxiom :: Defn
constTranspAxiom :: Defn
axiomConstTransp :: Defn -> Bool
datarecPars :: Defn -> Int
funClauses :: Defn -> [Clause]
funCompiled :: Defn -> Maybe CompiledClauses
funSplitTree :: Defn -> Maybe SplitTree
funTreeless :: Defn -> Maybe Compiled
funCovering :: Defn -> [Clause]
funInv :: Defn -> FunctionInverse
funMutual :: Defn -> Maybe [QName]
funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funFlags :: Defn -> SmallSet FunctionFlag
funTerminates :: Defn -> Maybe Bool
funExtLam :: Defn -> Maybe ExtLamInfo
funWith :: Defn -> Maybe QName
funIsKanOp :: Defn -> Maybe QName
funOpaque :: Defn -> IsOpaque
dataPars :: Defn -> Nat
dataIxs :: Defn -> Nat
dataClause :: Defn -> Maybe Clause
dataCons :: Defn -> [QName]
dataSort :: Defn -> Sort
dataMutual :: Defn -> Maybe [QName]
dataAbstr :: Defn -> IsAbstract
dataPathCons :: Defn -> [QName]
dataTranspIx :: Defn -> Maybe QName
dataTransp :: Defn -> Maybe QName
recPars :: Defn -> Nat
recClause :: Defn -> Maybe Clause
recConHead :: Defn -> ConHead
recNamedCon :: Defn -> Bool
recFields :: Defn -> [Dom QName]
recTel :: Defn -> Telescope
recMutual :: Defn -> Maybe [QName]
recEtaEquality' :: Defn -> EtaEquality
recPatternMatching :: Defn -> PatternOrCopattern
recInduction :: Defn -> Maybe Induction
recTerminates :: Defn -> Maybe Bool
recAbstr :: Defn -> IsAbstract
recComp :: Defn -> CompKit
conPars :: Defn -> Int
conArity :: Defn -> Int
conSrcCon :: Defn -> ConHead
conData :: Defn -> QName
conAbstr :: Defn -> IsAbstract
conComp :: Defn -> CompKit
conProj :: Defn -> Maybe [QName]
conForced :: Defn -> [IsForced]
conErased :: Defn -> Maybe [Bool]
conErasure :: Defn -> Bool
conInline :: Defn -> Bool
primAbstr :: Defn -> IsAbstract
primName :: Defn -> PrimitiveId
primClauses :: Defn -> [Clause]
primInv :: Defn -> FunctionInverse
primCompiled :: Defn -> Maybe CompiledClauses
primOpaque :: Defn -> IsOpaque
primSortName :: Defn -> BuiltinSort
primSortSort :: Defn -> Sort
lensFunction :: Lens' Defn FunctionData
lensConstructor :: Lens' Defn ConstructorData
lensRecord :: Lens' Defn RecordData
lensRecTel :: Lens' RecordData Telescope
lensRecEta :: Lens' RecordData EtaEquality
recRecursive :: Defn -> Bool
recRecursive_ :: RecordData -> Bool
recEtaEquality :: Defn -> HasEta
_recEtaEquality :: RecordData -> HasEta
emptyFunctionData :: HasOptions m => m FunctionData
emptyFunctionData_ :: Bool -> FunctionData
emptyFunction :: HasOptions m => m Defn
emptyFunction_ :: Bool -> Defn
funFlag_ :: FunctionFlag -> Lens' FunctionData Bool
funFlag :: FunctionFlag -> Lens' Defn Bool
funStatic :: Lens' Defn Bool
funInline :: Lens' Defn Bool
funMacro :: Lens' Defn Bool
funMacro_ :: Lens' FunctionData Bool
funFirstOrder :: Lens' Defn Bool
funErasure :: Lens' Defn Bool
funAbstract :: Lens' Defn Bool
funAbstr :: Lens' Defn IsAbstract
funAbstract_ :: Lens' FunctionData Bool
funAbstr_ :: Lens' FunctionData IsAbstract
funProj :: Lens' Defn Bool
funProj_ :: Lens' FunctionData Bool
isMacro :: Defn -> Bool
isEmptyFunction :: Defn -> Bool
isExtendedLambda :: Defn -> Bool
isWithFunction :: Defn -> Bool
isCopatternLHS :: [Clause] -> Bool
recCon :: Defn -> QName
defIsRecord :: Defn -> Bool
defIsDataOrRecord :: Defn -> Bool
defConstructors :: Defn -> [QName]
redReturn :: a -> ReduceM (Reduced a' a)
redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
notReduced :: a -> MaybeReduced a
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
allReductions :: AllowedReductions
reallyAllReductions :: AllowedReductions
reduceAllDefs :: ReduceDefs
locallyReduceDefs :: MonadTCEnv m => ReduceDefs -> m a -> m a
locallyTC :: MonadTCEnv m => Lens' TCEnv a -> (a -> a) -> m b -> m b
eReduceDefs :: Lens' TCEnv ReduceDefs
locallyReduceAllDefs :: MonadTCEnv m => m a -> m a
shouldReduceDef :: MonadTCEnv m => QName -> m Bool
asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
toReduceDefs :: (Bool, [QName]) -> ReduceDefs
fromReduceDefs :: ReduceDefs -> (Bool, [QName])
locallyReconstructed :: MonadTCEnv m => m a -> m a
eReconstructed :: Lens' TCEnv Bool
isReconstructed :: MonadTCEnv m => m Bool
primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
defClauses :: Definition -> [Clause]
defCompiled :: Definition -> Maybe CompiledClauses
defParameters :: Definition -> Maybe Nat
defInverse :: Definition -> FunctionInverse
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
defNonterminating :: Definition -> Bool
defTerminationUnconfirmed :: Definition -> Bool
defForced :: Definition -> [IsForced]
itableCounts :: Lens' InstanceTable (Map QName Int)
ifTopLevelAndHighlightingLevelIsOr :: MonadTCEnv tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs :: MonadTCEnv tcm => HighlightingLevel -> tcm () -> tcm ()
initEnv :: TCEnv
defaultUnquoteFlags :: UnquoteFlags
unquoteNormalise :: Lens' UnquoteFlags Bool
eUnquoteNormalise :: Lens' TCEnv Bool
eUnquoteFlags :: Lens' TCEnv UnquoteFlags
eContext :: Lens' TCEnv Context
eLetBindings :: Lens' TCEnv LetBindings
eCurrentModule :: Lens' TCEnv ModuleName
eCurrentPath :: Lens' TCEnv (Maybe AbsolutePath)
eAnonymousModules :: Lens' TCEnv [(ModuleName, Nat)]
eImportPath :: Lens' TCEnv [TopLevelModuleName]
eMutualBlock :: Lens' TCEnv (Maybe MutualId)
eTerminationCheck :: Lens' TCEnv (TerminationCheck ())
eCoverageCheck :: Lens' TCEnv CoverageCheck
eMakeCase :: Lens' TCEnv Bool
eSolvingConstraints :: Lens' TCEnv Bool
eCheckingWhere :: Lens' TCEnv Bool
eWorkingOnTypes :: Lens' TCEnv Bool
eAssignMetas :: Lens' TCEnv Bool
eActiveProblems :: Lens' TCEnv (Set ProblemId)
eAbstractMode :: Lens' TCEnv AbstractMode
eRelevance :: Lens' TCEnv Relevance
eQuantity :: Lens' TCEnv Quantity
eHardCompileTimeMode :: Lens' TCEnv Bool
eSplitOnStrict :: Lens' TCEnv Bool
eDisplayFormsEnabled :: Lens' TCEnv Bool
eFoldLetBindings :: Lens' TCEnv Bool
eRange :: Lens' TCEnv Range
eHighlightingRange :: Lens' TCEnv Range
eCall :: Lens' TCEnv (Maybe (Closure Call))
eHighlightingLevel :: Lens' TCEnv HighlightingLevel
eHighlightingMethod :: Lens' TCEnv HighlightingMethod
eExpandLast :: Lens' TCEnv ExpandHidden
eExpandLastBool :: Lens' TCEnv Bool
isExpandLast :: ExpandHidden -> Bool
toExpandLast :: Bool -> ExpandHidden
eAppDef :: Lens' TCEnv (Maybe QName)
eSimplification :: Lens' TCEnv Simplification
eAllowedReductions :: Lens' TCEnv AllowedReductions
eReduceDefsPair :: Lens' TCEnv (Bool, [QName])
eInjectivityDepth :: Lens' TCEnv Int
eCompareBlocked :: Lens' TCEnv Bool
ePrintDomainFreePi :: Lens' TCEnv Bool
ePrintMetasBare :: Lens' TCEnv Bool
eInsideDotPattern :: Lens' TCEnv Bool
eInstanceDepth :: Lens' TCEnv Int
eIsDebugPrinting :: Lens' TCEnv Bool
ePrintingPatternLambdas :: Lens' TCEnv [QName]
eCallByNeed :: Lens' TCEnv Bool
eCurrentCheckpoint :: Lens' TCEnv CheckpointId
eCheckpoints :: Lens' TCEnv (Map CheckpointId Substitution)
eGeneralizeMetas :: Lens' TCEnv DoGeneralize
eGeneralizedVars :: Lens' TCEnv (Map QName GeneralizedValue)
eActiveBackendName :: Lens' TCEnv (Maybe BackendName)
eConflComputingOverlap :: Lens' TCEnv Bool
eCurrentlyElaborating :: Lens' TCEnv Bool
currentModality :: MonadTCEnv m => m Modality
viewTC :: MonadTCEnv m => Lens' TCEnv a -> m a
onLetBindingType :: (Dom Type -> Dom Type) -> LetBinding -> LetBinding
isDontExpandLast :: ExpandHidden -> Bool
recordFieldWarningToError :: RecordFieldWarning -> TypeError
warningName :: Warning -> WarningName
illegalRewriteWarningName :: IllegalRewriteRuleReason -> WarningName
isSourceCodeWarning :: WarningName -> Bool
tcWarningOrigin :: TCWarning -> SrcFile
sizedTypesOption :: HasOptions m => m Bool
guardednessOption :: HasOptions m => m Bool
withoutKOption :: HasOptions m => m Bool
cubicalOption :: HasOptions m => m (Maybe Cubical)
cubicalCompatibleOption :: HasOptions m => m Bool
enableCaching :: HasOptions m => m Bool
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
reduceEnv :: Lens' ReduceEnv TCEnv
reduceSt :: Lens' ReduceEnv TCState
unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
thenReduce :: ReduceM a -> ReduceM b -> ReduceM b
beforeReduce :: ReduceM a -> ReduceM b -> ReduceM a
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
getsTC :: ReadTCState m => (TCState -> a) -> m a
modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
setTCLens :: MonadTCState m => Lens' TCState a -> a -> m ()
setTCLens' :: MonadTCState m => Lens' TCState a -> a -> m ()
modifyTCLens :: MonadTCState m => Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' :: MonadTCState m => Lens' TCState a -> (a -> a) -> m ()
modifyTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m a) -> m ()
stateTCLens :: MonadTCState m => Lens' TCState a -> (a -> (r, a)) -> m r
runBlocked :: Monad m => BlockT m a -> m (Either Blocker a)
pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
returnTCMT :: Applicative m => a -> TCMT m a
bindTCMT :: Monad m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
thenTCMT :: Applicative m => TCMT m a -> TCMT m b -> TCMT m b
fmapTCMT :: Functor m => (a -> b) -> TCMT m a -> TCMT m b
apTCMT :: Applicative m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
finally_ :: TCM a -> TCM b -> TCM a
typeError' :: MonadTCError m => CallStack -> TypeError -> m a
locatedTypeError :: MonadTCError m => (a -> TypeError) -> HasCallStack => a -> m b
genericDocError :: (HasCallStack, MonadTCError m) => Doc -> m a
typeError'_ :: (MonadTCEnv m, ReadTCState m) => CallStack -> TypeError -> m TCErr
typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m) => TypeError -> m 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 ()
patternInTeleName :: String
extendedLambdaName :: String
isExtendedLambdaName :: QName -> Bool
absurdLambdaName :: String
isAbsurdLambdaName :: QName -> Bool
generalizedFieldName :: String
getGeneralizedFieldName :: QName -> Maybe String
module Agda.TypeChecking.Monad.Base.Types
class (Functor m, Applicative m, Monad m) => HasOptions m where
- pragmaOptions :: m PragmaOptions
- commandLineOptions :: m CommandLineOptions
data RecordFieldWarning

Documentation

data Constraint Source #

Constructors

ValueCmp Comparison CompareAs Term Term
ValueCmpOnFace Comparison Term Type Term Term
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
SortCmp Comparison Sort Sort
LevelCmp Comparison Level Level
HasBiggerSort Sort
HasPTSRule (Dom Type) (Abs Sort)
CheckDataSort QName Sort	Check that the sort `Term` of data type `QName` admits data/record types. E.g., sorts `IUniv`, `SizeUniv` etc. do not admit such constructions. See `checkDataSort`.
CheckMetaInst MetaId
CheckType Type
UnBlock MetaId	Meta created for a term blocked by a postponed type checking problem or unsolved constraints. The `MetaInstantiation` for the meta (when unsolved) is either `BlockedConst` or `PostponedTypeCheckingProblem`.
IsEmpty Range Type	The range is the one of the absurd pattern.
CheckSizeLtSat Term	Check that the `Term` is either not a SIZELT or a non-empty SIZELT.
FindInstance MetaId (Maybe [Candidate])	the first argument is the instance argument and the second one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)
ResolveInstanceHead QName	Resolve the head symbol of the type that the given instance targets
CheckFunDef DefInfo QName [Clause] TCErr	Last argument is the error causing us to postpone.
UnquoteTactic Term Term Type	First argument is computation and the others are hole and goal type
CheckLockedVars Term Type (Arg Term) Type	`CheckLockedVars t ty lk lk_ty` with `t : ty`, `lk : lk_ty` and `t lk` well-typed.
UsableAtModality WhyCheckModality (Maybe Sort) Modality Term	Is the term usable at the given modality? This check should run if the `Sort` is `Nothing` or `isFibrant`.

Instances

Instances details

TermLike Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source # foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #
AllMetas Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allMetas :: Monoid m => (MetaId -> m) -> Constraint -> m Source #
HasRange Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range Source #
Reify Constraint Source #
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo Constraint Source # Methods reify :: MonadReify m => Constraint -> m (ReifiesTo Constraint) Source # reifyWhen :: MonadReify m => Bool -> Constraint -> m (ReifiesTo Constraint) Source #
Free Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => Constraint -> FreeM a c Source #
MentionsMeta Constraint Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Constraint -> Bool Source #
PrettyTCM Constraint Source #
Instance details Defined in Agda.TypeChecking.Pretty.Constraint Methods prettyTCM :: MonadPretty m => Constraint -> m Doc Source #
Instantiate Constraint Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Constraint -> ReduceM Constraint Source #
InstantiateFull Constraint Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Constraint -> ReduceM Constraint Source #
Normalise Constraint Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Constraint -> ReduceM Constraint Source #
Reduce Constraint Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Constraint -> ReduceM Constraint Source # reduceB' :: Constraint -> ReduceM (Blocked Constraint) Source #
Simplify Constraint Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Constraint -> ReduceM Constraint
Subst Constraint Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg Constraint Source # Methods applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint Source #
Generic Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep Constraint :: Type -> Type # Methods from :: Constraint -> Rep Constraint x # to :: Rep Constraint x -> Constraint #
Show Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Constraint -> ShowS # show :: Constraint -> String # showList :: [Constraint] -> ShowS #
NFData Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Constraint -> () #
type ReifiesTo Constraint Source #
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo Constraint = OutputConstraint Expr Expr
type SubstArg Constraint Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Constraint = Term
type Rep Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type Rep Constraint = D1 ('MetaData "Constraint" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) ((((C1 ('MetaCons "ValueCmp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CompareAs)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "ValueCmpOnFace" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))) :+: (C1 ('MetaCons "ElimCmp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Polarity]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [IsForced]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Elim]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Elim])))) :+: C1 ('MetaCons "SortCmp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort))))) :+: ((C1 ('MetaCons "LevelCmp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Level) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Level))) :+: C1 ('MetaCons "HasBiggerSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort))) :+: (C1 ('MetaCons "HasPTSRule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs Sort))) :+: (C1 ('MetaCons "CheckDataSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: C1 ('MetaCons "CheckMetaInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId)))))) :+: (((C1 ('MetaCons "CheckType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "UnBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId))) :+: (C1 ('MetaCons "IsEmpty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "CheckSizeLtSat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "FindInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Candidate])))))) :+: ((C1 ('MetaCons "ResolveInstanceHead" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "CheckFunDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCErr)))) :+: (C1 ('MetaCons "UnquoteTactic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "CheckLockedVars" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Term)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "UsableAtModality" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyCheckModality) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Sort))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Modality) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))))))

data TypeError Source #

Constructors

InternalError String
NotImplemented String
NotSupported String
CompilationError String
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
CantResolveOverloadedConstructorsTargetingSameDatatype QName (List1 QName)	Datatype, constructors.
DoesNotConstructAnElementOf QName Type	constructor, type
WrongHidingInLHS	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.
WrongHidingInProjection QName
IllegalHidingInPostfixProjection (NamedArg Expr)
WrongNamedArgument (NamedArg Expr) [NamedName]	A function is applied to a hidden named argument it does not have. The list contains names of possible hidden arguments at this point.
WrongIrrelevanceInLambda	Wrong user-given relevance annotation in lambda.
WrongQuantityInLambda	Wrong user-given quantity annotation in lambda.
WrongCohesionInLambda	Wrong user-given cohesion annotation in lambda.
QuantityMismatch Quantity Quantity	The given quantity does not correspond to the expected quantity.
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.
UninstantiatedDotPattern Expr
ForcedConstructorNotInstantiated Pattern
IllformedProjectionPatternAbstract Pattern
IllformedProjectionPatternConcrete Pattern
CannotEliminateWithPattern (Maybe Blocker) (NamedArg Pattern) Type
CannotEliminateWithProjection (Arg Type) Bool QName
WrongNumberOfConstructorArguments QName Nat Nat
ShouldBeEmpty Type [DeBruijnPattern]
ShouldBeASort Type	The given type should have been a sort.
ShouldBePi Type	The given type should have been a pi.
ShouldBePath Type
ShouldBeRecordType Type
ShouldBeRecordPattern DeBruijnPattern
NotAProjectionPattern (NamedArg Pattern)
NotAProperTerm
InvalidTypeSort Sort	This sort is not a type expression.
InvalidType Term	This term is not a type expression.
SplitOnCoinductive
SplitOnIrrelevant (Dom Type)
SplitOnUnusableCohesion (Dom Type)
SplitOnNonVariable Term Type
SplitOnNonEtaRecord QName
SplitOnAbstract QName
SplitOnUnchecked QName
SplitOnPartial (Dom Type)
SplitInProp DataOrRecordE
DefinitionIsIrrelevant QName
DefinitionIsErased QName
ProjectionIsIrrelevant QName
VariableIsIrrelevant Name
VariableIsErased Name
VariableIsOfUnusableCohesion Name Cohesion
UnequalLevel Comparison Level Level
UnequalTerms Comparison Term Term CompareAs
UnequalTypes Comparison Type Type
UnequalRelevance Comparison Term Term	The two function types have different relevance.
UnequalQuantity Comparison Term Term	The two function types have different relevance.
UnequalCohesion Comparison Term Term	The two function types have different cohesion.
UnequalFiniteness Comparison Term Term	One of the function types has a finite domain (i.e. is a `Partia`l@) and the other isonot.
UnequalHiding Term Term	The two function types have different hiding.
UnequalSorts Sort Sort
UnequalBecauseOfUniverseConflict Comparison Term Term
NotLeqSort Sort Sort
MetaCannotDependOn MetaId Nat	The arguments are the meta variable and the parameter that it wants to depend on.
MetaOccursInItself MetaId
MetaIrrelevantSolution MetaId Term
MetaErasedSolution MetaId Term
GenericError String
GenericDocError Doc
SortOfSplitVarError (Maybe Blocker) Doc	the meta is what we might be blocked on.
BuiltinMustBeConstructor BuiltinId Expr
NoSuchBuiltinName String
DuplicateBuiltinBinding BuiltinId Term Term
NoBindingForBuiltin BuiltinId
NoBindingForPrimitive PrimitiveId
NoSuchPrimitiveFunction String
DuplicatePrimitiveBinding PrimitiveId QName QName
WrongArgInfoForPrimitive PrimitiveId ArgInfo ArgInfo
ShadowedModule Name [ModuleName]
BuiltinInParameterisedModule BuiltinId
IllegalDeclarationInDataDefinition [Declaration]	The declaration list comes from a single `NiceDeclaration`.
IllegalLetInTelescope TypedBinding
IllegalPatternInTelescope Binder
NoRHSRequiresAbsurdPattern [NamedArg Pattern]
TooManyFields QName [Name] [Name]	Record type, fields not supplied by user, non-fields but supplied.
DuplicateFields [Name]
DuplicateConstructors [Name]
DuplicateOverlapPragma QName OverlapMode OverlapMode
WithOnFreeVariable Expr Term
UnexpectedWithPatterns [Pattern]
WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
IllTypedPatternAfterWithAbstraction Pattern
FieldOutsideRecord
ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
GeneralizeCyclicDependency
GeneralizeUnsolvedMeta
ReferencesFutureVariables Term (NonEmpty Int) (Arg Term) Int	The first term references the given list of variables, which are in "the future" with respect to the given lock (and its leftmost variable)
DoesNotMentionTicks Term Type (Arg Term)	Arguments: later term, its type, lock term. The lock term does not mention any @lock variables.
MismatchedProjectionsError QName QName
AttributeKindNotEnabled String String String
InvalidProjectionParameter (NamedArg Expr)
TacticAttributeNotAllowed
CannotRewriteByNonEquation Type
MacroResultTypeMismatch Type
NamedWhereModuleInRefinedContext [Term] [String]
CubicalPrimitiveNotFullyApplied QName
TooManyArgumentsToLeveledSort QName
TooManyArgumentsToUnivOmega QName
ComatchingDisabledForRecord QName
BuiltinMustBeIsOne Term
IncorrectTypeForRewriteRelation Term IncorrectTypeForRewriteRelationReason
UnexpectedParameter LamBinding
NoParameterOfName ArgName
UnexpectedModalityAnnotationInParameter LamBinding
ExpectedBindingForParameter (Dom Type) (Abs Type)
UnexpectedTypeSignatureForParameter (List1 (NamedArg Binder))
SortDoesNotAdmitDataDefinitions QName Sort
SortCannotDependOnItsIndex QName Type
UnusableAtModality WhyCheckModality Modality Term
SplitError SplitError
ImpossibleConstructor QName NegativeUnification
TooManyPolarities QName Int
RecursiveRecordNeedsInductivity QName	A record type inferred as recursive needs a manual declaration whether it should be inductively or coinductively. Sized type errors
CannotSolveSizeConstraints (List1 (ProblemConstraint, HypSizeConstraint)) Doc	The list of constraints is given redundantly as pairs of `ProblemConstraint` (original constraint) and `HypSizeConstraint` (form with size assumptions in context spelled out). The `Doc` is some extra reason for why solving failed.
ContradictorySizeConstraint (ProblemConstraint, HypSizeConstraint)
EmptyTypeOfSizes Term	This type, representing a type of sizes, might be empty.
FunctionTypeInSizeUniv Term	This term, a function type constructor, lives in `SizeUniv`, which is not allowed. Import errors
LibraryError LibErrors	Collected errors when processing the `.agda-lib` file.
LocalVsImportedModuleClash ModuleName
SolvedButOpenHoles	Some interaction points (holes) have not been 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]
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName	Found module name, expected module name.
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.
InvalidFileName AbsolutePath InvalidFileNameReason	The file name does not correspond to a module name. Scope errors
BothWithAndRHS
AbstractConstructorNotInScope QName
NotInScope [QName]
NoSuchModule QName
AmbiguousName QName AmbiguousNameReason
AmbiguousModule QName (List1 ModuleName)
AmbiguousField Name [ModuleName]
AmbiguousConstructor QName [QName]
ClashingDefinition QName QName (Maybe NiceDeclaration)
ClashingModule ModuleName ModuleName
ClashingImport Name QName
ClashingModuleImport Name ModuleName
DefinitionInDifferentModule QName	The given data/record definition rests in a different module than its signature.
DuplicateImports QName [ImportedName]
InvalidPattern Pattern
RepeatedVariablesInPattern [Name]
GeneralizeNotSupportedHere QName
GeneralizedVarInLetOpenedModule QName
MultipleFixityDecls [(Name, [Fixity'])]
MultiplePolarityPragmas [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
NotValidBeforeField NiceDeclaration
NothingAppliedToHiddenArg Expr
NothingAppliedToInstanceArg Expr
AsPatternInPatternSynonym
DotPatternInPatternSynonym
BadArgumentsToPatternSynonym AmbiguousQName
TooFewArgumentsToPatternSynonym AmbiguousQName
CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn))
IllegalInstanceVariableInPatternSynonym Name	This variable is bound in the lhs of the pattern synonym in instance position, but not on the rhs. This is forbidden because expansion of pattern synonyms would not be faithful to availability of instances in instance search.
PatternSynonymArgumentShadowsConstructorOrPatternSynonym LHSOrPatSyn Name (List1 AbstractName)	A variable to be bound in the pattern synonym resolved on the rhs as name of a constructor or a pattern synonym. The resolvents are given in the list.
UnusedVariableInPatternSynonym Name	This variable is only bound on the lhs of the pattern synonym, not on the rhs.
UnboundVariablesInPatternSynonym [Name]	These variables are only bound on the rhs of the pattern synonym, not on the lhs. Operator errors
NoParseForApplication (List2 Expr)
AmbiguousParseForApplication (List2 Expr) (List1 Expr)
NoParseForLHS LHSOrPatSyn [Pattern] Pattern	The list contains patterns that failed to be interpreted. If it is non-empty, the first entry could be printed as error hint.
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]	Pattern and its possible interpretations.
AmbiguousProjection QName [QName]
AmbiguousOverloadedProjection (List1 QName) Doc
OperatorInformation [NotationSection] TypeError
InstanceNoCandidate Type [(Term, TCErr)]
UnquoteFailed UnquoteError
DeBruijnIndexOutOfScope Nat Telescope [Name]
NeedOptionCopatterns
NeedOptionRewriting
NeedOptionProp
NeedOptionTwoLevel
NonFatalErrors [TCWarning]
InstanceSearchDepthExhausted Term Type Int
TriedToCopyConstrainedPrim QName
CustomBackendError String Doc	Used for backend-specific errors. The string is the backend name.

Instances

Instances details

PrettyTCM TypeError Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
Generic TypeError Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep TypeError :: Type -> Type # Methods from :: TypeError -> Rep TypeError x # to :: Rep TypeError x -> TypeError #
Show TypeError Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TypeError -> ShowS # show :: TypeError -> String # showList :: [TypeError] -> ShowS #
NFData TypeError Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: TypeError -> () #
type Rep TypeError Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type Rep TypeError = D1 ('MetaData "TypeError" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (((((((C1 ('MetaCons "InternalError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "NotImplemented" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "NotSupported" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "CompilationError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "PropMustBeSingleton" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataMustEndInSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))) :+: ((C1 ('MetaCons "ShouldEndInApplicationOfTheDatatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "ShouldBeAppliedToTheDatatypeParameters" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ShouldBeApplicationOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: (C1 ('MetaCons "ConstructorPatternInWrongDatatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "CantResolveOverloadedConstructorsTargetingSameDatatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 QName))) :+: C1 ('MetaCons "DoesNotConstructAnElementOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))) :+: (((C1 ('MetaCons "WrongHidingInLHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WrongHidingInLambda" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "WrongHidingInApplication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "WrongHidingInProjection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "IllegalHidingInPostfixProjection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))) :+: C1 ('MetaCons "WrongNamedArgument" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedName]))))) :+: ((C1 ('MetaCons "WrongIrrelevanceInLambda" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WrongQuantityInLambda" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongCohesionInLambda" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "QuantityMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity)) :+: (C1 ('MetaCons "HidingMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: C1 ('MetaCons "RelevanceMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance))))))) :+: ((((C1 ('MetaCons "UninstantiatedDotPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: (C1 ('MetaCons "ForcedConstructorNotInstantiated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :+: C1 ('MetaCons "IllformedProjectionPatternAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)))) :+: (C1 ('MetaCons "IllformedProjectionPatternConcrete" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :+: (C1 ('MetaCons "CannotEliminateWithPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Blocker)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Pattern)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "CannotEliminateWithProjection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))))) :+: ((C1 ('MetaCons "WrongNumberOfConstructorArguments" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat))) :+: (C1 ('MetaCons "ShouldBeEmpty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeBruijnPattern])) :+: C1 ('MetaCons "ShouldBeASort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "ShouldBePi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "ShouldBePath" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ShouldBeRecordType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))) :+: (((C1 ('MetaCons "ShouldBeRecordPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeBruijnPattern)) :+: (C1 ('MetaCons "NotAProjectionPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Pattern))) :+: C1 ('MetaCons "NotAProperTerm" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "InvalidTypeSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: (C1 ('MetaCons "InvalidType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "SplitOnCoinductive" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "SplitOnIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))) :+: (C1 ('MetaCons "SplitOnUnusableCohesion" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))) :+: C1 ('MetaCons "SplitOnNonVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: ((C1 ('MetaCons "SplitOnNonEtaRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "SplitOnAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "SplitOnUnchecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "SplitOnPartial" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))))))) :+: (((((C1 ('MetaCons "SplitInProp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecordE)) :+: (C1 ('MetaCons "DefinitionIsIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "DefinitionIsErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: (C1 ('MetaCons "ProjectionIsIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "VariableIsIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "VariableIsErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))) :+: ((C1 ('MetaCons "VariableIsOfUnusableCohesion" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cohesion)) :+: (C1 ('MetaCons "UnequalLevel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Level) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Level))) :+: C1 ('MetaCons "UnequalTerms" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CompareAs))))) :+: (C1 ('MetaCons "UnequalTypes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "UnequalRelevance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "UnequalQuantity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))))) :+: (((C1 ('MetaCons "UnequalCohesion" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "UnequalFiniteness" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "UnequalHiding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: (C1 ('MetaCons "UnequalSorts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: (C1 ('MetaCons "UnequalBecauseOfUniverseConflict" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comparison) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "NotLeqSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort))))) :+: ((C1 ('MetaCons "MetaCannotDependOn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: (C1 ('MetaCons "MetaOccursInItself" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId)) :+: C1 ('MetaCons "MetaIrrelevantSolution" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: (C1 ('MetaCons "MetaErasedSolution" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "GenericError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "GenericDocError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc))))))) :+: ((((C1 ('MetaCons "SortOfSplitVarError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Blocker)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc)) :+: (C1 ('MetaCons "BuiltinMustBeConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BuiltinId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "NoSuchBuiltinName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "DuplicateBuiltinBinding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BuiltinId) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "NoBindingForBuiltin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BuiltinId)) :+: C1 ('MetaCons "NoBindingForPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrimitiveId))))) :+: ((C1 ('MetaCons "NoSuchPrimitiveFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "DuplicatePrimitiveBinding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrimitiveId) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: C1 ('MetaCons "WrongArgInfoForPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrimitiveId) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))))) :+: (C1 ('MetaCons "ShadowedModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleName])) :+: (C1 ('MetaCons "BuiltinInParameterisedModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BuiltinId)) :+: C1 ('MetaCons "IllegalDeclarationInDataDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))) :+: (((C1 ('MetaCons "IllegalLetInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding)) :+: (C1 ('MetaCons "IllegalPatternInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Binder)) :+: C1 ('MetaCons "NoRHSRequiresAbsurdPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern])))) :+: (C1 ('MetaCons "TooManyFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "DuplicateConstructors" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: ((C1 ('MetaCons "DuplicateOverlapPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode))) :+: (C1 ('MetaCons "WithOnFreeVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "UnexpectedWithPatterns" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern])))) :+: ((C1 ('MetaCons "WithClausePatternMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg DeBruijnPattern))) :+: C1 ('MetaCons "IllTypedPatternAfterWithAbstraction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern))) :+: (C1 ('MetaCons "FieldOutsideRecord" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleArityMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr])))))))))) :+: ((((((C1 ('MetaCons "GeneralizeCyclicDependency" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GeneralizeUnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReferencesFutureVariables" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NonEmpty Int))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Term)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :+: (C1 ('MetaCons "DoesNotMentionTicks" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Term)))) :+: (C1 ('MetaCons "MismatchedProjectionsError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "AttributeKindNotEnabled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))) :+: ((C1 ('MetaCons "InvalidProjectionParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))) :+: (C1 ('MetaCons "TacticAttributeNotAllowed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotRewriteByNonEquation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "MacroResultTypeMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "NamedWhereModuleInRefinedContext" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "CubicalPrimitiveNotFullyApplied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))))) :+: (((C1 ('MetaCons "TooManyArgumentsToLeveledSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "TooManyArgumentsToUnivOmega" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "ComatchingDisabledForRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: (C1 ('MetaCons "BuiltinMustBeIsOne" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "IncorrectTypeForRewriteRelation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IncorrectTypeForRewriteRelationReason)) :+: C1 ('MetaCons "UnexpectedParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding))))) :+: ((C1 ('MetaCons "NoParameterOfName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName)) :+: (C1 ('MetaCons "UnexpectedModalityAnnotationInParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding)) :+: C1 ('MetaCons "ExpectedBindingForParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs Type))))) :+: (C1 ('MetaCons "UnexpectedTypeSignatureForParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder)))) :+: (C1 ('MetaCons "SortDoesNotAdmitDataDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: C1 ('MetaCons "SortCannotDependOnItsIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))))) :+: ((((C1 ('MetaCons "UnusableAtModality" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyCheckModality) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Modality) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "SplitError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitError)) :+: C1 ('MetaCons "ImpossibleConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NegativeUnification)))) :+: (C1 ('MetaCons "TooManyPolarities" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "RecursiveRecordNeedsInductivity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "CannotSolveSizeConstraints" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (ProblemConstraint, HypSizeConstraint))) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc))))) :+: ((C1 ('MetaCons "ContradictorySizeConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProblemConstraint, HypSizeConstraint))) :+: (C1 ('MetaCons "EmptyTypeOfSizes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "FunctionTypeInSizeUniv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: (C1 ('MetaCons "LibraryError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LibErrors)) :+: (C1 ('MetaCons "LocalVsImportedModuleClash" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :+: C1 ('MetaCons "SolvedButOpenHoles" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "CyclicModuleDependency" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopLevelModuleName])) :+: (C1 ('MetaCons "FileNotFound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath])) :+: C1 ('MetaCons "OverlappingProjects" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbsolutePath) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName))))) :+: (C1 ('MetaCons "AmbiguousTopLevelModuleName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath])) :+: (C1 ('MetaCons "ModuleNameUnexpected" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName)) :+: C1 ('MetaCons "ModuleNameDoesntMatchFileName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath]))))) :+: ((C1 ('MetaCons "ClashingFileNamesFor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath])) :+: (C1 ('MetaCons "ModuleDefinedInOtherFile" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbsolutePath) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbsolutePath))) :+: C1 ('MetaCons "InvalidFileName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbsolutePath) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InvalidFileNameReason)))) :+: ((C1 ('MetaCons "BothWithAndRHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbstractConstructorNotInScope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "NotInScope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: C1 ('MetaCons "NoSuchModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))))))) :+: (((((C1 ('MetaCons "AmbiguousName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousNameReason)) :+: (C1 ('MetaCons "AmbiguousModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 ModuleName))) :+: C1 ('MetaCons "AmbiguousField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleName])))) :+: (C1 ('MetaCons "AmbiguousConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: (C1 ('MetaCons "ClashingDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NiceDeclaration)))) :+: C1 ('MetaCons "ClashingModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))))) :+: ((C1 ('MetaCons "ClashingImport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "ClashingModuleImport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :+: C1 ('MetaCons "DefinitionInDifferentModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: (C1 ('MetaCons "DuplicateImports" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ImportedName])) :+: (C1 ('MetaCons "InvalidPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :+: C1 ('MetaCons "RepeatedVariablesInPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))))) :+: (((C1 ('MetaCons "GeneralizeNotSupportedHere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "GeneralizedVarInLetOpenedModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "MultipleFixityDecls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, [Fixity'])])))) :+: (C1 ('MetaCons "MultiplePolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "NotAModuleExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "NotAnExpression" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "NotAValidLetBinding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration)) :+: (C1 ('MetaCons "NotValidBeforeField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration)) :+: C1 ('MetaCons "NothingAppliedToHiddenArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "NothingAppliedToInstanceArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: (C1 ('MetaCons "AsPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BadArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "TooFewArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (QName, PatternSynDefn)))))) :+: (C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "PatternSynonymArgumentShadowsConstructorOrPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSOrPatSyn) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName)))) :+: C1 ('MetaCons "UnusedVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))) :+: ((C1 ('MetaCons "UnboundVariablesInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "NoParseForApplication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 Expr))) :+: C1 ('MetaCons "AmbiguousParseForApplication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 Expr)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Expr))))) :+: (C1 ('MetaCons "NoParseForLHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSOrPatSyn) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern))) :+: (C1 ('MetaCons "AmbiguousParseForLHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSOrPatSyn) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern]))) :+: C1 ('MetaCons "AmbiguousProjection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])))))) :+: (((C1 ('MetaCons "AmbiguousOverloadedProjection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 QName)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc)) :+: (C1 ('MetaCons "OperatorInformation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NotationSection]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeError)) :+: C1 ('MetaCons "InstanceNoCandidate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term, TCErr)])))) :+: (C1 ('MetaCons "UnquoteFailed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnquoteError)) :+: (C1 ('MetaCons "DeBruijnIndexOutOfScope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: C1 ('MetaCons "NeedOptionCopatterns" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "NeedOptionRewriting" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeedOptionProp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionTwoLevel" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NonFatalErrors" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TCWarning])) :+: C1 ('MetaCons "InstanceSearchDepthExhausted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))) :+: (C1 ('MetaCons "TriedToCopyConstrainedPrim" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "CustomBackendError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc))))))))))

data Comparison Source #

Constructors

CmpEq
CmpLeq

Instances

Instances details

Pretty Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source #
PrettyTCM Comparison Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #
EmbPrj Comparison Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Comparison -> S Int32 Source # icod_ :: Comparison -> S Int32 Source # value :: Int32 -> R Comparison Source #
Generic Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep Comparison :: Type -> Type # Methods from :: Comparison -> Rep Comparison x # to :: Rep Comparison x -> Comparison #
Show Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS # show :: Comparison -> String # showList :: [Comparison] -> ShowS #
NFData Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Comparison -> () #
Eq Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Comparison -> Comparison -> Bool # (/=) :: Comparison -> Comparison -> Bool #
type Rep Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

data ModuleInfo Source #

Constructors

ModuleInfo

Fields

miInterface :: Interface
miWarnings :: [TCWarning]
Warnings were encountered when the module was type checked. These might include warnings not stored in the interface itself, specifically unsolved interaction metas. See Agda.Interaction.Imports
miPrimitive :: Bool
True if the module is a primitive module, which should always be importable.
miMode :: ModuleCheckMode
The ModuleCheckMode used to create the Interface

Instances

Instances details

Generic ModuleInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ModuleInfo :: Type -> Type # Methods from :: ModuleInfo -> Rep ModuleInfo x # to :: Rep ModuleInfo x -> ModuleInfo #
NFData ModuleInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ModuleInfo -> () #
type Rep ModuleInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "miInterface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Interface) :: S1 ('MetaSel ('Just "miWarnings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TCWarning])) :: (S1 ('MetaSel ('Just "miPrimitive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "miMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleCheckMode))))

data Definition Source #

Constructors

Defn

Fields

defArgInfo :: ArgInfo
Hiding should not be used.
defName :: QName
The canonical name, used e.g. in compilation.
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.
defArgGeneralizable :: NumGeneralizableArgs
For a generalized variable, shows how many arguments should be generalised.
defGeneralizedParams :: [Maybe Name]
Gives the name of the (bound variable) parameter for named generalized parameters. This is needed to bring it into scope when type checking the data/record definition corresponding to a type with generalized parameters.
defDisplay :: [LocalDisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe InstanceInfo
Just q when this definition is an instance.
defCopy :: Bool
Has this function been created by a module instantiation?
defMatchable :: Set QName
The set of symbols with rewrite rules that match against this symbol
defNoCompilation :: Bool
should compilers skip this? Used for e.g. cubical's comp
defInjective :: Bool
Should the def be treated as injective by the pattern matching unifier?
defCopatternLHS :: Bool
Is this a function defined by copatterns?
defBlocked :: Blocked_
What blocking tag to use when we cannot reduce this def? Used when checking a function definition is blocked on a meta in the type.
defLanguage :: !Language
The language used for the definition.
theDef :: Defn

Instances

Instances details

LensArgInfo Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source #
LensModality Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: Definition -> Modality Source # setModality :: Modality -> Definition -> Definition Source # mapModality :: (Modality -> Modality) -> Definition -> Definition Source #
LensQuantity Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: Definition -> Quantity Source # setQuantity :: Quantity -> Definition -> Definition Source # mapQuantity :: (Quantity -> Quantity) -> Definition -> Definition Source #
LensRelevance Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: Definition -> Relevance Source # setRelevance :: Relevance -> Definition -> Definition Source # mapRelevance :: (Relevance -> Relevance) -> Definition -> Definition Source #
Pretty Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Definition -> Doc Source # prettyPrec :: Int -> Definition -> Doc Source # prettyList :: [Definition] -> Doc Source #
NamesIn Definition Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Definition -> m Source #
KillRange Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definition Source #
KillRange Definitions Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
InstantiateFull Definition Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Definition -> ReduceM Definition Source #
EmbPrj Definition Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Int32 Source # icod_ :: Definition -> S Int32 Source # value :: Int32 -> R Definition Source #
Abstract Definition Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Definition -> Definition Source #
Apply Definition Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Generic Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep Definition :: Type -> Type # Methods from :: Definition -> Rep Definition x # to :: Rep Definition x -> Definition #
Show Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Definition -> ShowS # show :: Definition -> String # showList :: [Definition] -> ShowS #
NFData Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Definition -> () #
type Rep Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type Rep Definition = D1 ('MetaData "Definition" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "Defn" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "defArgInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :: S1 ('MetaSel ('Just "defName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Just "defType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Just "defPolarity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Polarity]))) :: ((S1 ('MetaSel ('Just "defArgOccurrences") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Occurrence]) :: S1 ('MetaSel ('Just "defArgGeneralizable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NumGeneralizableArgs)) :: (S1 ('MetaSel ('Just "defGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Maybe Name]) :: (S1 ('MetaSel ('Just "defDisplay") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LocalDisplayForm]) :: S1 ('MetaSel ('Just "defMutual") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualId))))) :: (((S1 ('MetaSel ('Just "defCompiledRep") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CompiledRepresentation) :: S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe InstanceInfo))) :: (S1 ('MetaSel ('Just "defCopy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "defMatchable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :: S1 ('MetaSel ('Just "defNoCompilation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: ((S1 ('MetaSel ('Just "defInjective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "defCopatternLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "defBlocked") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Blocked_) :: (S1 ('MetaSel ('Just "defLanguage") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Language) :: S1 ('MetaSel ('Just "theDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Defn)))))))

data Builtin pf Source #

Constructors

Builtin Term
Prim pf
BuiltinRewriteRelations (Set QName)	`BUILTIN REWRITE`. We can have several rewrite relations.

Instances

Instances details

Foldable Builtin Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Builtin m -> m # foldMap :: Monoid m => (a -> m) -> Builtin a -> m # foldMap' :: Monoid m => (a -> m) -> Builtin a -> m # foldr :: (a -> b -> b) -> b -> Builtin a -> b # foldr' :: (a -> b -> b) -> b -> Builtin a -> b # foldl :: (b -> a -> b) -> b -> Builtin a -> b # foldl' :: (b -> a -> b) -> b -> Builtin a -> b # foldr1 :: (a -> a -> a) -> Builtin a -> a # foldl1 :: (a -> a -> a) -> Builtin a -> a # toList :: Builtin a -> [a] # null :: Builtin a -> Bool # length :: Builtin a -> Int # elem :: Eq a => a -> Builtin a -> Bool # maximum :: Ord a => Builtin a -> a # minimum :: Ord a => Builtin a -> a # sum :: Num a => Builtin a -> a # product :: Num a => Builtin a -> a #
Traversable Builtin Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b) # sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a) # mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b) # sequence :: Monad m => Builtin (m a) -> m (Builtin a) #
Functor Builtin Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Builtin a -> Builtin b # (<$) :: a -> Builtin b -> Builtin a #
NamesIn a => NamesIn (Builtin a) Source #