-- | Convert errors to their names.

module Agda.TypeChecking.Errors.Names where

import Agda.Syntax.Concrete.Definitions.Errors as N (DeclarationException'(..))
import Agda.TypeChecking.Monad.Base            as MB
import Agda.Interaction.Options.Errors

-- | Print the name of a 'TypeError'.
--
typeErrorString :: TypeError -> String
typeErrorString :: TypeError -> String
typeErrorString = ErrorName -> String
errorNameString (ErrorName -> String)
-> (TypeError -> ErrorName) -> TypeError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> ErrorName
typeErrorName

-- | Compute the name of a 'TypeError'.
--
typeErrorName :: TypeError -> ErrorName
typeErrorName :: TypeError -> ErrorName
typeErrorName = \case
  -- Error groups (alphabetically) with named sub errors
  ExecError                ExecError
err -> ExecError_ -> ErrorName
ExecError_             (ExecError_ -> ErrorName) -> ExecError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ ExecError -> ExecError_
execErrorName                  ExecError
err
  GHCBackendError          GHCBackendError
err -> GHCBackendError_ -> ErrorName
GHCBackendError_       (GHCBackendError_ -> ErrorName) -> GHCBackendError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ GHCBackendError -> GHCBackendError_
ghcBackendErrorName            GHCBackendError
err
  JSBackendError           JSBackendError
err -> JSBackendError_ -> ErrorName
JSBackendError_        (JSBackendError_ -> ErrorName) -> JSBackendError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ JSBackendError -> JSBackendError_
jsBackendErrorName             JSBackendError
err
  ImpossibleConstructor QName
_  NegativeUnification
err -> NegativeUnification_ -> ErrorName
ImpossibleConstructor_ (NegativeUnification_ -> ErrorName)
-> NegativeUnification_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName NegativeUnification
err
  InteractionError         InteractionError
err -> InteractionError_ -> ErrorName
InteractionError_      (InteractionError_ -> ErrorName) -> InteractionError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ InteractionError -> InteractionError_
interactionErrorName           InteractionError
err
  NicifierError            DeclarationException'
err -> DeclarationException_ -> ErrorName
NicifierError_         (DeclarationException_ -> ErrorName)
-> DeclarationException_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> DeclarationException_
declarationExceptionName       DeclarationException'
err
  SplitError               SplitError
err -> SplitError_ -> ErrorName
SplitError_            (SplitError_ -> ErrorName) -> SplitError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ SplitError -> SplitError_
splitErrorName                 SplitError
err
  UnquoteFailed            UnquoteError
err -> UnquoteError_ -> ErrorName
UnquoteError_          (UnquoteError_ -> ErrorName) -> UnquoteError_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ UnquoteError -> UnquoteError_
unquoteErrorName               UnquoteError
err
  -- Parametrized errors
  CannotQuote             CannotQuote
what -> CannotQuote_ -> ErrorName
CannotQuote_           (CannotQuote_ -> ErrorName) -> CannotQuote_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ CannotQuote -> CannotQuote_
unquotableName                 CannotQuote
what
  MissingTypeSignature    MissingTypeSignatureInfo
what -> DataRecOrFun_ -> ErrorName
MissingTypeSignature_  (DataRecOrFun_ -> ErrorName) -> DataRecOrFun_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName   MissingTypeSignatureInfo
what
  InvalidPun            ConstructorOrPatternSynonym
kind QName
_ -> ConstructorOrPatternSynonym -> ErrorName
InvalidPun_              ConstructorOrPatternSynonym
kind
  CannotQuoteTerm         CannotQuoteTerm
what -> CannotQuoteTerm -> ErrorName
CannotQuoteTerm_         CannotQuoteTerm
what
  NotAllowedInDotPatterns NotAllowedInDotPatterns
what -> NotAllowedInDotPatterns -> ErrorName
NotAllowedInDotPatterns_ NotAllowedInDotPatterns
what
  NotAValidLetBinding     Maybe NotAValidLetBinding
what -> Maybe NotAValidLetBinding -> ErrorName
NotAValidLetBinding_     Maybe NotAValidLetBinding
what
  NotAValidLetExpression  NotAValidLetExpression
what -> NotAValidLetExpression -> ErrorName
NotAValidLetExpression_  NotAValidLetExpression
what
  PatternSynonymArgumentShadows ConstructorOrPatternSynonym
what Name
_ List1 AbstractName
_ -> ConstructorOrPatternSynonym -> ErrorName
PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym
what
  -- Wrappers
  OperatorInformation [NotationSection]
_    TypeError
err -> TypeError -> ErrorName
typeErrorName TypeError
err
  -- Generic errors (alphabetically)
  CompilationError          {} -> ErrorName
CompilationError_
  CustomBackendError        {} -> ErrorName
CustomBackendError_
  GenericError              {} -> ErrorName
GenericError_
  GenericDocError           {} -> ErrorName
GenericDocError_
  InternalError             {} -> ErrorName
InternalError_
  LibraryError              {} -> ErrorName
LibraryError_
  NonFatalErrors            {} -> ErrorName
NonFatalErrors_
  NotImplemented            {} -> ErrorName
NotImplemented_
  NotSupported              {} -> ErrorName
NotSupported_
  OptionError               {} -> ErrorName
OptionError_
  SyntaxError               {} -> ErrorName
SyntaxError_
  -- Other errors (alphabetically)
  AbsentRHSRequiresAbsurdPattern                             {} -> ErrorName
AbsentRHSRequiresAbsurdPattern_
  AbstractConstructorNotInScope                              {} -> ErrorName
AbstractConstructorNotInScope_
  MB.AmbiguousConstructor                                    {} -> ErrorName
AmbiguousConstructor_
  AmbiguousField                                             {} -> ErrorName
AmbiguousField_
  AmbiguousModule                                            {} -> ErrorName
AmbiguousModule_
  AmbiguousName                                              {} -> ErrorName
AmbiguousName_
  AmbiguousOverloadedProjection                              {} -> ErrorName
AmbiguousOverloadedProjection_
  AmbiguousParseForApplication                               {} -> ErrorName
AmbiguousParseForApplication_
  AmbiguousParseForLHS                                       {} -> ErrorName
AmbiguousParseForLHS_
  AmbiguousProjection                                        {} -> ErrorName
AmbiguousProjection_
  AmbiguousTopLevelModuleName                                {} -> ErrorName
AmbiguousTopLevelModuleName_
  AsPatternInPatternSynonym                                  {} -> ErrorName
AsPatternInPatternSynonym_
  AttributeKindNotEnabled                                    {} -> ErrorName
AttributeKindNotEnabled_
  BackendDoesNotSupportOnlyScopeChecking                     {} -> ErrorName
BackendDoesNotSupportOnlyScopeChecking_
  BadArgumentsToPatternSynonym                               {} -> ErrorName
BadArgumentsToPatternSynonym_
  BuiltinInParameterisedModule                               {} -> ErrorName
BuiltinInParameterisedModule_
  BuiltinMustBeConstructor                                   {} -> ErrorName
BuiltinMustBeConstructor_
  BuiltinMustBeData                                          {} -> ErrorName
BuiltinMustBeData_
  BuiltinMustBeDef                                           {} -> ErrorName
BuiltinMustBeDef_
  BuiltinMustBeFunction                                      {} -> ErrorName
BuiltinMustBeFunction_
  BuiltinMustBePostulate                                     {} -> ErrorName
BuiltinMustBePostulate_
  CannotApply                                                {} -> ErrorName
CannotApply_
  CannotEliminateWithPattern                                 {} -> ErrorName
CannotEliminateWithPattern_
  CannotEliminateWithProjection                              {} -> ErrorName
CannotEliminateWithProjection_
  CannotGenerateHCompClause                                  {} -> ErrorName
CannotGenerateHCompClause_
  CannotGenerateTransportClause                              {} -> ErrorName
CannotGenerateTransportClause_
  CannotResolveAmbiguousPatternSynonym                       {} -> ErrorName
CannotResolveAmbiguousPatternSynonym_
  CannotRewriteByNonEquation                                 {} -> ErrorName
CannotRewriteByNonEquation_
  CannotSolveSizeConstraints                                 {} -> ErrorName
CannotSolveSizeConstraints_
  CantResolveOverloadedConstructorsTargetingSameDatatype     {} -> ErrorName
CantResolveOverloadedConstructorsTargetingSameDatatype_
  ClashingDefinition                                         {} -> ErrorName
ClashingDefinition_
  ClashingModule                                             {} -> ErrorName
ClashingModule_
  ComatchingDisabledForRecord                                {} -> ErrorName
ComatchingDisabledForRecord_
  ConstructorDoesNotTargetGivenType                          {} -> ErrorName
ConstructorDoesNotTargetGivenType_
  ConstructorNameOfNonRecord                                 {} -> ErrorName
ConstructorNameOfNonRecord_
  ConstructorPatternInWrongDatatype                          {} -> ErrorName
ConstructorPatternInWrongDatatype_
  ContradictorySizeConstraint                                {} -> ErrorName
ContradictorySizeConstraint_
  CopatternHeadNotProjection                                 {} -> ErrorName
CopatternHeadNotProjection_
  CubicalCompilationNotSupported                             {} -> ErrorName
CubicalCompilationNotSupported_
  CubicalPrimitiveNotFullyApplied                            {} -> ErrorName
CubicalPrimitiveNotFullyApplied_
  CyclicModuleDependency                                     {} -> ErrorName
CyclicModuleDependency_
  DeBruijnIndexOutOfScope                                    {} -> ErrorName
DeBruijnIndexOutOfScope_
  DeclarationsAfterTopLevelModule                            {} -> ErrorName
DeclarationsAfterTopLevelModule_
  DefinitionInDifferentModule                                {} -> ErrorName
DefinitionInDifferentModule_
  DefinitionIsErased                                         {} -> ErrorName
DefinitionIsErased_
  DefinitionIsIrrelevant                                     {} -> ErrorName
DefinitionIsIrrelevant_
  DoNotationError                                            {} -> ErrorName
DoNotationError_
  DoesNotMentionTicks                                        {} -> ErrorName
DoesNotMentionTicks_
  DotPatternInPatternSynonym                                 {} -> ErrorName
DotPatternInPatternSynonym_
  DuplicateBuiltinBinding                                    {} -> ErrorName
DuplicateBuiltinBinding_
  DuplicateConstructors                                      {} -> ErrorName
DuplicateConstructors_
  DuplicateFields                                            {} -> ErrorName
DuplicateFields_
  DuplicateImports                                           {} -> ErrorName
DuplicateImports_
  DuplicateOverlapPragma                                     {} -> ErrorName
DuplicateOverlapPragma_
  DuplicatePrimitiveBinding                                  {} -> ErrorName
DuplicatePrimitiveBinding_
  EmptyTypeOfSizes                                           {} -> ErrorName
EmptyTypeOfSizes_
  ExpectedBindingForParameter                                {} -> ErrorName
ExpectedBindingForParameter_
  ExpectedIntervalLiteral                                    {} -> ErrorName
ExpectedIntervalLiteral_
  FieldOutsideRecord                                         {} -> ErrorName
FieldOutsideRecord_
  FaceConstraintDisjunction                                  {} -> ErrorName
FaceConstraintDisjunction_
  FaceConstraintUnsatisfiable                                {} -> ErrorName
FaceConstraintUnsatisfiable_
  FileNotFound                                               {} -> ErrorName
FileNotFound_
  ForcedConstructorNotInstantiated                           {} -> ErrorName
ForcedConstructorNotInstantiated_
  FunctionTypeInSizeUniv                                     {} -> ErrorName
FunctionTypeInSizeUniv_
  GeneralizeCyclicDependency                                 {} -> ErrorName
GeneralizeCyclicDependency_
  GeneralizeNotSupportedHere                                 {} -> ErrorName
GeneralizeNotSupportedHere_
  GeneralizedVarInLetOpenedModule                            {} -> ErrorName
GeneralizedVarInLetOpenedModule_
  HidingMismatch                                             {} -> ErrorName
HidingMismatch_
  IdiomBracketError                                          {} -> ErrorName
IdiomBracketError_
  InvalidBuiltin                                             {} -> ErrorName
InvalidBuiltin_
  InvalidDottedExpression                                    {} -> ErrorName
InvalidDottedExpression_
  InvalidFieldModality                                       {} -> ErrorName
InvalidFieldModality_
  IllTypedPatternAfterWithAbstraction                        {} -> ErrorName
IllTypedPatternAfterWithAbstraction_
  IllegalDeclarationBeforeTopLevelModule                     {} -> ErrorName
IllegalDeclarationBeforeTopLevelModule_
  IllegalDeclarationInDataDefinition                         {} -> ErrorName
IllegalDeclarationInDataDefinition_
  IllegalHidingInPostfixProjection                           {} -> ErrorName
IllegalHidingInPostfixProjection_
  IllegalInstanceVariableInPatternSynonym                    {} -> ErrorName
IllegalInstanceVariableInPatternSynonym_
  IllegalLetInTelescope                                      {} -> ErrorName
IllegalLetInTelescope_
  IllegalPatternInTelescope                                  {} -> ErrorName
IllegalPatternInTelescope_
  IllformedProjectionPatternAbstract                         {} -> ErrorName
IllformedProjectionPatternAbstract_
  IllformedProjectionPatternConcrete                         {} -> ErrorName
IllformedProjectionPatternConcrete_
  IncorrectTypeForRewriteRelation                            {} -> ErrorName
IncorrectTypeForRewriteRelation_
  InstanceNoCandidate                                        {} -> ErrorName
InstanceNoCandidate_
  InstanceSearchDepthExhausted                               {} -> ErrorName
InstanceSearchDepthExhausted_
  InvalidFileName                                            {} -> ErrorName
InvalidFileName_
  InvalidModalTelescopeUse                                   {} -> ErrorName
InvalidModalTelescopeUse_
  InvalidPattern                                             {} -> ErrorName
InvalidPattern_
  InvalidProjectionParameter                                 {} -> ErrorName
InvalidProjectionParameter_
  InvalidTypeSort                                            {} -> ErrorName
InvalidTypeSort_
  LambdaIsErased                                             {} -> ErrorName
LambdaIsErased_
  LibTooFarDown                                              {} -> ErrorName
LibTooFarDown_
  LiteralTooBig                                              {} -> ErrorName
LiteralTooBig_
  MacroResultTypeMismatch                                    {} -> ErrorName
MacroResultTypeMismatch_
  MetaCannotDependOn                                         {} -> ErrorName
MetaCannotDependOn_
  MetaErasedSolution                                         {} -> ErrorName
MetaErasedSolution_
  MetaIrrelevantSolution                                     {} -> ErrorName
MetaIrrelevantSolution_
  MismatchedProjectionsError                                 {} -> ErrorName
MismatchedProjectionsError_
  ModuleArityMismatch                                        {} -> ErrorName
ModuleArityMismatch_
  ModuleDefinedInOtherFile                                   {} -> ErrorName
ModuleDefinedInOtherFile_
  ModuleNameDoesntMatchFileName                              {} -> ErrorName
ModuleNameDoesntMatchFileName_
  ModuleNameHashCollision                                    {} -> ErrorName
ModuleNameHashCollision_
  ModuleNameUnexpected                                       {} -> ErrorName
ModuleNameUnexpected_
  MultipleFixityDecls                                        {} -> ErrorName
MultipleFixityDecls_
  MultiplePolarityPragmas                                    {} -> ErrorName
MultiplePolarityPragmas_
  ExplicitPolarityVsPragma                                   {} -> ErrorName
ExplicitPolarityVsPragma_
  NamedWhereModuleInRefinedContext                           {} -> ErrorName
NamedWhereModuleInRefinedContext_
  NeedOptionAllowExec                                        {} -> ErrorName
NeedOptionAllowExec_
  NeedOptionCopatterns                                       {} -> ErrorName
NeedOptionCopatterns_
  NeedOptionCubical                                          {} -> ErrorName
NeedOptionCubical_
  NeedOptionPatternMatching                                  {} -> ErrorName
NeedOptionPatternMatching_
  NeedOptionProp                                             {} -> ErrorName
NeedOptionProp_
  NeedOptionRewriting                                        {} -> ErrorName
NeedOptionRewriting_
  NeedOptionSizedTypes                                       {} -> ErrorName
NeedOptionSizedTypes_
  NeedOptionTwoLevel                                         {} -> ErrorName
NeedOptionTwoLevel_
  NeedOptionUniversePolymorphism                             {} -> ErrorName
NeedOptionUniversePolymorphism_
  NegativeLiteralInPattern                                   {} -> ErrorName
NegativeLiteralInPattern_
  NoBindingForBuiltin                                        {} -> ErrorName
NoBindingForBuiltin_
  NoBindingForPrimitive                                      {} -> ErrorName
NoBindingForPrimitive_
  NoKnownRecordWithSuchFields                                {} -> ErrorName
NoKnownRecordWithSuchFields_
  NoParameterOfName                                          {} -> ErrorName
NoParameterOfName_
  NoParseForApplication                                      {} -> ErrorName
NoParseForApplication_
  NoParseForLHS                                              {} -> ErrorName
NoParseForLHS_
  NoSuchBuiltinName                                          {} -> ErrorName
NoSuchBuiltinName_
  NoSuchModule                                               {} -> ErrorName
NoSuchModule_
  NoSuchPrimitiveFunction                                    {} -> ErrorName
NoSuchPrimitiveFunction_
  NotAnExpression                                            {} -> ErrorName
NotAnExpression_
  NotInScope                                                 {} -> ErrorName
NotInScope_
  NotLeqSort                                                 {} -> ErrorName
NotLeqSort_
  NotValidBeforeField                                        {} -> ErrorName
NotValidBeforeField_
  OpenEverythingInRecordWhere                                {} -> ErrorName
OpenEverythingInRecordWhere_
  OverlappingProjects                                        {} -> ErrorName
OverlappingProjects_
  PatternInPathLambda                                        {} -> ErrorName
PatternInPathLambda_
  PatternInSystem                                            {} -> ErrorName
PatternInSystem_
  PostulatedSizeInModule                                     {} -> ErrorName
PostulatedSizeInModule_
  PrivateRecordField                                         {} -> ErrorName
PrivateRecordField_
  ProjectionIsIrrelevant                                     {} -> ErrorName
ProjectionIsIrrelevant_
  QualifiedLocalModule                                       {} -> ErrorName
QualifiedLocalModule_
  QuantityMismatch                                           {} -> ErrorName
QuantityMismatch_
  RecordIsErased                                             {} -> ErrorName
RecordIsErased_
  RecursiveRecordNeedsInductivity                            {} -> ErrorName
RecursiveRecordNeedsInductivity_
  ReferencesFutureVariables                                  {} -> ErrorName
ReferencesFutureVariables_
  RelevanceMismatch                                          {} -> ErrorName
RelevanceMismatch_
  RepeatedNamesInImportDirective                             {} -> ErrorName
RepeatedNamesInImportDirective_
  RepeatedVariablesInPattern                                 {} -> ErrorName
RepeatedVariablesInPattern_
  ShadowedModule                                             {} -> ErrorName
ShadowedModule_
  ShouldBeASort                                              {} -> ErrorName
ShouldBeASort_
  ShouldBeEmpty                                              {} -> ErrorName
ShouldBeEmpty_
  ShouldBePath                                               {} -> ErrorName
ShouldBePath_
  ShouldBePi                                                 {} -> ErrorName
ShouldBePi_
  ShouldBeRecordPattern                                      {} -> ErrorName
ShouldBeRecordPattern_
  ShouldBeRecordType                                         {} -> ErrorName
ShouldBeRecordType_
  ShouldEndInApplicationOfTheDatatype                        {} -> ErrorName
ShouldEndInApplicationOfTheDatatype_
  SolvedButOpenHoles                                         {} -> ErrorName
SolvedButOpenHoles_
  SortCannotDependOnItsIndex                                 {} -> ErrorName
SortCannotDependOnItsIndex_
  SortDoesNotAdmitDataDefinitions                            {} -> ErrorName
SortDoesNotAdmitDataDefinitions_
  SortOfSplitVarError                                        {} -> ErrorName
SortOfSplitVarError_
  SplitInProp                                                {} -> ErrorName
SplitInProp_
  SplitOnAbstract                                            {} -> ErrorName
SplitOnAbstract_
  SplitOnCoinductive                                         {} -> ErrorName
SplitOnCoinductive_
  SplitOnIrrelevant                                          {} -> ErrorName
SplitOnIrrelevant_
  SplitOnNonEtaRecord                                        {} -> ErrorName
SplitOnNonEtaRecord_
  SplitOnNonVariable                                         {} -> ErrorName
SplitOnNonVariable_
  SplitOnPartial                                             {} -> ErrorName
SplitOnPartial_
  SplitOnUnchecked                                           {} -> ErrorName
SplitOnUnchecked_
  SplitOnUnusableCohesion                                    {} -> ErrorName
SplitOnUnusableCohesion_
  SplitOnUnusablePolarity                                    {} -> ErrorName
SplitOnUnusablePolarity_
  TacticAttributeNotAllowed                                  {} -> ErrorName
TacticAttributeNotAllowed_
  TooFewArgumentsToPatternSynonym                            {} -> ErrorName
TooFewArgumentsToPatternSynonym_
  TooFewPatternsInWithClause                                 {} -> ErrorName
TooFewPatternsInWithClause_
  TooManyFields                                              {} -> ErrorName
TooManyFields_
  TooManyPatternsInWithClause                                {} -> ErrorName
TooManyPatternsInWithClause_
  TooManyPolarities                                          {} -> ErrorName
TooManyPolarities_
  TriedToCopyConstrainedPrim                                 {} -> ErrorName
TriedToCopyConstrainedPrim_
  InvalidInstanceHeadType                                    {} -> ErrorName
InvalidInstanceHeadType_
  UnboundVariablesInPatternSynonym                           {} -> ErrorName
UnboundVariablesInPatternSynonym_
  UnequalCohesion                                            {} -> ErrorName
UnequalCohesion_
  UnequalFiniteness                                          {} -> ErrorName
UnequalFiniteness_
  UnequalHiding                                              {} -> ErrorName
UnequalHiding_
  UnequalLevel                                               {} -> ErrorName
UnequalLevel_
  UnequalQuantity                                            {} -> ErrorName
UnequalQuantity_
  UnequalRelevance                                           {} -> ErrorName
UnequalRelevance_
  UnequalPolarity                                            {} -> ErrorName
UnequalPolarity_
  UnequalSorts                                               {} -> ErrorName
UnequalSorts_
  UnequalTerms                                               {} -> ErrorName
UnequalTerms_
  UnexpectedModalityAnnotationInParameter                    {} -> ErrorName
UnexpectedModalityAnnotationInParameter_
  UnexpectedParameter                                        {} -> ErrorName
UnexpectedParameter_
  UnexpectedTypeSignatureForParameter                        {} -> ErrorName
UnexpectedTypeSignatureForParameter_
  UnexpectedWithPatterns                                     {} -> ErrorName
UnexpectedWithPatterns_
  UnknownBackend                                             {} -> ErrorName
UnknownBackend_
  UnusableAtModality                                         {} -> ErrorName
UnusableAtModality_
  UnusedVariableInPatternSynonym                             {} -> ErrorName
UnusedVariableInPatternSynonym_
  VariableIsErased                                           {} -> ErrorName
VariableIsErased_
  VariableIsIrrelevant                                       {} -> ErrorName
VariableIsIrrelevant_
  VariableIsOfUnusableCohesion                               {} -> ErrorName
VariableIsOfUnusableCohesion_
  VariableIsOfUnusablePolarity                               {} -> ErrorName
VariableIsOfUnusablePolarity_
  WithClausePatternMismatch                                  {} -> ErrorName
WithClausePatternMismatch_
  WithOnFreeVariable                                         {} -> ErrorName
WithOnFreeVariable_
  WrongAnnotationInLambda                                    {} -> ErrorName
WrongAnnotationInLambda_
  WrongArgInfoForPrimitive                                   {} -> ErrorName
WrongArgInfoForPrimitive_
  WrongCohesionInLambda                                      {} -> ErrorName
WrongCohesionInLambda_
  WrongPolarityInLambda                                      {} -> ErrorName
WrongPolarityInLambda_
  WrongHidingInApplication                                   {} -> ErrorName
WrongHidingInApplication_
  WrongHidingInLHS                                           {} -> ErrorName
WrongHidingInLHS_
  WrongHidingInLambda                                        {} -> ErrorName
WrongHidingInLambda_
  WrongHidingInProjection                                    {} -> ErrorName
WrongHidingInProjection_
  WrongIrrelevanceInLambda                                   {} -> ErrorName
WrongIrrelevanceInLambda_
  WrongNamedArgument                                         {} -> ErrorName
WrongNamedArgument_
  WrongNumberOfConstructorArguments                          {} -> ErrorName
WrongNumberOfConstructorArguments_
  WrongQuantityInLambda                                      {} -> ErrorName
WrongQuantityInLambda_
  WrongSharpArity                                            {} -> ErrorName
WrongSharpArity_

declarationExceptionName :: DeclarationException' -> DeclarationException_
declarationExceptionName :: DeclarationException' -> DeclarationException_
declarationExceptionName = \case
  N.AmbiguousConstructor           {} -> DeclarationException_
AmbiguousConstructorN_
  AmbiguousFunClauses              {} -> DeclarationException_
AmbiguousFunClauses_
  BadMacroDef                      {} -> DeclarationException_
BadMacroDef_
  DisallowedInterleavedMutual      {} -> DeclarationException_
DisallowedInterleavedMutual_
  DuplicateAnonDeclaration         {} -> DeclarationException_
DuplicateAnonDeclaration_
  DuplicateDefinition              {} -> DeclarationException_
DuplicateDefinition_
  InvalidMeasureMutual             {} -> DeclarationException_
InvalidMeasureMutual_
  MissingWithClauses               {} -> DeclarationException_
MissingWithClauses_
  MultipleEllipses                 {} -> DeclarationException_
MultipleEllipses_
  OpaqueInMutual                   {} -> DeclarationException_
OpaqueInMutual_
  UnfoldingOutsideOpaque           {} -> DeclarationException_
UnfoldingOutsideOpaque_
  UnquoteDefRequiresSignature      {} -> DeclarationException_
UnquoteDefRequiresSignature_
  WrongContentBlock                {} -> DeclarationException_
WrongContentBlock_
  WrongDefinition                  {} -> DeclarationException_
WrongDefinition_

execErrorName :: ExecError -> ExecError_
execErrorName :: ExecError -> ExecError_
execErrorName = \case
  ExeNotTrusted    {} -> ExecError_
ExeNotTrusted_
  ExeNotFound      {} -> ExecError_
ExeNotFound_
  ExeNotExecutable {} -> ExecError_
ExeNotExecutable_

ghcBackendErrorName :: GHCBackendError -> GHCBackendError_
ghcBackendErrorName :: GHCBackendError -> GHCBackendError_
ghcBackendErrorName = \case
  ConstructorCountMismatch{} -> GHCBackendError_
ConstructorCountMismatch_
  NotAHaskellType Term
_ WhyNotAHaskellType
err      -> NotAHaskellType_ -> GHCBackendError_
NotAHaskellType_ (NotAHaskellType_ -> GHCBackendError_)
-> NotAHaskellType_ -> GHCBackendError_
forall a b. (a -> b) -> a -> b
$ WhyNotAHaskellType -> NotAHaskellType_
notAHaskellTypeErrorName WhyNotAHaskellType
err
  WrongTypeOfMain{}          -> GHCBackendError_
WrongTypeOfMain_

jsBackendErrorName :: JSBackendError -> JSBackendError_
jsBackendErrorName :: JSBackendError -> JSBackendError_
jsBackendErrorName = \case
  JSBackendError
BadCompilePragma -> JSBackendError_
BadCompilePragma_

impossibleConstructorErrorName :: NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName :: NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName = \case
  UnifyConflict {} -> NegativeUnification_
UnifyConflict_
  UnifyCycle    {} -> NegativeUnification_
UnifyCycle_

interactionErrorName :: InteractionError -> InteractionError_
interactionErrorName :: InteractionError -> InteractionError_
interactionErrorName = \case
  CaseSplitError{}              -> InteractionError_
CaseSplitError_
  CannotRefine{}                -> InteractionError_
CannotRefine_
  ExpectedIdentifier{}          -> InteractionError_
ExpectedIdentifier_
  ExpectedApplication{}         -> InteractionError_
ExpectedApplication_
  NoActionForInteractionPoint{} -> InteractionError_
NoActionForInteractionPoint_
  NoSuchInteractionPoint{}      -> InteractionError_
NoSuchInteractionPoint_
  UnexpectedWhere{}             -> InteractionError_
UnexpectedWhere_

missingTypeSignatureInfoName :: MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName :: MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName = \case
  MissingDataSignature      {} -> DataRecOrFun_
DataName_
  MissingRecordSignature    {} -> DataRecOrFun_
RecName_
  MissingFunctionSignature  {} -> DataRecOrFun_
FunName_

notAHaskellTypeErrorName :: WhyNotAHaskellType -> NotAHaskellType_
notAHaskellTypeErrorName :: WhyNotAHaskellType -> NotAHaskellType_
notAHaskellTypeErrorName = \case
  BadDontCare               {} -> NotAHaskellType_
BadDontCare_
  BadLambda                 {} -> NotAHaskellType_
BadLambda_
  BadMeta                   {} -> NotAHaskellType_
BadMeta_
  NoPragmaFor               {} -> NotAHaskellType_
NoPragmaFor_
  NotCompiled               {} -> NotAHaskellType_
NotCompiled_
  WrongPragmaFor            {} -> NotAHaskellType_
WrongPragmaFor_

splitErrorName :: SplitError -> SplitError_
splitErrorName :: SplitError -> SplitError_
splitErrorName = \case
  ErasedDatatype ErasedDatatypeReason
reason Closure Type
_      -> ErasedDatatypeReason -> SplitError_
ErasedDatatype_ ErasedDatatypeReason
reason
  GenericSplitError         {} -> SplitError_
GenericSplitError_
  -- Specific errors
  BlockedType               {} -> SplitError_
BlockedType_
  CannotCreateMissingClause {} -> SplitError_
CannotCreateMissingClause_
  CoinductiveDatatype       {} -> SplitError_
CoinductiveDatatype_
  CosplitCatchall           {} -> SplitError_
CosplitCatchall_
  CosplitNoRecordType       {} -> SplitError_
CosplitNoRecordType_
  CosplitNoTarget           {} -> SplitError_
CosplitNoTarget_
  NotADatatype              {} -> SplitError_
NotADatatype_
  UnificationStuck          {} -> SplitError_
UnificationStuck_

unquotableName :: CannotQuote -> CannotQuote_
unquotableName :: CannotQuote -> CannotQuote_
unquotableName = \case
  CannotQuoteAmbiguous         {} -> CannotQuote_
CannotQuoteAmbiguous_
  CannotQuoteExpression        {} -> CannotQuote_
CannotQuoteExpression_
  CannotQuoteHidden            {} -> CannotQuote_
CannotQuoteHidden_
  CannotQuoteNothing           {} -> CannotQuote_
CannotQuoteNothing_
  CannotQuotePattern           {} -> CannotQuote_
CannotQuotePattern_

unquoteErrorName :: UnquoteError -> UnquoteError_
unquoteErrorName :: UnquoteError -> UnquoteError_
unquoteErrorName = \case
  BlockedOnMeta               {} -> UnquoteError_
BlockedOnMeta_
  CannotDeclareHiddenFunction {} -> UnquoteError_
CannotDeclareHiddenFunction_
  CommitAfterDef              {} -> UnquoteError_
CommitAfterDef_
  ConInsteadOfDef             {} -> UnquoteError_
ConInsteadOfDef_
  DefineDataNotData           {} -> UnquoteError_
DefineDataNotData_
  DefInsteadOfCon             {} -> UnquoteError_
DefInsteadOfCon_
  MissingDeclaration          {} -> UnquoteError_
MissingDeclaration_
  MissingDefinition           {} -> UnquoteError_
MissingDefinition_
  NakedUnquote                {} -> UnquoteError_
NakedUnquote_
  NonCanonical                {} -> UnquoteError_
NonCanonical_
  PatLamWithoutClauses        {} -> UnquoteError_
PatLamWithoutClauses_
  StaleMeta                   {} -> UnquoteError_
StaleMeta_
  TooManyParameters           {} -> UnquoteError_
TooManyParameters_
  UnboundName                 {} -> UnquoteError_
UnboundName_

-- -- * Printing names of errors

-- -- The following might not be used yet:

-- ghcBackendErrorString :: GHCBackendError -> String
-- ghcBackendErrorString = ghcBackendErrorNameString . ghcBackendErrorName

-- interactionErrorString :: InteractionError -> String
-- interactionErrorString = interactionErrorNameString . interactionErrorName

-- splitErrorString :: SplitError -> String
-- splitErrorString = splitErrorNameString . splitErrorName

-- unquoteErrorString :: UnquoteError -> String
-- unquoteErrorString = unquoteErrorNameString . unquoteErrorName