Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Options.Errors

Contents

- Printing error names
- Print error messages
- Orphan instances

Description

Provide names for the errors Agda throws.Options/Er

Synopsis

- data CannotQuoteTerm
  - = CannotQuoteTermHidden
  - | CannotQuoteTermNothing
- data DataRecOrFun_
  - = DataName_
  - | RecName_
  - | FunName_
- data ErasedDatatypeReason
  - = SeveralConstructors
  - | NoErasedMatches
  - | NoK
- data NotAllowedInDotPatterns
  - = LetExpressions
  - | PatternLambdas
- data NotAValidLetBinding
  - = MissingRHS
  - | NotAValidLetPattern
  - | WhereClausesNotAllowed
- data NotAValidLetExpression = MissingBody
- data ErrorName
  - = ExecError_ ExecError_
  - | GHCBackendError_ GHCBackendError_
  - | ImpossibleConstructor_ NegativeUnification_
  - | InteractionError_ InteractionError_
  - | JSBackendError_ JSBackendError_
  - | NicifierError_ DeclarationException_
  - | SplitError_ SplitError_
  - | UnquoteError_ UnquoteError_
  - | CompilationError_
  - | CustomBackendError_
  - | GenericError_
  - | GenericDocError_
  - | InternalError_
  - | LibraryError_
  - | NonFatalErrors_
  - | NotImplemented_
  - | NotSupported_
  - | OptionError_
  - | SyntaxError_
  - | AbsentRHSRequiresAbsurdPattern_
  - | AbstractConstructorNotInScope_
  - | AmbiguousConstructor_
  - | AmbiguousField_
  - | AmbiguousModule_
  - | AmbiguousName_
  - | AmbiguousOverloadedProjection_
  - | AmbiguousParseForApplication_
  - | AmbiguousParseForLHS_
  - | AmbiguousProjection_
  - | AmbiguousTopLevelModuleName_
  - | AsPatternInPatternSynonym_
  - | AttributeKindNotEnabled_
  - | BackendDoesNotSupportOnlyScopeChecking_
  - | BadArgumentsToPatternSynonym_
  - | BothWithAndRHS_
  - | BuiltinInParameterisedModule_
  - | BuiltinMustBeConstructor_
  - | BuiltinMustBeData_
  - | BuiltinMustBeDef_
  - | BuiltinMustBeFunction_
  - | BuiltinMustBePostulate_
  - | CannotApply_
  - | CannotEliminateWithPattern_
  - | CannotEliminateWithProjection_
  - | CannotGenerateHCompClause_
  - | CannotGenerateTransportClause_
  - | CannotQuote_ CannotQuote_
  - | CannotQuoteTerm_ CannotQuoteTerm
  - | CannotResolveAmbiguousPatternSynonym_
  - | CannotRewriteByNonEquation_
  - | CannotSolveSizeConstraints_
  - | CantResolveOverloadedConstructorsTargetingSameDatatype_
  - | ClashingDefinition_
  - | ClashingModule_
  - | ComatchingDisabledForRecord_
  - | ConstructorDoesNotTargetGivenType_
  - | ConstructorPatternInWrongDatatype_
  - | ContradictorySizeConstraint_
  - | CopatternHeadNotProjection_
  - | CubicalCompilationNotSupported_
  - | CubicalNotErasure_
  - | CubicalPrimitiveNotFullyApplied_
  - | CyclicModuleDependency_
  - | DatatypeIndexPolarity_
  - | DeBruijnIndexOutOfScope_
  - | DeclarationsAfterTopLevelModule_
  - | DefinitionInDifferentModule_
  - | DefinitionIsErased_
  - | DefinitionIsIrrelevant_
  - | DoNotationError_
  - | DoesNotMentionTicks_
  - | DotPatternInPatternSynonym_
  - | DuplicateBuiltinBinding_
  - | DuplicateConstructors_
  - | DuplicateFields_
  - | DuplicateImports_
  - | DuplicateOverlapPragma_
  - | DuplicatePrimitiveBinding_
  - | EmptyTypeOfSizes_
  - | ExpectedBindingForParameter_
  - | ExpectedIntervalLiteral_
  - | FieldOutsideRecord_
  - | FaceConstraintDisjunction_
  - | FaceConstraintUnsatisfiable_
  - | FileNotFound_
  - | ForcedConstructorNotInstantiated_
  - | FunctionTypeInSizeUniv_
  - | GeneralizeCyclicDependency_
  - | GeneralizeNotSupportedHere_
  - | GeneralizedVarInLetOpenedModule_
  - | ModuleNameHashCollision_
  - | HidingMismatch_
  - | IdiomBracketError_
  - | InvalidBuiltin_
  - | InvalidDottedExpression_
  - | IllTypedPatternAfterWithAbstraction_
  - | IllegalDeclarationBeforeTopLevelModule_
  - | IllegalDeclarationInDataDefinition_
  - | IllegalHidingInPostfixProjection_
  - | IllegalInstanceVariableInPatternSynonym_
  - | IllegalLetInTelescope_
  - | IllegalPatternInTelescope_
  - | IllformedProjectionPatternAbstract_
  - | IllformedProjectionPatternConcrete_
  - | IncorrectTypeForRewriteRelation_
  - | InstanceNoCandidate_
  - | InstanceSearchDepthExhausted_
  - | InvalidFileName_
  - | InvalidModalTelescopeUse_
  - | InvalidPattern_
  - | InvalidProjectionParameter_
  - | InvalidPun_ ConstructorOrPatternSynonym
  - | InvalidTypeSort_
  - | LambdaIsErased_
  - | LibTooFarDown_
  - | LiteralTooBig_
  - | MacroResultTypeMismatch_
  - | MetaCannotDependOn_
  - | MetaErasedSolution_
  - | MetaIrrelevantSolution_
  - | MismatchedProjectionsError_
  - | MissingTypeSignature_ DataRecOrFun_
  - | ModuleArityMismatch_
  - | ModuleDefinedInOtherFile_
  - | ModuleNameDoesntMatchFileName_
  - | ModuleNameUnexpected_
  - | MultipleFixityDecls_
  - | MultiplePolarityPragmas_
  - | ExplicitPolarityVsPragma_
  - | ConstructorNameOfNonRecord_
  - | NamedWhereModuleInRefinedContext_
  - | NeedOptionAllowExec_
  - | NeedOptionCopatterns_
  - | NeedOptionCubical_
  - | NeedOptionPatternMatching_
  - | NeedOptionProp_
  - | NeedOptionRewriting_
  - | NeedOptionSizedTypes_
  - | NeedOptionTwoLevel_
  - | NeedOptionUniversePolymorphism_
  - | NegativeLiteralInPattern_
  - | NoBindingForBuiltin_
  - | NoBindingForPrimitive_
  - | NoKnownRecordWithSuchFields_
  - | NoParameterOfName_
  - | NoParseForApplication_
  - | NoParseForLHS_
  - | NoSuchBuiltinName_
  - | NoSuchModule_
  - | NoSuchPrimitiveFunction_
  - | NotAValidLetBinding_ (Maybe NotAValidLetBinding)
  - | NotAValidLetExpression_ NotAValidLetExpression
  - | NotAllowedInDotPatterns_ NotAllowedInDotPatterns
  - | NotAnExpression_
  - | NotInScope_
  - | NotLeqSort_
  - | NotValidBeforeField_
  - | OverlappingProjects_
  - | PathAbstractionFailed_
  - | PatternInPathLambda_
  - | PatternInSystem_
  - | PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym
  - | PostulatedSizeInModule_
  - | PrivateRecordField_
  - | ProjectionIsIrrelevant_
  - | QualifiedLocalModule_
  - | QuantityMismatch_
  - | RecordIsErased_
  - | RecursiveRecordNeedsInductivity_
  - | ReferencesFutureVariables_
  - | RelevanceMismatch_
  - | RepeatedNamesInImportDirective_
  - | RepeatedVariablesInPattern_
  - | ShadowedModule_
  - | ShouldBeASort_
  - | ShouldBeEmpty_
  - | ShouldBePath_
  - | ShouldBePi_
  - | ShouldBeRecordPattern_
  - | ShouldBeRecordType_
  - | ShouldEndInApplicationOfTheDatatype_
  - | SolvedButOpenHoles_
  - | SortCannotDependOnItsIndex_
  - | SortDoesNotAdmitDataDefinitions_
  - | SortOfSplitVarError_
  - | SplitInProp_
  - | SplitOnAbstract_
  - | SplitOnCoinductive_
  - | SplitOnIrrelevant_
  - | SplitOnNonEtaRecord_
  - | SplitOnNonVariable_
  - | SplitOnPartial_
  - | SplitOnUnchecked_
  - | SplitOnUnusableCohesion_
  - | SplitOnUnusablePolarity_
  - | TacticAttributeNotAllowed_
  - | TooFewArgumentsToPatternSynonym_
  - | TooFewPatternsInWithClause_
  - | TooManyFields_
  - | TooManyPatternsInWithClause_
  - | TriedToCopyConstrainedPrim_
  - | InvalidInstanceHeadType_
  - | UnboundVariablesInPatternSynonym_
  - | UnequalCohesion_
  - | UnequalFiniteness_
  - | UnequalHiding_
  - | UnequalLevel_
  - | UnequalQuantity_
  - | UnequalRelevance_
  - | UnequalPolarity_
  - | UnequalSorts_
  - | UnequalTerms_
  - | UnexpectedModalityAnnotationInParameter_
  - | UnexpectedParameter_
  - | UnexpectedTypeSignatureForParameter_
  - | UnexpectedWithPatterns_
  - | UnknownBackend_
  - | UnusableAtModality_
  - | UnusedVariableInPatternSynonym_
  - | VariableIsErased_
  - | VariableIsIrrelevant_
  - | VariableIsOfUnusableCohesion_
  - | VariableIsOfUnusablePolarity_
  - | WithClausePatternMismatch_
  - | WithOnFreeVariable_
  - | WrongAnnotationInLambda_
  - | WrongArgInfoForPrimitive_
  - | WrongCohesionInLambda_
  - | WrongPolarityInLambda_
  - | WrongHidingInApplication_
  - | WrongHidingInLHS_
  - | WrongHidingInLambda_
  - | WrongHidingInProjection_
  - | WrongIrrelevanceInLambda_
  - | WrongNamedArgument_
  - | WrongNumberOfConstructorArguments_
  - | WrongQuantityInLambda_
  - | WrongSharpArity_
