| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Options.Errors
Description
Provide names for the errors Agda throws.Options/Er
Synopsis
- data CannotQuoteTerm
- data DataRecOrFun_
- data ErasedDatatypeReason
- data NotAllowedInDotPatterns
- data NotAValidLetBinding
- 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_
- | OpenEverythingInRecordWhere_
- | 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_
- data JSBackendError_ = BadCompilePragma_
- data InteractionError_
- data NegativeUnification_
- data NotAHaskellType_
- data SplitError_
- data CannotQuote_
- data ExecError_
- data UnquoteError_
- 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
data DataRecOrFun_ Source #
What kind of declaration?
See also DataRecOrFun.
Instances
| Bounded DataRecOrFun_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum DataRecOrFun_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: DataRecOrFun_ -> DataRecOrFun_ # pred :: DataRecOrFun_ -> DataRecOrFun_ # toEnum :: Int -> DataRecOrFun_ # fromEnum :: DataRecOrFun_ -> Int # enumFrom :: DataRecOrFun_ -> [DataRecOrFun_] # enumFromThen :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] # enumFromTo :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] # enumFromThenTo :: DataRecOrFun_ -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_] # | |||||
| Generic DataRecOrFun_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show DataRecOrFun_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> DataRecOrFun_ -> ShowS # show :: DataRecOrFun_ -> String # showList :: [DataRecOrFun_] -> ShowS # | |||||
| type Rep DataRecOrFun_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep DataRecOrFun_ = D1 ('MetaData "DataRecOrFun_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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 |
| NoK | The K rule is not activated. |
Instances
| NFData ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods rnf :: ErasedDatatypeReason -> () # | |||||
| Bounded ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: ErasedDatatypeReason -> ErasedDatatypeReason # pred :: ErasedDatatypeReason -> ErasedDatatypeReason # toEnum :: Int -> ErasedDatatypeReason # fromEnum :: ErasedDatatypeReason -> Int # enumFrom :: ErasedDatatypeReason -> [ErasedDatatypeReason] # enumFromThen :: ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] # enumFromTo :: ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] # enumFromThenTo :: ErasedDatatypeReason -> ErasedDatatypeReason -> ErasedDatatypeReason -> [ErasedDatatypeReason] # | |||||
| Generic ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: ErasedDatatypeReason -> Rep ErasedDatatypeReason x # to :: Rep ErasedDatatypeReason x -> ErasedDatatypeReason # | |||||
| Show ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> ErasedDatatypeReason -> ShowS # show :: ErasedDatatypeReason -> String # showList :: [ErasedDatatypeReason] -> ShowS # | |||||
| type Rep ErasedDatatypeReason Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep ErasedDatatypeReason = D1 ('MetaData "ErasedDatatypeReason" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| NFData NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAllowedInDotPatterns -> () # | |||||
| Bounded NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns # pred :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns # toEnum :: Int -> NotAllowedInDotPatterns # fromEnum :: NotAllowedInDotPatterns -> Int # enumFrom :: NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] # enumFromThen :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] # enumFromTo :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] # enumFromThenTo :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns] # | |||||
| Generic NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x # to :: Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns # | |||||
| Show NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAllowedInDotPatterns -> ShowS # show :: NotAllowedInDotPatterns -> String # showList :: [NotAllowedInDotPatterns] -> ShowS # | |||||
| type Rep NotAllowedInDotPatterns Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
data NotAValidLetBinding Source #
Reasons for error NotAValidLetBinding.
Constructors
| MissingRHS | |
| NotAValidLetPattern | |
| WhereClausesNotAllowed |
Instances
| NFData NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAValidLetBinding -> () # | |||||
| Bounded NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: NotAValidLetBinding -> NotAValidLetBinding # pred :: NotAValidLetBinding -> NotAValidLetBinding # toEnum :: Int -> NotAValidLetBinding # fromEnum :: NotAValidLetBinding -> Int # enumFrom :: NotAValidLetBinding -> [NotAValidLetBinding] # enumFromThen :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] # enumFromTo :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] # enumFromThenTo :: NotAValidLetBinding -> NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding] # | |||||
| Generic NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: NotAValidLetBinding -> Rep NotAValidLetBinding x # to :: Rep NotAValidLetBinding x -> NotAValidLetBinding # | |||||
| Show NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAValidLetBinding -> ShowS # show :: NotAValidLetBinding -> String # showList :: [NotAValidLetBinding] -> ShowS # | |||||
| type Rep NotAValidLetBinding Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep NotAValidLetBinding = D1 ('MetaData "NotAValidLetBinding" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| NFData NotAValidLetExpression Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods rnf :: NotAValidLetExpression -> () # | |||||
| Bounded NotAValidLetExpression Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum NotAValidLetExpression Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: NotAValidLetExpression -> NotAValidLetExpression # pred :: NotAValidLetExpression -> NotAValidLetExpression # toEnum :: Int -> NotAValidLetExpression # fromEnum :: NotAValidLetExpression -> Int # enumFrom :: NotAValidLetExpression -> [NotAValidLetExpression] # enumFromThen :: NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] # enumFromTo :: NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] # enumFromThenTo :: NotAValidLetExpression -> NotAValidLetExpression -> NotAValidLetExpression -> [NotAValidLetExpression] # | |||||
| Generic NotAValidLetExpression Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: NotAValidLetExpression -> Rep NotAValidLetExpression x # to :: Rep NotAValidLetExpression x -> NotAValidLetExpression # | |||||
| Show NotAValidLetExpression Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAValidLetExpression -> ShowS # show :: NotAValidLetExpression -> String # showList :: [NotAValidLetExpression] -> ShowS # | |||||
| type Rep NotAValidLetExpression 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_ | |
| OpenEverythingInRecordWhere_ | |
| 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
| Bounded ErrorName Source # | |||||
| Enum ErrorName Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: ErrorName -> ErrorName # pred :: ErrorName -> ErrorName # fromEnum :: ErrorName -> Int # enumFrom :: ErrorName -> [ErrorName] # enumFromThen :: ErrorName -> ErrorName -> [ErrorName] # enumFromTo :: ErrorName -> ErrorName -> [ErrorName] # enumFromThenTo :: ErrorName -> ErrorName -> ErrorName -> [ErrorName] # | |||||
| Generic ErrorName Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show ErrorName Source # | |||||
| type Rep ErrorName Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep ErrorName = D1 ('MetaData "ErrorName" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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 "OpenEverythingInRecordWhere_" '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
| Bounded DeclarationException_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum DeclarationException_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: DeclarationException_ -> DeclarationException_ # pred :: DeclarationException_ -> DeclarationException_ # toEnum :: Int -> DeclarationException_ # fromEnum :: DeclarationException_ -> Int # enumFrom :: DeclarationException_ -> [DeclarationException_] # enumFromThen :: DeclarationException_ -> DeclarationException_ -> [DeclarationException_] # enumFromTo :: DeclarationException_ -> DeclarationException_ -> [DeclarationException_] # enumFromThenTo :: DeclarationException_ -> DeclarationException_ -> DeclarationException_ -> [DeclarationException_] # | |||||
| Generic DeclarationException_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: DeclarationException_ -> Rep DeclarationException_ x # to :: Rep DeclarationException_ x -> DeclarationException_ # | |||||
| Show DeclarationException_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> DeclarationException_ -> ShowS # show :: DeclarationException_ -> String # showList :: [DeclarationException_] -> ShowS # | |||||
| type Rep DeclarationException_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep DeclarationException_ = D1 ('MetaData "DeclarationException_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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 #
Instances
| Bounded GHCBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum GHCBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: GHCBackendError_ -> GHCBackendError_ # pred :: GHCBackendError_ -> GHCBackendError_ # toEnum :: Int -> GHCBackendError_ # fromEnum :: GHCBackendError_ -> Int # enumFrom :: GHCBackendError_ -> [GHCBackendError_] # enumFromThen :: GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] # enumFromTo :: GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] # enumFromThenTo :: GHCBackendError_ -> GHCBackendError_ -> GHCBackendError_ -> [GHCBackendError_] # | |||||
| Generic GHCBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: GHCBackendError_ -> Rep GHCBackendError_ x # to :: Rep GHCBackendError_ x -> GHCBackendError_ # | |||||
| Show GHCBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> GHCBackendError_ -> ShowS # show :: GHCBackendError_ -> String # showList :: [GHCBackendError_] -> ShowS # | |||||
| type Rep GHCBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep GHCBackendError_ = D1 ('MetaData "GHCBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded JSBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum JSBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: JSBackendError_ -> JSBackendError_ # pred :: JSBackendError_ -> JSBackendError_ # toEnum :: Int -> JSBackendError_ # fromEnum :: JSBackendError_ -> Int # enumFrom :: JSBackendError_ -> [JSBackendError_] # enumFromThen :: JSBackendError_ -> JSBackendError_ -> [JSBackendError_] # enumFromTo :: JSBackendError_ -> JSBackendError_ -> [JSBackendError_] # enumFromThenTo :: JSBackendError_ -> JSBackendError_ -> JSBackendError_ -> [JSBackendError_] # | |||||
| Generic JSBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: JSBackendError_ -> Rep JSBackendError_ x # to :: Rep JSBackendError_ x -> JSBackendError_ # | |||||
| Show JSBackendError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> JSBackendError_ -> ShowS # show :: JSBackendError_ -> String # showList :: [JSBackendError_] -> ShowS # | |||||
| type Rep JSBackendError_ Source # | |||||
data InteractionError_ Source #
Constructors
| CannotGive_ | |
| CannotRefine_ | |
| CaseSplitError_ | |
| ExpectedIdentifier_ | |
| ExpectedApplication_ | |
| NoActionForInteractionPoint_ | |
| NoSuchInteractionPoint_ | |
| UnexpectedWhere_ |
Instances
| Bounded InteractionError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum InteractionError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: InteractionError_ -> InteractionError_ # pred :: InteractionError_ -> InteractionError_ # toEnum :: Int -> InteractionError_ # fromEnum :: InteractionError_ -> Int # enumFrom :: InteractionError_ -> [InteractionError_] # enumFromThen :: InteractionError_ -> InteractionError_ -> [InteractionError_] # enumFromTo :: InteractionError_ -> InteractionError_ -> [InteractionError_] # enumFromThenTo :: InteractionError_ -> InteractionError_ -> InteractionError_ -> [InteractionError_] # | |||||
| Generic InteractionError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: InteractionError_ -> Rep InteractionError_ x # to :: Rep InteractionError_ x -> InteractionError_ # | |||||
| Show InteractionError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> InteractionError_ -> ShowS # show :: InteractionError_ -> String # showList :: [InteractionError_] -> ShowS # | |||||
| type Rep InteractionError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep InteractionError_ = D1 ('MetaData "InteractionError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded NegativeUnification_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum NegativeUnification_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: NegativeUnification_ -> NegativeUnification_ # pred :: NegativeUnification_ -> NegativeUnification_ # toEnum :: Int -> NegativeUnification_ # fromEnum :: NegativeUnification_ -> Int # enumFrom :: NegativeUnification_ -> [NegativeUnification_] # enumFromThen :: NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] # enumFromTo :: NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] # enumFromThenTo :: NegativeUnification_ -> NegativeUnification_ -> NegativeUnification_ -> [NegativeUnification_] # | |||||
| Generic NegativeUnification_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: NegativeUnification_ -> Rep NegativeUnification_ x # to :: Rep NegativeUnification_ x -> NegativeUnification_ # | |||||
| Show NegativeUnification_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NegativeUnification_ -> ShowS # show :: NegativeUnification_ -> String # showList :: [NegativeUnification_] -> ShowS # | |||||
| type Rep NegativeUnification_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
data NotAHaskellType_ Source #
Instances
| Bounded NotAHaskellType_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum NotAHaskellType_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: NotAHaskellType_ -> NotAHaskellType_ # pred :: NotAHaskellType_ -> NotAHaskellType_ # toEnum :: Int -> NotAHaskellType_ # fromEnum :: NotAHaskellType_ -> Int # enumFrom :: NotAHaskellType_ -> [NotAHaskellType_] # enumFromThen :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] # enumFromTo :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] # enumFromThenTo :: NotAHaskellType_ -> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_] # | |||||
| Generic NotAHaskellType_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
Methods from :: NotAHaskellType_ -> Rep NotAHaskellType_ x # to :: Rep NotAHaskellType_ x -> NotAHaskellType_ # | |||||
| Show NotAHaskellType_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> NotAHaskellType_ -> ShowS # show :: NotAHaskellType_ -> String # showList :: [NotAHaskellType_] -> ShowS # | |||||
| type Rep NotAHaskellType_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep NotAHaskellType_ = D1 ('MetaData "NotAHaskellType_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded SplitError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum SplitError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: SplitError_ -> SplitError_ # pred :: SplitError_ -> SplitError_ # toEnum :: Int -> SplitError_ # fromEnum :: SplitError_ -> Int # enumFrom :: SplitError_ -> [SplitError_] # enumFromThen :: SplitError_ -> SplitError_ -> [SplitError_] # enumFromTo :: SplitError_ -> SplitError_ -> [SplitError_] # enumFromThenTo :: SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_] # | |||||
| Generic SplitError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show SplitError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> SplitError_ -> ShowS # show :: SplitError_ -> String # showList :: [SplitError_] -> ShowS # | |||||
| type Rep SplitError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep SplitError_ = D1 ('MetaData "SplitError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded CannotQuote_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum CannotQuote_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: CannotQuote_ -> CannotQuote_ # pred :: CannotQuote_ -> CannotQuote_ # toEnum :: Int -> CannotQuote_ # fromEnum :: CannotQuote_ -> Int # enumFrom :: CannotQuote_ -> [CannotQuote_] # enumFromThen :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_] # enumFromTo :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_] # enumFromThenTo :: CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_] # | |||||
| Generic CannotQuote_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show CannotQuote_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> CannotQuote_ -> ShowS # show :: CannotQuote_ -> String # showList :: [CannotQuote_] -> ShowS # | |||||
| type Rep CannotQuote_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep CannotQuote_ = D1 ('MetaData "CannotQuote_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded ExecError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum ExecError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: ExecError_ -> ExecError_ # pred :: ExecError_ -> ExecError_ # toEnum :: Int -> ExecError_ # fromEnum :: ExecError_ -> Int # enumFrom :: ExecError_ -> [ExecError_] # enumFromThen :: ExecError_ -> ExecError_ -> [ExecError_] # enumFromTo :: ExecError_ -> ExecError_ -> [ExecError_] # enumFromThenTo :: ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_] # | |||||
| Generic ExecError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show ExecError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> ExecError_ -> ShowS # show :: ExecError_ -> String # showList :: [ExecError_] -> ShowS # | |||||
| type Rep ExecError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep ExecError_ = D1 ('MetaData "ExecError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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
| Bounded UnquoteError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors | |||||
| Enum UnquoteError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods succ :: UnquoteError_ -> UnquoteError_ # pred :: UnquoteError_ -> UnquoteError_ # toEnum :: Int -> UnquoteError_ # fromEnum :: UnquoteError_ -> Int # enumFrom :: UnquoteError_ -> [UnquoteError_] # enumFromThen :: UnquoteError_ -> UnquoteError_ -> [UnquoteError_] # enumFromTo :: UnquoteError_ -> UnquoteError_ -> [UnquoteError_] # enumFromThenTo :: UnquoteError_ -> UnquoteError_ -> UnquoteError_ -> [UnquoteError_] # | |||||
| Generic UnquoteError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Associated Types
| |||||
| Show UnquoteError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors Methods showsPrec :: Int -> UnquoteError_ -> ShowS # show :: UnquoteError_ -> String # showList :: [UnquoteError_] -> ShowS # | |||||
| type Rep UnquoteError_ Source # | |||||
Defined in Agda.Interaction.Options.Errors type Rep UnquoteError_ = D1 ('MetaData "UnquoteError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0-inplace" '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 #
errorNameString :: ErrorName -> String Source #
helpErrors :: String Source #
Print list of errors.