| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.Interaction.Options.Errors
Description
Provide names for the errors Agda throws.Options/Er
Synopsis
- data CannotQuoteTerm
- data DataRecOrFun_
- data NotAllowedInDotPatterns
- data NotAValidLetBinding
- data NotAValidLetExpression = MissingBody
- data ErrorName
- = ExecError_ ExecError_
- | ImpossibleConstructor_ NegativeUnification_
- | SplitError_ SplitError_
- | CompilationError_
- | CustomBackendError_
- | InternalError_
- | LibraryError_
- | NonFatalErrors_
- | OptionError_
- | SyntaxError_
- | UserError_
- | AbsentRHSRequiresAbsurdPattern_
- | AbstractConstructorNotInScope_
- | AmbiguousConstructor_
- | AmbiguousField_
- | AmbiguousModule_
- | AmbiguousName_
- | AmbiguousOverloadedProjection_
- | AmbiguousParseForApplication_
- | AmbiguousParseForLHS_
- | AmbiguousProjection_
- | AmbiguousTopLevelModuleName_
- | AsPatternInPatternSynonym_
- | BackendDoesNotSupportOnlyScopeChecking_
- | BadArgumentsToPatternSynonym_
- | BothWithAndRHS_
- | BuiltinInParameterisedModule_
- | BuiltinMustBeConstructor_
- | BuiltinMustBeData_
- | BuiltinMustBeDef_
- | BuiltinMustBeFunction_
- | BuiltinMustBePostulate_
- | CannotApply_
- | CannotGeneralizeEtaExpandable_
- | CannotGenerateTransportClause_
- | CannotQuote_ CannotQuote_
- | CannotQuoteTerm_ CannotQuoteTerm
- | CannotResolveAmbiguousPatternSynonym_
- | CannotRewriteByNonEquation_
- | CantResolveOverloadedConstructorsTargetingSameDatatype_
- | ClashingDefinition_
- | ClashingModule_
- | ComatchingDisabledForRecord_
- | ConstructorDoesNotTargetGivenType_
- | ConstructorPatternInWrongDatatype_
- | CopatternHeadNotProjection_
- | CubicalPrimitiveNotFullyApplied_
- | CyclicModuleDependency_
- | DeBruijnIndexOutOfScope_
- | DeclarationsAfterTopLevelModule_
- | DefinitionInDifferentModule_
- | DoNotationError_
- | DotPatternInPatternSynonym_
- | DuplicateBuiltinBinding_
- | DuplicateConstructors_
- | DuplicateFields_
- | DuplicateImports_
- | DuplicateOverlapPragma_
- | DuplicatePrimitiveBinding_
- | ExpectedBindingForParameter_
- | ExpectedIntervalLiteral_
- | FieldOutsideRecord_
- | FaceConstraintDisjunction_
- | FaceConstraintUnsatisfiable_
- | FileNotFound_
- | ForcedConstructorNotInstantiated_
- | GeneralizationFailed_
- | GeneralizationPrepruneErrorRefinedContext_
- | GeneralizationPrepruneErrorCyclicDependencies_
- | GeneralizationPrepruneErrorFailedToInstantiate_
- | GeneralizeCyclicDependency_
- | GeneralizeNotSupportedHere_
- | GeneralizedVarInLetOpenedModule_
- | ModuleNameHashCollision_
- | HidingMismatch_
- | IdiomBracketError_
- | InvalidBuiltin_
- | InvalidDottedExpression_
- | IllTypedPatternAfterWithAbstraction_
- | IllegalDeclarationBeforeTopLevelModule_
- | IllegalHidingInPostfixProjection_
- | IllegalInstanceVariableInPatternSynonym_
- | IllegalLetInTelescope_
- | IllegalPatternInTelescope_
- | IllformedProjectionPatternAbstract_
- | IllformedProjectionPatternConcrete_
- | InvalidFileName_
- | InvalidPattern_
- | InvalidProjectionParameter_
- | InvalidPun_ ConstructorOrPatternSynonym
- | InvalidTypeSort_
- | LibTooFarDown_
- | LiteralTooBig_
- | MacroResultTypeMismatch_
- | MetaCannotDependOn_
- | MismatchedProjectionsError_
- | MissingBindingsForTelescopeVariables_
- | MissingTypeSignature_ DataRecOrFun_
- | ModuleArityMismatch_
- | ModuleDefinedInOtherFile_
- | ModuleNameDoesntMatchFileName_
- | ModuleNameUnexpected_
- | MultipleFixityDecls_
- | MultiplePolarityPragmas_
- | ConstructorNameOfNonRecord_
- | NonLocalWhereModuleInRefinedContext_
- | NeedOptionAllowExec_
- | NeedOptionCopatterns_
- | NeedOptionCubical_
- | NeedOptionPatternMatching_
- | NeedOptionProp_
- | 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
- | PrivateRecordField_
- | QualifiedLocalModule_
- | ReferencesFutureVariables_
- | RepeatedNamesInImportDirective_
- | RepeatedVariablesInPattern_
- | ShadowedModule_
- | ShouldBeASort_
- | ShouldBeEmpty_
- | ShouldBePath_
- | ShouldBePi_
- | ShouldBeRecordPattern_
- | ShouldBeRecordType_
- | ShouldEndInApplicationOfTheDatatype_
- | SolvedButOpenHoles_
- | SortCannotDependOnItsIndex_
- | SortDoesNotAdmitDataDefinitions_
- | TacticAttributeNotAllowed_
- | TooFewArgumentsToPatternSynonym_
- | TooFewPatternsInWithClause_
- | TooManyFields_
- | TooManyPatternsInWithClause_
- | TriedToCopyConstrainedPrim_
- | UnboundVariablesInPatternSynonym_
- | UnequalTerms_
- | UnequalTypes_
- | UnexpectedParameter_
- | UnexpectedTypeSignatureForParameter_
- | UnexpectedWithPatterns_
- | UnknownBackend_
- | UnusedVariableInPatternSynonym_
- | WithClausePatternMismatch_
- | WithOnFreeVariable_
- | WrongAnnotationInLambda_
- | WrongHidingInApplication_
- | WrongHidingInLHS_
- | WrongHidingInLambda_
- | WrongHidingInProjection_
- | WrongNamedArgument_
- | WrongNumberOfConstructorArguments_
- data NegativeUnification_
- data NotAHaskellType_
- data SplitError_
- = GenericSplitError_
- | BlockedType_
- | CannotCreateMissingClause_
- | CannotEliminateWithPattern_
- | CannotEliminateWithProjection_
- | CoinductiveDatatype_
- | CosplitNoRecordType_
- | CosplitNoTarget_
- | NotADatatype_
- | UnificationStuck_
- | SortOfSplitVarError_
- | SplitInProp_
- | SplitOnAbstract_
- | SplitOnCoinductive_
- | SplitOnNonEtaRecord_
- | SplitOnNonVariable_
- | SplitOnPartial_
- | SplitOnUnchecked_
- data CannotQuote_
- data ExecError_
- defaultErrorNameString :: Show a => a -> String
- errorNameString :: ErrorName -> String
- constructorOrPatternSynonymNameString :: ConstructorOrPatternSynonym -> String
- dataRecOrFunString :: DataRecOrFun_ -> 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
- helpErrors :: String
- verbalizeNotAValidLetBinding :: NotAValidLetBinding -> String
- verbalizeNotAValidLetExpression :: NotAValidLetExpression -> String
Documentation
data CannotQuoteTerm Source #
Extra information for error CannotQuoteTerm.
Constructors
| CannotQuoteTermHidden Hiding | |
| CannotQuoteTermNothing |
Instances
data DataRecOrFun_ Source #
What kind of declaration?
See also DataRecOrFun.
Instances
| Bounded DataRecOrFun_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum DataRecOrFun_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
| |||||
| Show DataRecOrFun_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> DataRecOrFun_ -> ShowS # show :: DataRecOrFun_ -> String # showList :: [DataRecOrFun_] -> ShowS # | |||||
| type Rep DataRecOrFun_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep DataRecOrFun_ = D1 ('MetaData "DataRecOrFun_" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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 NotAllowedInDotPatterns Source #
Things not allowed in dot patterns.
Constructors
| LetExpressions | |
| PatternLambdas |
Instances
| NFData NotAllowedInDotPatterns Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods rnf :: NotAllowedInDotPatterns -> () # | |||||
| Bounded NotAllowedInDotPatterns Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum NotAllowedInDotPatterns Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
Methods from :: NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x # to :: Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns # | |||||
| Show NotAllowedInDotPatterns Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> NotAllowedInDotPatterns -> ShowS # show :: NotAllowedInDotPatterns -> String # showList :: [NotAllowedInDotPatterns] -> ShowS # | |||||
| type Rep NotAllowedInDotPatterns Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
data NotAValidLetBinding Source #
Reasons for error NotAValidLetBinding.
Instances
| NFData NotAValidLetBinding Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods rnf :: NotAValidLetBinding -> () # | |||||
| Bounded NotAValidLetBinding Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum NotAValidLetBinding Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
Methods from :: NotAValidLetBinding -> Rep NotAValidLetBinding x # to :: Rep NotAValidLetBinding x -> NotAValidLetBinding # | |||||
| Show NotAValidLetBinding Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> NotAValidLetBinding -> ShowS # show :: NotAValidLetBinding -> String # showList :: [NotAValidLetBinding] -> ShowS # | |||||
| type Rep NotAValidLetBinding Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep NotAValidLetBinding = D1 ('MetaData "NotAValidLetBinding" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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) :+: C1 ('MetaCons "CopatternsNotAllowed" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
data NotAValidLetExpression Source #
Reasons for error NotAValidLetExpression.
Constructors
| MissingBody |
Instances
| NFData NotAValidLetExpression Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods rnf :: NotAValidLetExpression -> () # | |||||
| Bounded NotAValidLetExpression Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum NotAValidLetExpression Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
Methods from :: NotAValidLetExpression -> Rep NotAValidLetExpression x # to :: Rep NotAValidLetExpression x -> NotAValidLetExpression # | |||||
| Show NotAValidLetExpression Source # | |||||
Defined in Mikan.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_ | |
| ImpossibleConstructor_ NegativeUnification_ | |
| SplitError_ SplitError_ | |
| CompilationError_ | |
| CustomBackendError_ | |
| InternalError_ | |
| LibraryError_ | |
| NonFatalErrors_ | |
| OptionError_ | |
| SyntaxError_ | |
| UserError_ | |
| AbsentRHSRequiresAbsurdPattern_ | |
| AbstractConstructorNotInScope_ | |
| AmbiguousConstructor_ | |
| AmbiguousField_ | |
| AmbiguousModule_ | |
| AmbiguousName_ | |
| AmbiguousOverloadedProjection_ | |
| AmbiguousParseForApplication_ | |
| AmbiguousParseForLHS_ | |
| AmbiguousProjection_ | |
| AmbiguousTopLevelModuleName_ | |
| AsPatternInPatternSynonym_ | |
| BackendDoesNotSupportOnlyScopeChecking_ | |
| BadArgumentsToPatternSynonym_ | |
| BothWithAndRHS_ | |
| BuiltinInParameterisedModule_ | |
| BuiltinMustBeConstructor_ | |
| BuiltinMustBeData_ | |
| BuiltinMustBeDef_ | |
| BuiltinMustBeFunction_ | |
| BuiltinMustBePostulate_ | |
| CannotApply_ | |
| CannotGeneralizeEtaExpandable_ | |
| CannotGenerateTransportClause_ | |
| CannotQuote_ CannotQuote_ | |
| CannotQuoteTerm_ CannotQuoteTerm | |
| CannotResolveAmbiguousPatternSynonym_ | |
| CannotRewriteByNonEquation_ | |
| CantResolveOverloadedConstructorsTargetingSameDatatype_ | |
| ClashingDefinition_ | |
| ClashingModule_ | |
| ComatchingDisabledForRecord_ | |
| ConstructorDoesNotTargetGivenType_ | |
| ConstructorPatternInWrongDatatype_ | |
| CopatternHeadNotProjection_ | |
| CubicalPrimitiveNotFullyApplied_ | |
| CyclicModuleDependency_ | |
| DeBruijnIndexOutOfScope_ | |
| DeclarationsAfterTopLevelModule_ | |
| DefinitionInDifferentModule_ | |
| DoNotationError_ | |
| DotPatternInPatternSynonym_ | |
| DuplicateBuiltinBinding_ | |
| DuplicateConstructors_ | |
| DuplicateFields_ | |
| DuplicateImports_ | |
| DuplicateOverlapPragma_ | |
| DuplicatePrimitiveBinding_ | |
| ExpectedBindingForParameter_ | |
| ExpectedIntervalLiteral_ | |
| FieldOutsideRecord_ | |
| FaceConstraintDisjunction_ | |
| FaceConstraintUnsatisfiable_ | |
| FileNotFound_ | |
| ForcedConstructorNotInstantiated_ | |
| GeneralizationFailed_ | |
| GeneralizationPrepruneErrorRefinedContext_ | |
| GeneralizationPrepruneErrorCyclicDependencies_ | |
| GeneralizationPrepruneErrorFailedToInstantiate_ | |
| GeneralizeCyclicDependency_ | |
| GeneralizeNotSupportedHere_ | |
| GeneralizedVarInLetOpenedModule_ | |
| ModuleNameHashCollision_ | |
| HidingMismatch_ | |
| IdiomBracketError_ | |
| InvalidBuiltin_ | |
| InvalidDottedExpression_ | |
| IllTypedPatternAfterWithAbstraction_ | |
| IllegalDeclarationBeforeTopLevelModule_ | |
| IllegalHidingInPostfixProjection_ | |
| IllegalInstanceVariableInPatternSynonym_ | |
| IllegalLetInTelescope_ | |
| IllegalPatternInTelescope_ | |
| IllformedProjectionPatternAbstract_ | |
| IllformedProjectionPatternConcrete_ | |
| InvalidFileName_ | |
| InvalidPattern_ | |
| InvalidProjectionParameter_ | |
| InvalidPun_ ConstructorOrPatternSynonym | |
| InvalidTypeSort_ | |
| LibTooFarDown_ | |
| LiteralTooBig_ | |
| MacroResultTypeMismatch_ | |
| MetaCannotDependOn_ | |
| MismatchedProjectionsError_ | |
| MissingBindingsForTelescopeVariables_ | |
| MissingTypeSignature_ DataRecOrFun_ | |
| ModuleArityMismatch_ | |
| ModuleDefinedInOtherFile_ | |
| ModuleNameDoesntMatchFileName_ | |
| ModuleNameUnexpected_ | |
| MultipleFixityDecls_ | |
| MultiplePolarityPragmas_ | |
| ConstructorNameOfNonRecord_ | |
| NonLocalWhereModuleInRefinedContext_ | |
| NeedOptionAllowExec_ | |
| NeedOptionCopatterns_ | |
| NeedOptionCubical_ | |
| NeedOptionPatternMatching_ | |
| NeedOptionProp_ | |
| 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 | |
| PrivateRecordField_ | |
| QualifiedLocalModule_ | |
| ReferencesFutureVariables_ | |
| RepeatedNamesInImportDirective_ | |
| RepeatedVariablesInPattern_ | |
| ShadowedModule_ | |
| ShouldBeASort_ | |
| ShouldBeEmpty_ | |
| ShouldBePath_ | |
| ShouldBePi_ | |
| ShouldBeRecordPattern_ | |
| ShouldBeRecordType_ | |
| ShouldEndInApplicationOfTheDatatype_ | |
| SolvedButOpenHoles_ | |
| SortCannotDependOnItsIndex_ | |
| SortDoesNotAdmitDataDefinitions_ | |
| TacticAttributeNotAllowed_ | |
| TooFewArgumentsToPatternSynonym_ | |
| TooFewPatternsInWithClause_ | |
| TooManyFields_ | |
| TooManyPatternsInWithClause_ | |
| TriedToCopyConstrainedPrim_ | |
| UnboundVariablesInPatternSynonym_ | |
| UnequalTerms_ | |
| UnequalTypes_ | |
| UnexpectedParameter_ | |
| UnexpectedTypeSignatureForParameter_ | |
| UnexpectedWithPatterns_ | |
| UnknownBackend_ | |
| UnusedVariableInPatternSynonym_ | |
| WithClausePatternMismatch_ | |
| WithOnFreeVariable_ | |
| WrongAnnotationInLambda_ | |
| WrongHidingInApplication_ | |
| WrongHidingInLHS_ | |
| WrongHidingInLambda_ | |
| WrongHidingInProjection_ | |
| WrongNamedArgument_ | |
| WrongNumberOfConstructorArguments_ |
Instances
| Bounded ErrorName Source # | |||||
| Enum ErrorName Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
| |||||
| Show ErrorName Source # | |||||
| type Rep ErrorName Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep ErrorName = D1 ('MetaData "ErrorName" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (((((((C1 ('MetaCons "ExecError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExecError_)) :+: C1 ('MetaCons "ImpossibleConstructor_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NegativeUnification_))) :+: (C1 ('MetaCons "SplitError_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitError_)) :+: (C1 ('MetaCons "CompilationError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendError_" '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 "OptionError_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyntaxError_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "UserError_" '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 "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 "CannotGeneralizeEtaExpandable_" '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 "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 "CopatternHeadNotProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CubicalPrimitiveNotFullyApplied_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CyclicModuleDependency_" '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 "DoNotationError_" '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 "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 "GeneralizationFailed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GeneralizationPrepruneErrorRefinedContext_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizationPrepruneErrorCyclicDependencies_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "GeneralizationPrepruneErrorFailedToInstantiate_" '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 "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 "InvalidFileName_" '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 "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 "MismatchedProjectionsError_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "MissingBindingsForTelescopeVariables_" '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 "ConstructorNameOfNonRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonLocalWhereModuleInRefinedContext_" '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 "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 "PrivateRecordField_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QualifiedLocalModule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReferencesFutureVariables_" '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 "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 "UnboundVariablesInPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnequalTerms_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnequalTypes_" '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 "UnusedVariableInPatternSynonym_" '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 "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 "WrongNamedArgument_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WrongNumberOfConstructorArguments_" 'PrefixI 'False) (U1 :: Type -> Type))))))))) | |||||
data NegativeUnification_ Source #
Constructors
| UnifyConflict_ | |
| UnifyCycle_ |
Instances
| Bounded NegativeUnification_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum NegativeUnification_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
Methods from :: NegativeUnification_ -> Rep NegativeUnification_ x # to :: Rep NegativeUnification_ x -> NegativeUnification_ # | |||||
| Show NegativeUnification_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> NegativeUnification_ -> ShowS # show :: NegativeUnification_ -> String # showList :: [NegativeUnification_] -> ShowS # | |||||
| type Rep NegativeUnification_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
data NotAHaskellType_ Source #
Instances
| Bounded NotAHaskellType_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum NotAHaskellType_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
Methods from :: NotAHaskellType_ -> Rep NotAHaskellType_ x # to :: Rep NotAHaskellType_ x -> NotAHaskellType_ # | |||||
| Show NotAHaskellType_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> NotAHaskellType_ -> ShowS # show :: NotAHaskellType_ -> String # showList :: [NotAHaskellType_] -> ShowS # | |||||
| type Rep NotAHaskellType_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep NotAHaskellType_ = D1 ('MetaData "NotAHaskellType_" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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
| GenericSplitError_ | |
| BlockedType_ | |
| CannotCreateMissingClause_ | |
| CannotEliminateWithPattern_ | |
| CannotEliminateWithProjection_ | |
| CoinductiveDatatype_ | |
| CosplitNoRecordType_ | |
| CosplitNoTarget_ | |
| NotADatatype_ | |
| UnificationStuck_ | |
| SortOfSplitVarError_ | |
| SplitInProp_ | |
| SplitOnAbstract_ | |
| SplitOnCoinductive_ | |
| SplitOnNonEtaRecord_ | |
| SplitOnNonVariable_ | |
| SplitOnPartial_ | |
| SplitOnUnchecked_ |
Instances
| Bounded SplitError_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum SplitError_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
| |||||
| Show SplitError_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> SplitError_ -> ShowS # show :: SplitError_ -> String # showList :: [SplitError_] -> ShowS # | |||||
| type Rep SplitError_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep SplitError_ = D1 ('MetaData "SplitError_" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((((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 "CannotEliminateWithPattern_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CannotEliminateWithProjection_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoinductiveDatatype_" '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) :+: 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 "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)))))) | |||||
data CannotQuote_ Source #
Constructors
| CannotQuoteAmbiguous_ | |
| CannotQuoteExpression_ | |
| CannotQuoteHidden_ | |
| CannotQuoteNothing_ | |
| CannotQuotePattern_ |
Instances
| Bounded CannotQuote_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors | |||||
| Enum CannotQuote_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
| |||||
| Show CannotQuote_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> CannotQuote_ -> ShowS # show :: CannotQuote_ -> String # showList :: [CannotQuote_] -> ShowS # | |||||
| type Rep CannotQuote_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep CannotQuote_ = D1 ('MetaData "CannotQuote_" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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 Mikan.Interaction.Options.Errors | |||||
| Enum ExecError_ Source # | |||||
Defined in Mikan.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 Mikan.Interaction.Options.Errors Associated Types
| |||||
| Show ExecError_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors Methods showsPrec :: Int -> ExecError_ -> ShowS # show :: ExecError_ -> String # showList :: [ExecError_] -> ShowS # | |||||
| type Rep ExecError_ Source # | |||||
Defined in Mikan.Interaction.Options.Errors type Rep ExecError_ = D1 ('MetaData "ExecError_" "Mikan.Interaction.Options.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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))) | |||||
Printing error names
defaultErrorNameString :: Show a => a -> String Source #
errorNameString :: ErrorName -> String Source #
helpErrors :: String Source #
Print list of errors.