- data DeclarationException_
  - = AmbiguousConstructorN_
  - | AmbiguousFunClauses_
  - | BadMacroDef_
  - | DisallowedInterleavedMutual_
  - | DuplicateAnonDeclaration_
  - | DuplicateDefinition_
  - | InvalidMeasureMutual_
  - | MissingWithClauses_
  - | MultipleEllipses_
  - | OpaqueInMutual_
  - | UnfoldingOutsideOpaque_
  - | UnquoteDefRequiresSignature_
  - | WrongContentBlock_
  - | WrongDefinition_
- data GHCBackendError_
  - = ConstructorCountMismatch_
  - | NotAHaskellType_ NotAHaskellType_
  - | WrongTypeOfMain_
- data JSBackendError_ = BadCompilePragma_
- data InteractionError_
  - = CannotGive_
  - | CannotRefine_
  - | CaseSplitError_
  - | ExpectedIdentifier_
  - | ExpectedApplication_
  - | NoActionForInteractionPoint_
  - | NoSuchInteractionPoint_
  - | UnexpectedWhere_
- data NegativeUnification_
  - = UnifyConflict_
  - | UnifyCycle_
- data NotAHaskellType_
  - = BadDontCare_
  - | BadLambda_
  - | BadMeta_
  - | NoPragmaFor_
  - | NotCompiled_
  - | WrongPragmaFor_
- data SplitError_
  - = ErasedDatatype_ ErasedDatatypeReason
  - | GenericSplitError_
  - | BlockedType_
  - | CannotCreateMissingClause_
  - | CoinductiveDatatype_
  - | CosplitCatchall_
  - | CosplitNoRecordType_
  - | CosplitNoTarget_
  - | NotADatatype_
  - | UnificationStuck_
- data CannotQuote_
  - = CannotQuoteAmbiguous_
  - | CannotQuoteExpression_
  - | CannotQuoteHidden_
  - | CannotQuoteNothing_
  - | CannotQuotePattern_
- data ExecError_
  - = ExeNotTrusted_
  - | ExeNotFound_
  - | ExeNotExecutable_
- data UnquoteError_
  - = BlockedOnMeta_
  - | CannotDeclareHiddenFunction_
  - | CommitAfterDef_
  - | ConInsteadOfDef_
  - | DefineDataNotData_
  - | DefInsteadOfCon_
  - | MissingDeclaration_
  - | MissingDefinition_
  - | NakedUnquote_
  - | NonCanonical_
  - | PatLamWithoutClauses_
  - | StaleMeta_
  - | TooManyParameters_
  - | UnboundName_
- defaultErrorNameString :: Show a => a -> String
- erasedDatatypeReasonString :: ErasedDatatypeReason -> String
- errorNameString :: ErrorName -> String
- constructorOrPatternSynonymNameString :: ConstructorOrPatternSynonym -> String
- dataRecOrFunString :: DataRecOrFun_ -> String
- declarationExceptionNameString :: DeclarationException_ -> String
- ghcBackendErrorNameString :: GHCBackendError_ -> String
- jsBackendErrorNameString :: JSBackendError_ -> String
- interactionErrorNameString :: InteractionError_ -> String
- negativeUnificationErrorNameString :: NegativeUnification_ -> String
- notAHaskellTypeErrorNameString :: NotAHaskellType_ -> String
- notAValidLetBindingString :: NotAValidLetBinding -> String
- notAValidLetExpressionString :: NotAValidLetExpression -> String
- notAllowedInDotPatternsString :: NotAllowedInDotPatterns -> String
- splitErrorNameString :: SplitError_ -> String
- cannotQuoteNameString :: CannotQuote_ -> String
- cannotQuoteTermNameString :: CannotQuoteTerm -> String
- execErrorNameString :: ExecError_ -> String
- unquoteErrorNameString :: UnquoteError_ -> String
- helpErrors :: String
- verbalizeNotAValidLetBinding :: NotAValidLetBinding -> String
- verbalizeNotAValidLetExpression :: NotAValidLetExpression -> String

# Documentation

data CannotQuoteTerm Source #

Extra information for error `CannotQuoteTerm`.

Constructors

CannotQuoteTermHidden |
CannotQuoteTermNothing |

#### Instances

Instances details

NFData CannotQuoteTerm Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods rnf :: CannotQuoteTerm -> () Source #
Bounded CannotQuoteTerm Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: CannotQuoteTerm Source # maxBound :: CannotQuoteTerm Source #
Enum CannotQuoteTerm Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: CannotQuoteTerm -> CannotQuoteTerm Source #

pred :: CannotQuoteTerm -> CannotQuoteTerm Source #

toEnum :: Int -> CannotQuoteTerm Source #

fromEnum :: CannotQuoteTerm -> Int Source #

enumFrom :: CannotQuoteTerm -> [CannotQuoteTerm] Source #

enumFromThen :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm] Source #

enumFromTo :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm] Source #

enumFromThenTo :: CannotQuoteTerm -> CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm] Source #

Generic CannotQuoteTerm Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep CannotQuoteTerm |
Instance details Defined in Agda.Interaction.Options.Errors type Rep CannotQuoteTerm = D1 ('MetaData "CannotQuoteTerm" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "CannotQuoteTermHidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuoteTermNothing" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: CannotQuoteTerm -> Rep CannotQuoteTerm x Source #

to :: Rep CannotQuoteTerm x -> CannotQuoteTerm Source #

Show CannotQuoteTerm Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> CannotQuoteTerm -> ShowS Source # show :: CannotQuoteTerm -> String Source # showList :: [CannotQuoteTerm] -> ShowS Source #
type Rep CannotQuoteTerm Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep CannotQuoteTerm = D1 ('MetaData "CannotQuoteTerm" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "CannotQuoteTermHidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuoteTermNothing" 'PrefixI 'False) (U1 :: Type -> Type))

data DataRecOrFun_ Source #

What kind of declaration?

See also `DataRecOrFun`.

Constructors

DataName_ | Name of a data type.
RecName_ | Name of a record type.
FunName_ | Name of a function.

#### Instances

Instances details

Bounded DataRecOrFun_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: DataRecOrFun_ Source # maxBound :: DataRecOrFun_ Source #
Enum DataRecOrFun_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: DataRecOrFun_ -> DataRecOrFun_ Source #

pred :: DataRecOrFun_ -> DataRecOrFun_ Source #

toEnum :: Int -> DataRecOrFun_ Source #

fromEnum :: DataRecOrFun_ -> Int Source #

enumFrom :: DataRecOrFun_ -> [DataRecOrFun_] Source #

enumFromThen :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] Source #

enumFromTo :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] Source #

enumFromThenTo :: DataRecOrFun_ -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] Source #

