    -- | 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_
      BothWithAndRHS                                             {} -> ErrorName
    BothWithAndRHS_
      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_
      CubicalNotErasure                                          {} -> ErrorName
    CubicalNotErasure_
      CubicalPrimitiveNotFullyApplied                            {} -> ErrorName
    CubicalPrimitiveNotFullyApplied_
      CyclicModuleDependency                                     {} -> ErrorName
    CyclicModuleDependency_
      DatatypeIndexPolarity                                      {} -> ErrorName
    DatatypeIndexPolarity_
      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_
      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_
      OverlappingProjects                                        {} -> ErrorName
    OverlappingProjects_
      PathAbstractionFailed                                      {} -> ErrorName
    PathAbstractionFailed_
      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_
      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_
      CannotGive{}                  -> InteractionError_
    CannotGive_
      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