Generic DataRecOrFun_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep DataRecOrFun_ |
Instance details Defined in Agda.Interaction.Options.Errors type Rep DataRecOrFun_ = D1 ('MetaData "DataRecOrFun_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DataName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RecName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunName_" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: DataRecOrFun_ -> Rep DataRecOrFun_ x Source #

to :: Rep DataRecOrFun_ x -> DataRecOrFun_ Source #

Show DataRecOrFun_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> DataRecOrFun_ -> ShowS Source # show :: DataRecOrFun_ -> String Source # showList :: [DataRecOrFun_] -> ShowS Source #
type Rep DataRecOrFun_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep DataRecOrFun_ = D1 ('MetaData "DataRecOrFun_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DataName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RecName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunName_" 'PrefixI 'False) (U1 :: Type -> Type)))

data ErasedDatatypeReason Source #

The reason for an `ErasedDatatype` error.

Constructors

SeveralConstructors | There are several constructors.
NoErasedMatches | The flag `--erased-matches` is not used.
NoK | The K rule is not activated.

#### Instances

Instances details

NFData ErasedDatatypeReason Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods rnf :: ErasedDatatypeReason -> () Source #
Bounded ErasedDatatypeReason Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: ErasedDatatypeReason Source # maxBound :: ErasedDatatypeReason Source #
Enum ErasedDatatypeReason Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: ErasedDatatypeReason -> ErasedDatatypeReason Source #

pred :: ErasedDatatypeReason -> ErasedDatatypeReason Source #

toEnum :: Int -> ErasedDatatypeReason Source #

fromEnum :: ErasedDatatypeReason -> Int Source #

enumFrom :: ErasedDatatypeReason -> [ErasedDatatypeReason] Source #

enumFromThen :: ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] Source #

enumFromTo :: ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] Source #

enumFromThenTo :: ErasedDatatypeReason -> ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] Source #

Generic ErasedDatatypeReason Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep ErasedDatatypeReason |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ErasedDatatypeReason = D1 ('MetaData "ErasedDatatypeReason" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SeveralConstructors" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoErasedMatches" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoK" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: ErasedDatatypeReason -> Rep ErasedDatatypeReason x Source #

to :: Rep ErasedDatatypeReason x -> ErasedDatatypeReason Source #

Show ErasedDatatypeReason Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> ErasedDatatypeReason -> ShowS Source # show :: ErasedDatatypeReason -> String Source # showList :: [ErasedDatatypeReason] -> ShowS Source #
type Rep ErasedDatatypeReason Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ErasedDatatypeReason = D1 ('MetaData "ErasedDatatypeReason" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SeveralConstructors" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoErasedMatches" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoK" 'PrefixI 'False) (U1 :: Type -> Type)))

data NotAllowedInDotPatterns Source #

Things not allowed in dot patterns.

Constructors

LetExpressions |
PatternLambdas |

#### Instances

Instances details

NFData NotAllowedInDotPatterns Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAllowedInDotPatterns -> () Source #
Bounded NotAllowedInDotPatterns Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: NotAllowedInDotPatterns Source # maxBound :: NotAllowedInDotPatterns Source #
Enum NotAllowedInDotPatterns Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns Source #

pred :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns Source #

toEnum :: Int -> NotAllowedInDotPatterns Source #

fromEnum :: NotAllowedInDotPatterns -> Int Source #

enumFrom :: NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] Source #

enumFromThen :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] Source #

enumFromTo :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] Source #

enumFromThenTo :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] Source #

Generic NotAllowedInDotPatterns Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep NotAllowedInDotPatterns |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NotAllowedInDotPatterns = D1 ('MetaData "NotAllowedInDotPatterns" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LetExpressions" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternLambdas" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x Source #

to :: Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns Source #

Show NotAllowedInDotPatterns Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAllowedInDotPatterns -> ShowS Source # show :: NotAllowedInDotPatterns -> String Source # showList :: [NotAllowedInDotPatterns] -> ShowS Source #
type Rep NotAllowedInDotPatterns Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NotAllowedInDotPatterns = D1 ('MetaData "NotAllowedInDotPatterns" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LetExpressions" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternLambdas" 'PrefixI 'False) (U1 :: Type -> Type))

data NotAValidLetBinding Source #

Reasons for error `NotAValidLetBinding`.

Constructors

MissingRHS |
NotAValidLetPattern |
WhereClausesNotAllowed |

#### Instances

Instances details

NFData NotAValidLetBinding Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAValidLetBinding -> () Source #
Bounded NotAValidLetBinding Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: NotAValidLetBinding Source # maxBound :: NotAValidLetBinding Source #
Enum NotAValidLetBinding Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: NotAValidLetBinding -> NotAValidLetBinding Source #

pred :: NotAValidLetBinding -> NotAValidLetBinding Source #

toEnum :: Int -> NotAValidLetBinding Source #

fromEnum :: NotAValidLetBinding -> Int Source #

enumFrom :: NotAValidLetBinding -> [NotAValidLetBinding] Source #

enumFromThen :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] Source #

enumFromTo :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] Source #

enumFromThenTo :: NotAValidLetBinding -> NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] Source #

Generic NotAValidLetBinding Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep NotAValidLetBinding |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep NotAValidLetBinding = D1 ('MetaData "NotAValidLetBinding" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MissingRHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAValidLetPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WhereClausesNotAllowed" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: NotAValidLetBinding -> Rep NotAValidLetBinding x Source #

to :: Rep NotAValidLetBinding x -> NotAValidLetBinding Source #

Show NotAValidLetBinding Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAValidLetBinding -> ShowS Source # show :: NotAValidLetBinding -> String Source # showList :: [NotAValidLetBinding] -> ShowS Source #
type Rep NotAValidLetBinding Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep NotAValidLetBinding = D1 ('MetaData "NotAValidLetBinding" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MissingRHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAValidLetPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WhereClausesNotAllowed" 'PrefixI 'False) (U1 :: Type -> Type)))

data NotAValidLetExpression Source #

Reasons for error `NotAValidLetExpression`.

Constructors

MissingBody |

#### Instances

Instances details

NFData NotAValidLetExpression Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAValidLetExpression -> () Source #
Bounded NotAValidLetExpression Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: NotAValidLetExpression Source # maxBound :: NotAValidLetExpression Source #
Enum NotAValidLetExpression Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: NotAValidLetExpression -> NotAValidLetExpression Source #

pred :: NotAValidLetExpression -> NotAValidLetExpression Source #

toEnum :: Int -> NotAValidLetExpression Source #

fromEnum :: NotAValidLetExpression -> Int Source #

enumFrom :: NotAValidLetExpression -> [NotAValidLetExpression] Source #

enumFromThen :: NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] Source #

enumFromTo :: NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] Source #

enumFromThenTo :: NotAValidLetExpression -> NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] Source #

Generic NotAValidLetExpression Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep NotAValidLetExpression |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NotAValidLetExpression = D1 ('MetaData "NotAValidLetExpression" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MissingBody" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: NotAValidLetExpression -> Rep NotAValidLetExpression x Source #

to :: Rep NotAValidLetExpression x -> NotAValidLetExpression Source #

Show NotAValidLetExpression Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAValidLetExpression -> ShowS Source # show :: NotAValidLetExpression -> String Source # showList :: [NotAValidLetExpression] -> ShowS Source #
type Rep NotAValidLetExpression Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NotAValidLetExpression = D1 ('MetaData "NotAValidLetExpression" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MissingBody" 'PrefixI 'False) (U1 :: Type -> Type))

data ErrorName Source #

Symbolic name of an Agda error.

Constructors

ExecError_ ExecError_ |
GHCBackendError_ GHCBackendError_ |
ImpossibleConstructor_ NegativeUnification_ |
InteractionError_ InteractionError_ |
JSBackendError_ JSBackendError_ |
NicifierError_ DeclarationException_ |
SplitError_ SplitError_ |
UnquoteError_ UnquoteError_ |
CompilationError_ |
CustomBackendError_ |
GenericError_ |
GenericDocError_ |
InternalError_ |
LibraryError_ |
NonFatalErrors_ |
NotImplemented_ |
NotSupported_ |
OptionError_ |
SyntaxError_ |
AbsentRHSRequiresAbsurdPattern_ |
AbstractConstructorNotInScope_ |
AmbiguousConstructor_ |
AmbiguousField_ |
AmbiguousModule_ |
AmbiguousName_ |
AmbiguousOverloadedProjection_ |
AmbiguousParseForApplication_ |
AmbiguousParseForLHS_ |
AmbiguousProjection_ |
AmbiguousTopLevelModuleName_ |
AsPatternInPatternSynonym_ |
AttributeKindNotEnabled_ |
BackendDoesNotSupportOnlyScopeChecking_ |
BadArgumentsToPatternSynonym_ |
BothWithAndRHS_ |
BuiltinInParameterisedModule_ |
BuiltinMustBeConstructor_ |
BuiltinMustBeData_ |
BuiltinMustBeDef_ |
BuiltinMustBeFunction_ |
BuiltinMustBePostulate_ |
CannotApply_ |
CannotEliminateWithPattern_ |
CannotEliminateWithProjection_ |
CannotGenerateHCompClause_ |
CannotGenerateTransportClause_ |
CannotQuote_ CannotQuote_ |
CannotQuoteTerm_ CannotQuoteTerm |
CannotResolveAmbiguousPatternSynonym_ |
CannotRewriteByNonEquation_ |
CannotSolveSizeConstraints_ |
CantResolveOverloadedConstructorsTargetingSameDatatype_ |
ClashingDefinition_ |
ClashingModule_ |
ComatchingDisabledForRecord_ |
ConstructorDoesNotTargetGivenType_ |
ConstructorPatternInWrongDatatype_ |
ContradictorySizeConstraint_ |
CopatternHeadNotProjection_ |
CubicalCompilationNotSupported_ |
CubicalNotErasure_ |
CubicalPrimitiveNotFullyApplied_ |
CyclicModuleDependency_ |
DatatypeIndexPolarity_ |
DeBruijnIndexOutOfScope_ |
DeclarationsAfterTopLevelModule_ |
DefinitionInDifferentModule_ |
DefinitionIsErased_ |
DefinitionIsIrrelevant_ |
DoNotationError_ |
DoesNotMentionTicks_ |
DotPatternInPatternSynonym_ |
DuplicateBuiltinBinding_ |
DuplicateConstructors_ |
DuplicateFields_ |
DuplicateImports_ |
DuplicateOverlapPragma_ |
DuplicatePrimitiveBinding_ |
EmptyTypeOfSizes_ |
ExpectedBindingForParameter_ |
ExpectedIntervalLiteral_ |
FieldOutsideRecord_ |
FaceConstraintDisjunction_ |
FaceConstraintUnsatisfiable_ |
FileNotFound_ |
ForcedConstructorNotInstantiated_ |
FunctionTypeInSizeUniv_ |
GeneralizeCyclicDependency_ |
GeneralizeNotSupportedHere_ |
GeneralizedVarInLetOpenedModule_ |
ModuleNameHashCollision_ |
HidingMismatch_ |
IdiomBracketError_ |
InvalidBuiltin_ |
InvalidDottedExpression_ |
IllTypedPatternAfterWithAbstraction_ |
IllegalDeclarationBeforeTopLevelModule_ |
IllegalDeclarationInDataDefinition_ |
IllegalHidingInPostfixProjection_ |
IllegalInstanceVariableInPatternSynonym_ |
IllegalLetInTelescope_ |
IllegalPatternInTelescope_ |
IllformedProjectionPatternAbstract_ |
IllformedProjectionPatternConcrete_ |
IncorrectTypeForRewriteRelation_ |
InstanceNoCandidate_ |
InstanceSearchDepthExhausted_ |
InvalidFileName_ |
InvalidModalTelescopeUse_ |
InvalidPattern_ |
InvalidProjectionParameter_ |
InvalidPun_ ConstructorOrPatternSynonym |
InvalidTypeSort_ |
LambdaIsErased_ |
LibTooFarDown_ |
LiteralTooBig_ |
MacroResultTypeMismatch_ |
MetaCannotDependOn_ |
MetaErasedSolution_ |
MetaIrrelevantSolution_ |
MismatchedProjectionsError_ |
MissingTypeSignature_ DataRecOrFun_ |
ModuleArityMismatch_ |
ModuleDefinedInOtherFile_ |
ModuleNameDoesntMatchFileName_ |
ModuleNameUnexpected_ |
MultipleFixityDecls_ |
MultiplePolarityPragmas_ |
ExplicitPolarityVsPragma_ |
ConstructorNameOfNonRecord_ |
NamedWhereModuleInRefinedContext_ |
NeedOptionAllowExec_ |
NeedOptionCopatterns_ |
NeedOptionCubical_ |
NeedOptionPatternMatching_ |
NeedOptionProp_ |
NeedOptionRewriting_ |
NeedOptionSizedTypes_ |
NeedOptionTwoLevel_ |
NeedOptionUniversePolymorphism_ |
NegativeLiteralInPattern_ |
NoBindingForBuiltin_ |
NoBindingForPrimitive_ |
NoKnownRecordWithSuchFields_ |
NoParameterOfName_ |
NoParseForApplication_ |
NoParseForLHS_ |
NoSuchBuiltinName_ |
NoSuchModule_ |
NoSuchPrimitiveFunction_ |
NotAValidLetBinding_ (Maybe NotAValidLetBinding) |
NotAValidLetExpression_ NotAValidLetExpression |
NotAllowedInDotPatterns_ NotAllowedInDotPatterns |
NotAnExpression_ |
NotInScope_ |
NotLeqSort_ |
NotValidBeforeField_ |
OverlappingProjects_ |
PathAbstractionFailed_ |
PatternInPathLambda_ |
PatternInSystem_ |
PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym |
PostulatedSizeInModule_ |
PrivateRecordField_ |
ProjectionIsIrrelevant_ |
QualifiedLocalModule_ |
QuantityMismatch_ |
RecordIsErased_ |
RecursiveRecordNeedsInductivity_ |
ReferencesFutureVariables_ |
RelevanceMismatch_ |
RepeatedNamesInImportDirective_ |
RepeatedVariablesInPattern_ |
ShadowedModule_ |
ShouldBeASort_ |
ShouldBeEmpty_ |
ShouldBePath_ |
ShouldBePi_ |
ShouldBeRecordPattern_ |
ShouldBeRecordType_ |
ShouldEndInApplicationOfTheDatatype_ |
SolvedButOpenHoles_ |
SortCannotDependOnItsIndex_ |
SortDoesNotAdmitDataDefinitions_ |
SortOfSplitVarError_ |
SplitInProp_ |
SplitOnAbstract_ |
SplitOnCoinductive_ |
SplitOnIrrelevant_ |
SplitOnNonEtaRecord_ |
SplitOnNonVariable_ |
SplitOnPartial_ |
SplitOnUnchecked_ |
SplitOnUnusableCohesion_ |
SplitOnUnusablePolarity_ |
TacticAttributeNotAllowed_ |
TooFewArgumentsToPatternSynonym_ |
TooFewPatternsInWithClause_ |
TooManyFields_ |
TooManyPatternsInWithClause_ |
TriedToCopyConstrainedPrim_ |
InvalidInstanceHeadType_ |
UnboundVariablesInPatternSynonym_ |
UnequalCohesion_ |
UnequalFiniteness_ |
UnequalHiding_ |
UnequalLevel_ |
UnequalQuantity_ |
UnequalRelevance_ |
UnequalPolarity_ |
UnequalSorts_ |
UnequalTerms_ |
UnexpectedModalityAnnotationInParameter_ |
UnexpectedParameter_ |
UnexpectedTypeSignatureForParameter_ |
UnexpectedWithPatterns_ |
UnknownBackend_ |
UnusableAtModality_ |
UnusedVariableInPatternSynonym_ |
VariableIsErased_ |
VariableIsIrrelevant_ |
VariableIsOfUnusableCohesion_ |
VariableIsOfUnusablePolarity_ |
WithClausePatternMismatch_ |
WithOnFreeVariable_ |
WrongAnnotationInLambda_ |
WrongArgInfoForPrimitive_ |
WrongCohesionInLambda_ |
WrongPolarityInLambda_ |
WrongHidingInApplication_ |
WrongHidingInLHS_ |
WrongHidingInLambda_ |
WrongHidingInProjection_ |
WrongIrrelevanceInLambda_ |
WrongNamedArgument_ |
WrongNumberOfConstructorArguments_ |
WrongQuantityInLambda_ |
WrongSharpArity_ |

#### Instances

Instances details

Bounded ErrorName Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: ErrorName Source # maxBound :: ErrorName Source #
Enum ErrorName Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: ErrorName -> ErrorName Source #

pred :: ErrorName -> ErrorName Source #

toEnum :: Int -> ErrorName Source #

fromEnum :: ErrorName -> Int Source #

enumFrom :: ErrorName -> [ErrorName] Source #

enumFromThen :: ErrorName -> ErrorName -> [ErrorName] Source #

enumFromTo :: ErrorName -> ErrorName -> [ErrorName] Source #

enumFromThenTo :: ErrorName -> ErrorName -> ErrorName -> [ErrorName] Source #

Generic ErrorName Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep ErrorName |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ErrorName = D1 ('MetaData "ErrorName" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((((((C1 ('MetaCons "ExecError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExecError_)) :+: (C1 ('MetaCons "GHCBackendError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GHCBackendError_)) :+: C1 ('MetaCons "ImpossibleConstructor_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NegativeUnification_)))) :+: ((C1 ('MetaCons "InteractionError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionError_)) :+: C1 ('MetaCons "JSBackendError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 JSBackendError_))) :+: (C1 ('MetaCons "NicifierError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationException_)) :+: C1 ('MetaCons "SplitError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitError_))))) :+: ((C1 ('MetaCons "UnquoteError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnquoteError_)) :+: (C1 ('MetaCons "CompilationError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendError_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "GenericError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GenericDocError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InternalError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibraryError_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NonFatalErrors_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotImplemented_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotSupported_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "OptionError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyntaxError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AbsentRHSRequiresAbsurdPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbstractConstructorNotInScope_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "AmbiguousConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AmbiguousModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousName_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "AmbiguousOverloadedProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousParseForApplication_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AmbiguousParseForLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousProjection_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "AmbiguousTopLevelModuleName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AsPatternInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AttributeKindNotEnabled_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BackendDoesNotSupportOnlyScopeChecking_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadArgumentsToPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BothWithAndRHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinInParameterisedModule_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "BuiltinMustBeConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinMustBeData_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinMustBeDef_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinMustBeFunction_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinMustBePostulate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotApply_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotEliminateWithPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotEliminateWithProjection_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "CannotGenerateHCompClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotGenerateTransportClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuote_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuote_)))) :+: ((C1 ('MetaCons "CannotQuoteTerm_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuoteTerm)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotRewriteByNonEquation_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotSolveSizeConstraints_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "CantResolveOverloadedConstructorsTargetingSameDatatype_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ClashingDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ClashingModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ComatchingDisabledForRecord_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConstructorDoesNotTargetGivenType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConstructorPatternInWrongDatatype_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ContradictorySizeConstraint_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CopatternHeadNotProjection_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "CubicalCompilationNotSupported_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CubicalNotErasure_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CubicalPrimitiveNotFullyApplied_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CyclicModuleDependency_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DatatypeIndexPolarity_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DeBruijnIndexOutOfScope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DeclarationsAfterTopLevelModule_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "DefinitionInDifferentModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DefinitionIsErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DefinitionIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DoNotationError_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DoesNotMentionTicks_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateBuiltinBinding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateConstructors_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DuplicateImports_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateOverlapPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DuplicatePrimitiveBinding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyTypeOfSizes_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ExpectedBindingForParameter_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpectedIntervalLiteral_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FieldOutsideRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FaceConstraintDisjunction_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintUnsatisfiable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FileNotFound_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ForcedConstructorNotInstantiated_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunctionTypeInSizeUniv_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "GeneralizeCyclicDependency_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeNotSupportedHere_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "GeneralizedVarInLetOpenedModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ModuleNameHashCollision_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HidingMismatch_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "IdiomBracketError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidDottedExpression_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllTypedPatternAfterWithAbstraction_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "IllegalDeclarationBeforeTopLevelModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalDeclarationInDataDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllegalHidingInPostfixProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "IllegalLetInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalPatternInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllformedProjectionPatternAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllformedProjectionPatternConcrete_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "IncorrectTypeForRewriteRelation_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InstanceNoCandidate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceSearchDepthExhausted_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidFileName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidModalTelescopeUse_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidProjectionParameter_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InvalidPun_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "InvalidTypeSort_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LambdaIsErased_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibTooFarDown_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "LiteralTooBig_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroResultTypeMismatch_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MetaCannotDependOn_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MetaErasedSolution_" 'PrefixI 'False) (U1 :: Type -> Type)))))))) :+: ((((((C1 ('MetaCons "MetaIrrelevantSolution_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MismatchedProjectionsError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingTypeSignature_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun_)))) :+: ((C1 ('MetaCons "ModuleArityMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleDefinedInOtherFile_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ModuleNameDoesntMatchFileName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNameUnexpected_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MultipleFixityDecls_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MultiplePolarityPragmas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExplicitPolarityVsPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConstructorNameOfNonRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NamedWhereModuleInRefinedContext_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NeedOptionAllowExec_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionCopatterns_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NeedOptionCubical_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeedOptionPatternMatching_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionProp_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NeedOptionRewriting_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionSizedTypes_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NeedOptionTwoLevel_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionUniversePolymorphism_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NegativeLiteralInPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoBindingForBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoBindingForPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoKnownRecordWithSuchFields_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NoParameterOfName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoParseForApplication_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoParseForLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoSuchBuiltinName_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "NoSuchModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoSuchPrimitiveFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotAValidLetBinding_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NotAValidLetBinding))))) :+: ((C1 ('MetaCons "NotAValidLetExpression_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAValidLetExpression)) :+: C1 ('MetaCons "NotAllowedInDotPatterns_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAllowedInDotPatterns))) :+: (C1 ('MetaCons "NotAnExpression_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotInScope_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NotLeqSort_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotValidBeforeField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OverlappingProjects_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PathAbstractionFailed_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternInPathLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternInSystem_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatternSynonymArgumentShadows_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "PostulatedSizeInModule_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrivateRecordField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjectionIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QualifiedLocalModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "QuantityMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecordIsErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RecursiveRecordNeedsInductivity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReferencesFutureVariables_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "RelevanceMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RepeatedNamesInImportDirective_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RepeatedVariablesInPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowedModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ShouldBeASort_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldBeEmpty_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ShouldBePath_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldBePi_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "ShouldBeRecordPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ShouldBeRecordType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldEndInApplicationOfTheDatatype_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SolvedButOpenHoles_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SortCannotDependOnItsIndex_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SortDoesNotAdmitDataDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SortOfSplitVarError_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "SplitInProp_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SplitOnCoinductive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SplitOnNonEtaRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnNonVariable_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SplitOnPartial_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnUnchecked_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "SplitOnUnusableCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SplitOnUnusablePolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TacticAttributeNotAllowed_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TooFewArgumentsToPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooFewPatternsInWithClause_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooManyPatternsInWithClause_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TriedToCopyConstrainedPrim_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidInstanceHeadType_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnboundVariablesInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalCohesion_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnequalFiniteness_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalHiding_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnequalLevel_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalQuantity_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "UnequalRelevance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnequalPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalSorts_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnequalTerms_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedModalityAnnotationInParameter_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnexpectedParameter_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedTypeSignatureForParameter_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "UnexpectedWithPatterns_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownBackend_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnusableAtModality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnusedVariableInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VariableIsErased_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VariableIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VariableIsOfUnusableCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VariableIsOfUnusablePolarity_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "WithClausePatternMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithOnFreeVariable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongAnnotationInLambda_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongArgInfoForPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongCohesionInLambda_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongPolarityInLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongHidingInApplication_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "WrongHidingInLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongHidingInLambda_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongHidingInProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongIrrelevanceInLambda_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongNamedArgument_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongNumberOfConstructorArguments_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongQuantityInLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongSharpArity_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

Methods

from :: ErrorName -> Rep ErrorName x Source #

to :: Rep ErrorName x -> ErrorName Source #

Show ErrorName Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> ErrorName -> ShowS Source # show :: ErrorName -> String Source # showList :: [ErrorName] -> ShowS Source #
type Rep ErrorName Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ErrorName = D1 ('MetaData "ErrorName" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((((((C1 ('MetaCons "ExecError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExecError_)) :+: (C1 ('MetaCons "GHCBackendError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GHCBackendError_)) :+: C1 ('MetaCons "ImpossibleConstructor_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NegativeUnification_)))) :+: ((C1 ('MetaCons "InteractionError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionError_)) :+: C1 ('MetaCons "JSBackendError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 JSBackendError_))) :+: (C1 ('MetaCons "NicifierError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationException_)) :+: C1 ('MetaCons "SplitError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitError_))))) :+: ((C1 ('MetaCons "UnquoteError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnquoteError_)) :+: (C1 ('MetaCons "CompilationError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendError_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "GenericError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GenericDocError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InternalError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibraryError_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NonFatalErrors_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotImplemented_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotSupported_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "OptionError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyntaxError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AbsentRHSRequiresAbsurdPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbstractConstructorNotInScope_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "AmbiguousConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AmbiguousModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousName_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "AmbiguousOverloadedProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousParseForApplication_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AmbiguousParseForLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AmbiguousProjection_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "AmbiguousTopLevelModuleName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AsPatternInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AttributeKindNotEnabled_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BackendDoesNotSupportOnlyScopeChecking_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadArgumentsToPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BothWithAndRHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinInParameterisedModule_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "BuiltinMustBeConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinMustBeData_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinMustBeDef_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinMustBeFunction_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinMustBePostulate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotApply_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotEliminateWithPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotEliminateWithProjection_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "CannotGenerateHCompClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotGenerateTransportClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuote_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuote_)))) :+: ((C1 ('MetaCons "CannotQuoteTerm_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuoteTerm)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotRewriteByNonEquation_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotSolveSizeConstraints_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "CantResolveOverloadedConstructorsTargetingSameDatatype_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ClashingDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ClashingModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ComatchingDisabledForRecord_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConstructorDoesNotTargetGivenType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConstructorPatternInWrongDatatype_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ContradictorySizeConstraint_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CopatternHeadNotProjection_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "CubicalCompilationNotSupported_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CubicalNotErasure_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CubicalPrimitiveNotFullyApplied_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CyclicModuleDependency_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DatatypeIndexPolarity_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DeBruijnIndexOutOfScope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DeclarationsAfterTopLevelModule_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "DefinitionInDifferentModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DefinitionIsErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DefinitionIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DoNotationError_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DoesNotMentionTicks_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateBuiltinBinding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateConstructors_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DuplicateImports_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateOverlapPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DuplicatePrimitiveBinding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyTypeOfSizes_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ExpectedBindingForParameter_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpectedIntervalLiteral_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FieldOutsideRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FaceConstraintDisjunction_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintUnsatisfiable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FileNotFound_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ForcedConstructorNotInstantiated_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunctionTypeInSizeUniv_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "GeneralizeCyclicDependency_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeNotSupportedHere_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "GeneralizedVarInLetOpenedModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ModuleNameHashCollision_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HidingMismatch_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "IdiomBracketError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidDottedExpression_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllTypedPatternAfterWithAbstraction_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "IllegalDeclarationBeforeTopLevelModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalDeclarationInDataDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllegalHidingInPostfixProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "IllegalLetInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllegalPatternInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllformedProjectionPatternAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IllformedProjectionPatternConcrete_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "IncorrectTypeForRewriteRelation_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InstanceNoCandidate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceSearchDepthExhausted_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidFileName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidModalTelescopeUse_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidProjectionParameter_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InvalidPun_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "InvalidTypeSort_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LambdaIsErased_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibTooFarDown_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "LiteralTooBig_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroResultTypeMismatch_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MetaCannotDependOn_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MetaErasedSolution_" 'PrefixI 'False) (U1 :: Type -> Type)))))))) :+: ((((((C1 ('MetaCons "MetaIrrelevantSolution_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MismatchedProjectionsError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingTypeSignature_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun_)))) :+: ((C1 ('MetaCons "ModuleArityMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleDefinedInOtherFile_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ModuleNameDoesntMatchFileName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNameUnexpected_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MultipleFixityDecls_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MultiplePolarityPragmas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExplicitPolarityVsPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConstructorNameOfNonRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NamedWhereModuleInRefinedContext_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NeedOptionAllowExec_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionCopatterns_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NeedOptionCubical_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeedOptionPatternMatching_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionProp_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NeedOptionRewriting_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionSizedTypes_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NeedOptionTwoLevel_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NeedOptionUniversePolymorphism_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NegativeLiteralInPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoBindingForBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoBindingForPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoKnownRecordWithSuchFields_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NoParameterOfName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoParseForApplication_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoParseForLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoSuchBuiltinName_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "NoSuchModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoSuchPrimitiveFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotAValidLetBinding_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NotAValidLetBinding))))) :+: ((C1 ('MetaCons "NotAValidLetExpression_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAValidLetExpression)) :+: C1 ('MetaCons "NotAllowedInDotPatterns_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAllowedInDotPatterns))) :+: (C1 ('MetaCons "NotAnExpression_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotInScope_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NotLeqSort_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotValidBeforeField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OverlappingProjects_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PathAbstractionFailed_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternInPathLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternInSystem_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatternSynonymArgumentShadows_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "PostulatedSizeInModule_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrivateRecordField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjectionIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QualifiedLocalModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "QuantityMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecordIsErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RecursiveRecordNeedsInductivity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReferencesFutureVariables_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "RelevanceMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RepeatedNamesInImportDirective_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RepeatedVariablesInPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowedModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ShouldBeASort_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldBeEmpty_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ShouldBePath_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldBePi_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "ShouldBeRecordPattern_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ShouldBeRecordType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShouldEndInApplicationOfTheDatatype_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SolvedButOpenHoles_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SortCannotDependOnItsIndex_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SortDoesNotAdmitDataDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SortOfSplitVarError_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "SplitInProp_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SplitOnCoinductive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SplitOnNonEtaRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnNonVariable_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SplitOnPartial_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SplitOnUnchecked_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "SplitOnUnusableCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SplitOnUnusablePolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TacticAttributeNotAllowed_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TooFewArgumentsToPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooFewPatternsInWithClause_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooManyPatternsInWithClause_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TriedToCopyConstrainedPrim_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidInstanceHeadType_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnboundVariablesInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalCohesion_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnequalFiniteness_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalHiding_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnequalLevel_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalQuantity_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "UnequalRelevance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnequalPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalSorts_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnequalTerms_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedModalityAnnotationInParameter_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnexpectedParameter_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedTypeSignatureForParameter_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "UnexpectedWithPatterns_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownBackend_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnusableAtModality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnusedVariableInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VariableIsErased_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VariableIsIrrelevant_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VariableIsOfUnusableCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VariableIsOfUnusablePolarity_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "WithClausePatternMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithOnFreeVariable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongAnnotationInLambda_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongArgInfoForPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongCohesionInLambda_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongPolarityInLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongHidingInApplication_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "WrongHidingInLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongHidingInLambda_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongHidingInProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongIrrelevanceInLambda_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongNamedArgument_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongNumberOfConstructorArguments_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongQuantityInLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongSharpArity_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

data DeclarationException_ Source #

Nicifier errors.

Constructors

AmbiguousConstructorN_ |
AmbiguousFunClauses_ |
BadMacroDef_ |
DisallowedInterleavedMutual_ |
DuplicateAnonDeclaration_ |
DuplicateDefinition_ |
InvalidMeasureMutual_ |
MissingWithClauses_ |
MultipleEllipses_ |
OpaqueInMutual_ |
UnfoldingOutsideOpaque_ |
UnquoteDefRequiresSignature_ |
WrongContentBlock_ |
WrongDefinition_ |

#### Instances

Instances details

Bounded DeclarationException_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: DeclarationException_ Source # maxBound :: DeclarationException_ Source #
Enum DeclarationException_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: DeclarationException_ -> DeclarationException_ Source #

pred :: DeclarationException_ -> DeclarationException_ Source #

toEnum :: Int -> DeclarationException_ Source #

fromEnum :: DeclarationException_ -> Int Source #

enumFrom :: DeclarationException_ -> [DeclarationException_] Source #

enumFromThen :: DeclarationException_ -> DeclarationException_ -> [DeclarationException_] Source #

enumFromTo :: DeclarationException_ -> DeclarationException_ -> [DeclarationException_] Source #

enumFromThenTo :: DeclarationException_ -> DeclarationException_ -> DeclarationException_ -> [DeclarationException_] Source #

Generic DeclarationException_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep DeclarationException_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep DeclarationException_ = D1 ('MetaData "DeclarationException_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "AmbiguousConstructorN_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AmbiguousFunClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadMacroDef_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DisallowedInterleavedMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateAnonDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidMeasureMutual_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MissingWithClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MultipleEllipses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OpaqueInMutual_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnfoldingOutsideOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnquoteDefRequiresSignature_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongContentBlock_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: DeclarationException_ -> Rep DeclarationException_ x Source #

to :: Rep DeclarationException_ x -> DeclarationException_ Source #

Show DeclarationException_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> DeclarationException_ -> ShowS Source # show :: DeclarationException_ -> String Source # showList :: [DeclarationException_] -> ShowS Source #
type Rep DeclarationException_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep DeclarationException_ = D1 ('MetaData "DeclarationException_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "AmbiguousConstructorN_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AmbiguousFunClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadMacroDef_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DisallowedInterleavedMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateAnonDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidMeasureMutual_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MissingWithClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MultipleEllipses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OpaqueInMutual_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnfoldingOutsideOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnquoteDefRequiresSignature_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WrongContentBlock_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)))))

data GHCBackendError_ Source #

Constructors

ConstructorCountMismatch_ |
NotAHaskellType_ NotAHaskellType_ |
WrongTypeOfMain_ |

#### Instances

Instances details

Bounded GHCBackendError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: GHCBackendError_ Source # maxBound :: GHCBackendError_ Source #
Enum GHCBackendError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: GHCBackendError_ -> GHCBackendError_ Source #

pred :: GHCBackendError_ -> GHCBackendError_ Source #

toEnum :: Int -> GHCBackendError_ Source #

fromEnum :: GHCBackendError_ -> Int Source #

enumFrom :: GHCBackendError_ -> [GHCBackendError_] Source #

enumFromThen :: GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] Source #

enumFromTo :: GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] Source #

enumFromThenTo :: GHCBackendError_ -> GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] Source #

Generic GHCBackendError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep GHCBackendError_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep GHCBackendError_ = D1 ('MetaData "GHCBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConstructorCountMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAHaskellType_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAHaskellType_)) :+: C1 ('MetaCons "WrongTypeOfMain_" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: GHCBackendError_ -> Rep GHCBackendError_ x Source #

to :: Rep GHCBackendError_ x -> GHCBackendError_ Source #

Show GHCBackendError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> GHCBackendError_ -> ShowS Source # show :: GHCBackendError_ -> String Source # showList :: [GHCBackendError_] -> ShowS Source #
type Rep GHCBackendError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep GHCBackendError_ = D1 ('MetaData "GHCBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConstructorCountMismatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAHaskellType_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAHaskellType_)) :+: C1 ('MetaCons "WrongTypeOfMain_" 'PrefixI 'False) (U1 :: Type -> Type)))

data JSBackendError_ Source #

Constructors

BadCompilePragma_ |

#### Instances

Instances details

Bounded JSBackendError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: JSBackendError_ Source # maxBound :: JSBackendError_ Source #
Enum JSBackendError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: JSBackendError_ -> JSBackendError_ Source #

pred :: JSBackendError_ -> JSBackendError_ Source #

toEnum :: Int -> JSBackendError_ Source #

fromEnum :: JSBackendError_ -> Int Source #

enumFrom :: JSBackendError_ -> [JSBackendError_] Source #

enumFromThen :: JSBackendError_ -> JSBackendError_ -> [JSBackendError_] Source #

enumFromTo :: JSBackendError_ -> JSBackendError_ -> [JSBackendError_] Source #

enumFromThenTo :: JSBackendError_ -> JSBackendError_ -> JSBackendError_ -> [JSBackendError_] Source #

Generic JSBackendError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep JSBackendError_ |
Instance details Defined in Agda.Interaction.Options.Errors type Rep JSBackendError_ = D1 ('MetaData "JSBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "BadCompilePragma_" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: JSBackendError_ -> Rep JSBackendError_ x Source #

to :: Rep JSBackendError_ x -> JSBackendError_ Source #

Show JSBackendError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> JSBackendError_ -> ShowS Source # show :: JSBackendError_ -> String Source # showList :: [JSBackendError_] -> ShowS Source #
type Rep JSBackendError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep JSBackendError_ = D1 ('MetaData "JSBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "BadCompilePragma_" 'PrefixI 'False) (U1 :: Type -> Type))

data InteractionError_ Source #

Constructors

CannotGive_ |
CannotRefine_ |
CaseSplitError_ |
ExpectedIdentifier_ |
ExpectedApplication_ |
NoActionForInteractionPoint_ |
NoSuchInteractionPoint_ |
UnexpectedWhere_ |

#### Instances

Instances details

Bounded InteractionError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: InteractionError_ Source # maxBound :: InteractionError_ Source #
Enum InteractionError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: InteractionError_ -> InteractionError_ Source #

pred :: InteractionError_ -> InteractionError_ Source #

toEnum :: Int -> InteractionError_ Source #

fromEnum :: InteractionError_ -> Int Source #

enumFrom :: InteractionError_ -> [InteractionError_] Source #

enumFromThen :: InteractionError_ -> InteractionError_ -> [InteractionError_] Source #

enumFromTo :: InteractionError_ -> InteractionError_ -> [InteractionError_] Source #

enumFromThenTo :: InteractionError_ -> InteractionError_ -> InteractionError_ -> [InteractionError_] Source #

Generic InteractionError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep InteractionError_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep InteractionError_ = D1 ('MetaData "InteractionError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "CannotGive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotRefine_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CaseSplitError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpectedIdentifier_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ExpectedApplication_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoActionForInteractionPoint_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoSuchInteractionPoint_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedWhere_" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: InteractionError_ -> Rep InteractionError_ x Source #

to :: Rep InteractionError_ x -> InteractionError_ Source #

Show InteractionError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> InteractionError_ -> ShowS Source # show :: InteractionError_ -> String Source # showList :: [InteractionError_] -> ShowS Source #
type Rep InteractionError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep InteractionError_ = D1 ('MetaData "InteractionError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "CannotGive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotRefine_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CaseSplitError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpectedIdentifier_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ExpectedApplication_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoActionForInteractionPoint_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NoSuchInteractionPoint_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnexpectedWhere_" 'PrefixI 'False) (U1 :: Type -> Type))))

data NegativeUnification_ Source #

Constructors

UnifyConflict_ |
UnifyCycle_ |

#### Instances

Instances details

Bounded NegativeUnification_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: NegativeUnification_ Source # maxBound :: NegativeUnification_ Source #
Enum NegativeUnification_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: NegativeUnification_ -> NegativeUnification_ Source #

pred :: NegativeUnification_ -> NegativeUnification_ Source #

toEnum :: Int -> NegativeUnification_ Source #

fromEnum :: NegativeUnification_ -> Int Source #

enumFrom :: NegativeUnification_ -> [NegativeUnification_] Source #

enumFromThen :: NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] Source #

enumFromTo :: NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] Source #

enumFromThenTo :: NegativeUnification_ -> NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] Source #

Generic NegativeUnification_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep NegativeUnification_ |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NegativeUnification_ = D1 ('MetaData "NegativeUnification_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnifyConflict_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnifyCycle_" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: NegativeUnification_ -> Rep NegativeUnification_ x Source #

to :: Rep NegativeUnification_ x -> NegativeUnification_ Source #

Show NegativeUnification_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NegativeUnification_ -> ShowS Source # show :: NegativeUnification_ -> String Source # showList :: [NegativeUnification_] -> ShowS Source #
type Rep NegativeUnification_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors type Rep NegativeUnification_ = D1 ('MetaData "NegativeUnification_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnifyConflict_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnifyCycle_" 'PrefixI 'False) (U1 :: Type -> Type))

data NotAHaskellType_ Source #

Constructors

BadDontCare_ |
BadLambda_ |
BadMeta_ |
NoPragmaFor_ |
NotCompiled_ |
WrongPragmaFor_ |

#### Instances

Instances details

Bounded NotAHaskellType_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: NotAHaskellType_ Source # maxBound :: NotAHaskellType_ Source #
Enum NotAHaskellType_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: NotAHaskellType_ -> NotAHaskellType_ Source #

pred :: NotAHaskellType_ -> NotAHaskellType_ Source #

toEnum :: Int -> NotAHaskellType_ Source #

fromEnum :: NotAHaskellType_ -> Int Source #

enumFrom :: NotAHaskellType_ -> [NotAHaskellType_] Source #

enumFromThen :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] Source #

enumFromTo :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] Source #

enumFromThenTo :: NotAHaskellType_ -> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] Source #

Generic NotAHaskellType_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep NotAHaskellType_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep NotAHaskellType_ = D1 ('MetaData "NotAHaskellType_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "BadDontCare_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BadLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadMeta_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "NoPragmaFor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotCompiled_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongPragmaFor_" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: NotAHaskellType_ -> Rep NotAHaskellType_ x Source #

to :: Rep NotAHaskellType_ x -> NotAHaskellType_ Source #

Show NotAHaskellType_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAHaskellType_ -> ShowS Source # show :: NotAHaskellType_ -> String Source # showList :: [NotAHaskellType_] -> ShowS Source #
type Rep NotAHaskellType_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep NotAHaskellType_ = D1 ('MetaData "NotAHaskellType_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "BadDontCare_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BadLambda_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BadMeta_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "NoPragmaFor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotCompiled_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongPragmaFor_" 'PrefixI 'False) (U1 :: Type -> Type))))

data SplitError_ Source #

Constructors

ErasedDatatype_ ErasedDatatypeReason |
GenericSplitError_ |
BlockedType_ |
CannotCreateMissingClause_ |
CoinductiveDatatype_ |
CosplitCatchall_ |
CosplitNoRecordType_ |
CosplitNoTarget_ |
NotADatatype_ |
UnificationStuck_ |

#### Instances

Instances details

Bounded SplitError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: SplitError_ Source # maxBound :: SplitError_ Source #
Enum SplitError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: SplitError_ -> SplitError_ Source #

pred :: SplitError_ -> SplitError_ Source #

toEnum :: Int -> SplitError_ Source #

fromEnum :: SplitError_ -> Int Source #

enumFrom :: SplitError_ -> [SplitError_] Source #

enumFromThen :: SplitError_ -> SplitError_ -> [SplitError_] Source #

enumFromTo :: SplitError_ -> SplitError_ -> [SplitError_] Source #

enumFromThenTo :: SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_] Source #

Generic SplitError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep SplitError_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep SplitError_ = D1 ('MetaData "SplitError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "ErasedDatatype_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErasedDatatypeReason)) :+: C1 ('MetaCons "GenericSplitError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BlockedType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotCreateMissingClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoinductiveDatatype_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "CosplitCatchall_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CosplitNoRecordType_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosplitNoTarget_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotADatatype_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationStuck_" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: SplitError_ -> Rep SplitError_ x Source #

to :: Rep SplitError_ x -> SplitError_ Source #

Show SplitError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> SplitError_ -> ShowS Source # show :: SplitError_ -> String Source # showList :: [SplitError_] -> ShowS Source #
type Rep SplitError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep SplitError_ = D1 ('MetaData "SplitError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "ErasedDatatype_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErasedDatatypeReason)) :+: C1 ('MetaCons "GenericSplitError_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BlockedType_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotCreateMissingClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoinductiveDatatype_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "CosplitCatchall_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CosplitNoRecordType_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosplitNoTarget_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotADatatype_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationStuck_" 'PrefixI 'False) (U1 :: Type -> Type)))))

data CannotQuote_ Source #

Constructors

CannotQuoteAmbiguous_ |
CannotQuoteExpression_ |
CannotQuoteHidden_ |
CannotQuoteNothing_ |
CannotQuotePattern_ |

#### Instances

Instances details

Bounded CannotQuote_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: CannotQuote_ Source # maxBound :: CannotQuote_ Source #
Enum CannotQuote_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: CannotQuote_ -> CannotQuote_ Source #

pred :: CannotQuote_ -> CannotQuote_ Source #

toEnum :: Int -> CannotQuote_ Source #

fromEnum :: CannotQuote_ -> Int Source #

enumFrom :: CannotQuote_ -> [CannotQuote_] Source #

enumFromThen :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_] Source #

enumFromTo :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_] Source #

enumFromThenTo :: CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_] Source #

Generic CannotQuote_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep CannotQuote_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep CannotQuote_ = D1 ('MetaData "CannotQuote_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "CannotQuoteAmbiguous_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuoteExpression_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotQuoteHidden_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotQuoteNothing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuotePattern_" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: CannotQuote_ -> Rep CannotQuote_ x Source #

to :: Rep CannotQuote_ x -> CannotQuote_ Source #

Show CannotQuote_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> CannotQuote_ -> ShowS Source # show :: CannotQuote_ -> String Source # showList :: [CannotQuote_] -> ShowS Source #
type Rep CannotQuote_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep CannotQuote_ = D1 ('MetaData "CannotQuote_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "CannotQuoteAmbiguous_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuoteExpression_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotQuoteHidden_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotQuoteNothing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CannotQuotePattern_" 'PrefixI 'False) (U1 :: Type -> Type))))

data ExecError_ Source #

Constructors

ExeNotTrusted_ |
ExeNotFound_ |
ExeNotExecutable_ |

#### Instances

Instances details

Bounded ExecError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: ExecError_ Source # maxBound :: ExecError_ Source #
Enum ExecError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: ExecError_ -> ExecError_ Source #

pred :: ExecError_ -> ExecError_ Source #

toEnum :: Int -> ExecError_ Source #

fromEnum :: ExecError_ -> Int Source #

enumFrom :: ExecError_ -> [ExecError_] Source #

enumFromThen :: ExecError_ -> ExecError_ -> [ExecError_] Source #

enumFromTo :: ExecError_ -> ExecError_ -> [ExecError_] Source #

enumFromThenTo :: ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_] Source #

Generic ExecError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep ExecError_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ExecError_ = D1 ('MetaData "ExecError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ExeNotTrusted_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ExeNotFound_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExeNotExecutable_" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: ExecError_ -> Rep ExecError_ x Source #

to :: Rep ExecError_ x -> ExecError_ Source #

Show ExecError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> ExecError_ -> ShowS Source # show :: ExecError_ -> String Source # showList :: [ExecError_] -> ShowS Source #
type Rep ExecError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep ExecError_ = D1 ('MetaData "ExecError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ExeNotTrusted_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ExeNotFound_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExeNotExecutable_" 'PrefixI 'False) (U1 :: Type -> Type)))

data UnquoteError_ Source #

Constructors

BlockedOnMeta_ |
CannotDeclareHiddenFunction_ |
CommitAfterDef_ |
ConInsteadOfDef_ |
DefineDataNotData_ |
DefInsteadOfCon_ |
MissingDeclaration_ |
MissingDefinition_ |
NakedUnquote_ |
NonCanonical_ |
PatLamWithoutClauses_ |
StaleMeta_ |
TooManyParameters_ |
UnboundName_ |

#### Instances

Instances details

Bounded UnquoteError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods minBound :: UnquoteError_ Source # maxBound :: UnquoteError_ Source #
Enum UnquoteError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Methods

succ :: UnquoteError_ -> UnquoteError_ Source #

pred :: UnquoteError_ -> UnquoteError_ Source #

toEnum :: Int -> UnquoteError_ Source #

fromEnum :: UnquoteError_ -> Int Source #

enumFrom :: UnquoteError_ -> [UnquoteError_] Source #

enumFromThen :: UnquoteError_ -> UnquoteError_ -> [UnquoteError_] Source #

enumFromTo :: UnquoteError_ -> UnquoteError_ -> [UnquoteError_] Source #

enumFromThenTo :: UnquoteError_ -> UnquoteError_ -> UnquoteError_ -> [UnquoteError_] Source #

Generic UnquoteError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

Associated Types

type Rep UnquoteError_ |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep UnquoteError_ = D1 ('MetaData "UnquoteError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "BlockedOnMeta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotDeclareHiddenFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CommitAfterDef_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConInsteadOfDef_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DefineDataNotData_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DefInsteadOfCon_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MissingDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NakedUnquote_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonCanonical_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatLamWithoutClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StaleMeta_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TooManyParameters_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnboundName_" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: UnquoteError_ -> Rep UnquoteError_ x Source #

to :: Rep UnquoteError_ x -> UnquoteError_ Source #

Show UnquoteError_ Source # |
Instance details Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> UnquoteError_ -> ShowS Source # show :: UnquoteError_ -> String Source # showList :: [UnquoteError_] -> ShowS Source #
type Rep UnquoteError_ Source # |

Instance details

Defined in Agda.Interaction.Options.Errors

type Rep UnquoteError_ = D1 ('MetaData "UnquoteError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "BlockedOnMeta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotDeclareHiddenFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CommitAfterDef_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ConInsteadOfDef_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DefineDataNotData_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DefInsteadOfCon_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MissingDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NakedUnquote_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonCanonical_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatLamWithoutClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StaleMeta_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TooManyParameters_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnboundName_" 'PrefixI 'False) (U1 :: Type -> Type)))))

# Printing error names

defaultErrorNameString :: Show a => a -> String Source #

erasedDatatypeReasonString :: ErasedDatatypeReason -> String Source #

errorNameString :: ErrorName -> String Source #

constructorOrPatternSynonymNameString :: ConstructorOrPatternSynonym -> String Source #

dataRecOrFunString :: DataRecOrFun_ -> String Source #

declarationExceptionNameString :: DeclarationException_ -> String Source #

ghcBackendErrorNameString :: GHCBackendError_ -> String Source #

jsBackendErrorNameString :: JSBackendError_ -> String Source #

interactionErrorNameString :: InteractionError_ -> String Source #

negativeUnificationErrorNameString :: NegativeUnification_ -> String Source #

notAHaskellTypeErrorNameString :: NotAHaskellType_ -> String Source #

notAValidLetBindingString :: NotAValidLetBinding -> String Source #

notAValidLetExpressionString :: NotAValidLetExpression -> String Source #

notAllowedInDotPatternsString :: NotAllowedInDotPatterns -> String Source #

splitErrorNameString :: SplitError_ -> String Source #

cannotQuoteNameString :: CannotQuote_ -> String Source #

cannotQuoteTermNameString :: CannotQuoteTerm -> String Source #

execErrorNameString :: ExecError_ -> String Source #

unquoteErrorNameString :: UnquoteError_ -> String Source #

helpErrors :: String Source #

Print list of errors.

# Print error messages

verbalizeNotAValidLetBinding :: NotAValidLetBinding -> String Source #

verbalizeNotAValidLetExpression :: NotAValidLetExpression -> String Source #

# Orphan instances

(Bounded a, Enum a) => Bounded (Maybe a) Source # |
Instance details Methods minBound :: Maybe a Source # maxBound :: Maybe a Source #
(Bounded a, Enum a) => Enum (Maybe a) Source # |
Instance details Methods succ :: Maybe a -> Maybe a Source # pred :: Maybe a -> Maybe a Source # toEnum :: Int -> Maybe a Source # fromEnum :: Maybe a -> Int Source # enumFrom :: Maybe a -> [Maybe a] Source # enumFromThen :: Maybe a -> Maybe a -> [Maybe a] Source # enumFromTo :: Maybe a -> Maybe a -> [Maybe a] Source # enumFromThenTo :: Maybe a -> Maybe a -> Maybe a -> [Maybe a] Source #