content: 
  -- | Generates data used for precise syntax highlighting.
  
  -- {-# OPTIONS_GHC -fwarn-unused-imports #-}  -- Semigroup import obsolete in later ghcs
  -- {-# OPTIONS_GHC -fwarn-unused-binds   #-}
  
  module Agda.Interaction.Highlighting.Generate
    ( Level(..)
    , generateAndPrintSyntaxInfo
    , generateTokenInfo, generateTokenInfoFromSource
    , generateTokenInfoFromString
    , printSyntaxInfo
    , printErrorInfo, errorHighlighting
    , printUnsolvedInfo
    , printHighlightingInfo
    , highlightAsTypeChecked
    , highlightWarning, warningHighlighting
    , computeUnsolvedInfo
    , storeDisambiguatedConstructor, storeDisambiguatedProjection
    , disambiguateRecordFields
    ) where
  
  import Prelude hiding (null)
  
  import Control.Monad
  
  import qualified Data.Foldable as Fold
  import qualified Data.Map as Map
  import Data.Maybe
  import Data.List ((\\))
  import qualified Data.List as List
  import qualified Data.IntMap as IntMap
  import Data.HashMap.Strict (HashMap)
  import qualified Data.HashMap.Strict as HMap
  import Data.Semigroup (sconcat)
  import Data.Sequence (Seq)
  import qualified Data.Set as Set
  import qualified Data.Text.Lazy as Text
  
  import Agda.Interaction.Response
    ( RemoveTokenBasedHighlighting( KeepHighlighting ) )
  import Agda.Interaction.Highlighting.Precise as H
  import Agda.Interaction.Highlighting.Range
    (rToR, rangeToRange, overlappings, Ranges)
  import Agda.Interaction.Highlighting.FromAbstract
  
  import qualified Agda.TypeChecking.Errors as TCM
  import Agda.TypeChecking.MetaVars (isBlockedTerm, hasTwinMeta)
  import Agda.TypeChecking.Monad
    hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
  import qualified Agda.TypeChecking.Monad  as TCM
  import qualified Agda.TypeChecking.Monad.Base.Warning as W
  import qualified Agda.TypeChecking.Pretty as TCM
  import Agda.TypeChecking.Positivity.Occurrence
  import Agda.TypeChecking.Warnings ( raiseWarningsOnUsage )
  
  import qualified Agda.Syntax.Abstract as A
  import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..), DeclarationWarning'(..) )
  import Agda.Syntax.Common (Induction(..), pattern Ranged)
  import qualified Agda.Syntax.Common.Aspect as Aspect
  import qualified Agda.Syntax.Concrete.Name as C
  import qualified Agda.Syntax.Internal as I
  import qualified Agda.Syntax.Literal as L
  import qualified Agda.Syntax.Parser as Pa
  import qualified Agda.Syntax.Parser.Tokens as T
  import qualified Agda.Syntax.Position as P
  import Agda.Syntax.Position
    (RangeFile, Range, HasRange, getRange, noRange)
  import Agda.Syntax.TopLevelModuleName
  
  import Agda.Syntax.Scope.Base     ( WithKind(..) )
  import Agda.Syntax.Abstract.Views ( KName, declaredNames )
  
  import Agda.Utils.FileName
  import Agda.Utils.List            ( caseList, last1 )
  import Agda.Utils.List1           ( List1 )
  import qualified Agda.Utils.List1 as List1
  import Agda.Utils.List2           ( List2 )
  import qualified Agda.Utils.List2 as List2
  import Agda.Utils.Maybe
  import qualified Agda.Utils.Maybe.Strict as Strict
  import Agda.Utils.Null
  import Agda.Syntax.Common.Pretty
  import Agda.Utils.Singleton
  
  import Agda.Utils.Impossible
  
  -- | Highlighting levels.
  
  data Level
    = Full
      -- ^ Full highlighting. Should only be used after typechecking has
      --   completed successfully.
    | Partial
      -- ^ Highlighting without disambiguation of overloaded
      --   constructors.
  
  -- | Highlight a warning.
  --   We do not generate highlighting for unsolved metas and
  --   constraints, as that gets handled in bulk after typechecking.
  highlightWarning :: TCWarning -> TCM ()
  highlightWarning tcwarn = do
    let h = convert $ warningHighlighting' False tcwarn
    -- Highlighting for warnings coming from the Happy parser is placed
    -- together with token highlighting.
    case tcWarning tcwarn of
      ParseWarning{} -> modifyTCLens stTokens     (h <>)
      _              -> modifyTCLens stSyntaxInfo (h <>)
    ifTopLevelAndHighlightingLevelIs NonInteractive $
      printHighlightingInfo KeepHighlighting h
  
  -- | Generate syntax highlighting information for the given
  -- declaration, and (if appropriate) print it. If the boolean is
  -- 'True', then the state is additionally updated with the new
  -- highlighting info (in case of a conflict new info takes precedence
  -- over old info).
  --
  -- The procedure makes use of some of the highlighting info
  -- corresponding to 'stTokens' (that corresponding to the interval
  -- covered by the declaration). If the boolean is 'True', then this
  -- highlighting info is additionally removed from the data structure
  -- that 'stTokens' refers to.
  
  generateAndPrintSyntaxInfo
    :: A.Declaration
         -- ^ Declaration to highlight.
    -> Level
         -- ^ Amount of highlighting.
    -> Bool
         -- ^ Update the state?
    -> TCM ()
  generateAndPrintSyntaxInfo decl _ _ | null $ getRange decl = return ()
  generateAndPrintSyntaxInfo decl hlLevel updateState = do
    top <- fromMaybe __IMPOSSIBLE__ <$> currentTopLevelModule
  
    reportSDoc "import.iface.create" 15 $
      TCM.fwords
        ("Generating syntax info for the following declaration " ++
         case hlLevel of
           Full   {} -> "(final):"
           Partial{} -> "(first approximation):")
        TCM.$$
      TCM.prettyA decl
  
    ignoreAbstractMode $ do
      kinds <- nameKinds hlLevel decl
  
      -- After the code has been type checked more information may be
      -- available for overloaded constructors, and
      -- @generateConstructorInfo@ takes advantage of this information.
      -- Note, however, that highlighting for overloaded constructors is
      -- included also in @nameInfo@.
      constructorInfo <- case hlLevel of
        Full{} -> generateConstructorInfo top kinds decl
        _      -> return mempty
  
      -- Main source of scope-checker generated highlighting:
      let nameInfo = runHighlighter top kinds decl
  
      reportSDoc "highlighting.warning" 60 $ TCM.hcat
        [ "current path = "
        , Strict.maybe "(nothing)" (return . pretty) =<< do
            P.rangeFile <$> viewTC eRange
        ]
  
      -- Highlighting from the lexer and Happy parser:
      (curTokens, otherTokens) <-
        insideAndOutside (rangeToRange (getRange decl)) <$> useTC stTokens
  
      -- @constructorInfo@ needs
      -- to be placed before @nameInfo@ since, when typechecking is done,
      -- constructors are included in both lists. Finally the token
      -- information is placed last since token highlighting is more
      -- crude than the others.
      let syntaxInfo = convert (constructorInfo <> nameInfo)
                         <>
                       curTokens
  
      when updateState $ do
        stSyntaxInfo `modifyTCLens` mappend syntaxInfo
        stTokens     `setTCLens`    otherTokens
  
      ifTopLevelAndHighlightingLevelIs NonInteractive $
        printHighlightingInfo KeepHighlighting syntaxInfo
  
  -- | Generate and return the syntax highlighting information for the
  -- tokens in the given file.
  
  generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo
  generateTokenInfo file =
    generateTokenInfoFromSource rf . Text.unpack =<<
      runPM (Pa.readFilePM rf)
    where
    -- Note the use of Nothing here. The file might not even parse, but
    -- it should still be possible to obtain token-based highlighting
    -- information. The top-level module names seem to be *mostly*
    -- unused, but one cannot use __IMPOSSIBLE__ instead of Nothing,
    -- because the top-level module names are used by interleaveRanges,
    -- which is used by parseLiterateWithComments, which is used by
    -- generateTokenInfoFromSource.
    rf = P.mkRangeFile file Nothing
  
  -- | Generate and return the syntax highlighting information for the
  -- tokens in the given file.
  
  generateTokenInfoFromSource
    :: RangeFile
       -- ^ The module to highlight.
    -> String
       -- ^ The file contents. Note that the file is /not/ read from
       -- disk.
    -> TCM HighlightingInfo
  generateTokenInfoFromSource file input =
    runPM $ tokenHighlighting . fst . fst <$>
            Pa.parseFile Pa.tokensParser file input
  
  -- | Generate and return the syntax highlighting information for the
  -- tokens in the given string, which is assumed to correspond to the
  -- given range.
  
  generateTokenInfoFromString :: Range -> String -> TCM HighlightingInfo
  generateTokenInfoFromString r _ | r == noRange = return mempty
  generateTokenInfoFromString r s = do
    runPM $ tokenHighlighting . fst <$>
            Pa.parsePosString Pa.tokensParser p s
    where
      Just p = P.rStart r
  
  -- | Compute syntax highlighting for the given tokens.
  tokenHighlighting :: [T.Token] -> HighlightingInfo
  tokenHighlighting = convert . mconcat . map tokenToHI
    where
    -- Converts an aspect and a range to a file.
    aToF a r = H.singleton (rToR r) (mempty { aspect = Just a })
  
    tokenToHI :: T.Token -> HighlightingInfoBuilder
    tokenToHI (T.TokKeyword T.KwForall i)  = aToF Symbol (getRange i)
    tokenToHI (T.TokKeyword T.KwREWRITE _) = mempty  -- #4361, REWRITE is not always a Keyword
    tokenToHI (T.TokKeyword _ i)           = aToF Keyword (getRange i)
    tokenToHI (T.TokSymbol T.SymQuestionMark i) = aToF Hole (getRange i)
    tokenToHI (T.TokSymbol  _ i)                = aToF Symbol (getRange i)
    tokenToHI (T.TokLiteral (Ranged r (L.LitNat    _))) = aToF Number r
    tokenToHI (T.TokLiteral (Ranged r (L.LitWord64 _))) = aToF Number r
    tokenToHI (T.TokLiteral (Ranged r (L.LitFloat  _))) = aToF Number r
    tokenToHI (T.TokLiteral (Ranged r (L.LitString _))) = aToF String r
    tokenToHI (T.TokLiteral (Ranged r (L.LitChar   _))) = aToF String r
    tokenToHI (T.TokLiteral (Ranged r (L.LitQName  _))) = aToF String r
    tokenToHI (T.TokLiteral (Ranged r (L.LitMeta _ _))) = aToF String r
    tokenToHI (T.TokComment (i, _))            = aToF Comment (getRange i)
    tokenToHI (T.TokTeX (i, _))                = aToF Background (getRange i)
    tokenToHI (T.TokMarkup (i, _))             = aToF Markup (getRange i)
    tokenToHI (T.TokId {})                     = mempty
    tokenToHI (T.TokQId {})                    = mempty
    tokenToHI (T.TokString (i,s))              = aToF Pragma (getRange i)
    tokenToHI (T.TokDummy {})                  = mempty
    tokenToHI (T.TokEOF {})                    = mempty
  
  -- | Builds a 'NameKinds' function.
  
  nameKinds :: Level
               -- ^ This should only be @'Full'@ if
               -- type-checking completed successfully (without any
               -- errors).
            -> A.Declaration
            -> TCM NameKinds
  nameKinds hlLevel decl = do
    imported <- useTC $ stImports . sigDefinitions
    local    <- case hlLevel of
      Full{} -> useTC $ stSignature . sigDefinitions
      _      -> return HMap.empty
    impPatSyns <- useTC stPatternSynImports
    locPatSyns <- case hlLevel of
      Full{} -> useTC stPatternSyns
      _      -> return empty
        -- Traverses the syntax tree and constructs a map from qualified
        -- names to name kinds. TODO: Handle open public.
    let syntax :: NameKindMap
        syntax = runBuilder (declaredNames decl :: NameKindBuilder) HMap.empty
    return $ \ n -> unionsMaybeWith mergeNameKind
      [ TCM.defnToNameKind . theDef <$> HMap.lookup n local
      , con <$ Map.lookup n locPatSyns
      , TCM.defnToNameKind . theDef <$> HMap.lookup n imported
      , con <$ Map.lookup n impPatSyns
      , HMap.lookup n syntax
      ]
    where
  
    con :: NameKind
    con = Constructor Inductive
  
  -- | The 'TCM.Axiom' constructor is used to represent various things
  -- which are not really axioms, so when maps are merged 'Postulate's
  -- are thrown away whenever possible. The 'declaredNames' function
  -- below can return several explanations for one qualified name; the
  -- 'Postulate's are bogus.
  mergeNameKind :: NameKind -> NameKind -> NameKind
  mergeNameKind Postulate k = k
  mergeNameKind _     Macro = Macro  -- If the abstract syntax says macro, it's a macro.
  mergeNameKind k         _ = k
  
  -- Auxiliary types for @nameKinds@ generation
  
  type NameKindMap     = HashMap A.QName NameKind
  data NameKindBuilder = NameKindBuilder
    { runBuilder :: NameKindMap -> NameKindMap
    }
  
  instance Semigroup (NameKindBuilder) where
    NameKindBuilder f <> NameKindBuilder g = NameKindBuilder $ f . g
  
  instance Monoid (NameKindBuilder) where
    mempty = NameKindBuilder id
    mappend = (<>)
  
  instance Singleton KName NameKindBuilder where
    singleton (WithKind k q) = NameKindBuilder $
      HMap.insertWith mergeNameKind q $ kindOfNameToNameKind k
  
  instance Collection KName NameKindBuilder
  
  -- | Generates syntax highlighting information for all constructors
  -- occurring in patterns and expressions in the given declaration.
  --
  -- This function should only be called after type checking.
  -- Constructors can be overloaded, and the overloading is resolved by
  -- the type checker.
  
  generateConstructorInfo
    :: TopLevelModuleName
       -- ^ The module to highlight.
    -> NameKinds
    -> A.Declaration
    -> TCM HighlightingInfoBuilder
  generateConstructorInfo top kinds decl = do
  
    -- Get boundaries of current declaration.
    -- @noRange@ should be impossible, but in case of @noRange@
    -- it makes sense to return mempty.
    caseList (P.rangeIntervals $ getRange decl)
             (return mempty) $ \ i is -> do
      let start = fromIntegral $ P.posPos $ P.iStart i
          end   = fromIntegral $ P.posPos $ P.iEnd $ last1 i is
  
      -- Get all disambiguated names that fall within the range of decl.
      m0 <- useTC stDisambiguatedNames
      let (_, m1) = IntMap.split (pred start) m0
          (m2, _) = IntMap.split end m1
          constrs = IntMap.elems m2
  
      -- Return suitable syntax highlighting information.
      return $ foldMap (runHighlighter top kinds) constrs
  
  printSyntaxInfo :: Range -> TCM ()
  printSyntaxInfo r = do
    syntaxInfo <- useTC stSyntaxInfo
    ifTopLevelAndHighlightingLevelIs NonInteractive $
      printHighlightingInfo KeepHighlighting
        (restrictTo (rangeToRange r) syntaxInfo)
  
  -- | Prints syntax highlighting info for an error.
  
  printErrorInfo :: TCErr -> TCM ()
  printErrorInfo e =
    printHighlightingInfo KeepHighlighting . convert =<<
      errorHighlighting e
  
  -- | Generate highlighting for error.
  
  errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
  errorHighlighting e = errorHighlighting' (getRange e) <$> TCM.renderError e
  
  errorHighlighting'
    :: Range     -- ^ Error range.
    -> String    -- ^ Error message for tooltip.
    -> HighlightingInfoBuilder
  errorHighlighting' r s = mconcat
    [ -- Erase previous highlighting.
      H.singleton (rToR $ P.continuousPerLine r) mempty
    , -- Print new highlighting.
      H.singleton (rToR r)
           $ parserBased { otherAspects = Set.singleton Error
                         , note         = s
                         }
    ]
  
  -- | Highlighting for warnings that are considered fatal.
  
  errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
  errorWarningHighlighting w =
    H.singleton (rToR $ P.continuousPerLine $ getRange w) $
      parserBased { otherAspects = Set.singleton ErrorWarning }
  -- errorWarningHighlighting w = errorHighlighting' (getRange w) ""
    -- MonadPretty not available here, so, no tooltip.
    -- errorHighlighting' (getRange w) . render <$> TCM.prettyWarning (tcWarning w)
  
  -- | Generate syntax highlighting for warnings.
  
  warningHighlighting :: TCWarning -> HighlightingInfoBuilder
  warningHighlighting = warningHighlighting' True
  
  warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
                       -> TCWarning -> HighlightingInfoBuilder
  warningHighlighting' b w = case tcWarning w of
    TerminationIssue terrs     -> terminationErrorHighlighting terrs
    NotStrictlyPositive d ocs  -> positivityErrorHighlighting d ocs
    ConstructorDoesNotFitInData _dataOrRecord c _s1 _s2 _err -> errorWarningHighlighting $
       getRange c `catchNull` getRange w
    CoinductiveEtaRecord _x    -> deadcodeHighlighting w
    -- #3965 highlight each unreachable clause independently: they
    -- may be interleaved with actually reachable clauses!
    UnreachableClauses _ rs    -> foldMap deadcodeHighlighting rs
    CoverageIssue{}            -> coverageErrorHighlighting $ getRange w
    CoverageNoExactSplit{}     -> catchallHighlighting $ getRange w
    InlineNoExactSplit{}       -> catchallHighlighting $ getRange w
    UnsolvedConstraints cs     -> if b then constraintsHighlighting [] $ Fold.toList cs else mempty
    UnsolvedMetaVariables rs   -> if b then metasHighlighting          $ Fold.toList rs else mempty
    AbsurdPatternRequiresAbsentRHS{} -> deadcodeHighlighting w
    DuplicateRecordDirective{}   -> deadcodeHighlighting w
    ModuleDoesntExport _ _ _ xs  -> foldMap deadcodeHighlighting xs
    DuplicateUsing xs            -> foldMap deadcodeHighlighting xs
    FixityInRenamingModule rs    -> foldMap deadcodeHighlighting rs
    -- expanded catch-all case to get a warning for new constructors
    CantGeneralizeOverSorts{}  -> mempty
    UnsolvedInteractionMetas{} -> mempty
    InteractionMetaBoundaries{} -> mempty
    OldBuiltin{}                -> deadcodeHighlighting w
    BuiltinDeclaresIdentifier{} -> mempty
    EmptyRewritePragma{}       -> deadcodeHighlighting w
    EmptyWhere{}               -> deadcodeHighlighting w
    -- TODO: linearity
    -- FixingQuantity _ q _       -> if null r then cosmeticHighlighting w else deadcodeHighlighting r
    --   where r = getRange q
    FixingRelevance _ q _      -> if null r then cosmeticProblemHighlighting w else deadcodeHighlighting r
      where r = getRange q
    FixingCohesion _ q _       -> if null r then cosmeticProblemHighlighting w else deadcodeHighlighting r
      where r = getRange q
    FixingPolarity _ q _       -> if null r then cosmeticProblemHighlighting w else deadcodeHighlighting r
      where r = getRange q
    IllformedAsClause{}        -> deadcodeHighlighting w
    UselessPragma r _          -> deadcodeHighlighting r
    UselessPublic{}            -> deadcodeHighlighting w
    UselessHiding xs           -> foldMap deadcodeHighlighting xs
    UselessInline{}            -> mempty
    UselessPatternDeclarationForRecord{} -> deadcodeHighlighting w
    UselessTactic{}            -> deadcodeHighlighting w
    ClashesViaRenaming _ xs    -> foldMap deadcodeHighlighting xs
      -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
      -- Should we have a different color?
    WrongInstanceDeclaration{}   -> instanceProblemHighlighting w
    InstanceWithExplicitArg{}    -> instanceProblemHighlighting w
    InstanceNoOutputTypeName{}   -> instanceProblemHighlighting w
    InstanceArgWithExplicitArg{} -> instanceProblemHighlighting w
    InversionDepthReached{}    -> mempty
    -- Andreas, 2020-03-21, issue #4456:
    -- Error warnings that do not have dedicated highlighting
    -- are highlighted as errors.
    InvalidCharacterLiteral{}             -> errorWarningHighlighting w
    SafeFlagPostulate{}                   -> errorWarningHighlighting w
    SafeFlagPragma{}                      -> errorWarningHighlighting w
    SafeFlagWithoutKFlagPrimEraseEquality -> errorWarningHighlighting w
    InfectiveImport{}                     -> errorWarningHighlighting w
    CoInfectiveImport{}                   -> errorWarningHighlighting w
    InvalidDisplayForm{}                  -> deadcodeHighlighting w
    UnusedVariablesInDisplayForm xs       -> foldMap deadcodeHighlighting xs
    TooManyArgumentsToSort _ args         -> errorWarningHighlighting args
    RewritesNothing                       -> cosmeticProblemHighlighting w
    WithClauseProjectionFixityMismatch p _ _ _ -> cosmeticProblemHighlighting p
    WithoutKFlagPrimEraseEquality -> mempty
    ConflictingPragmaOptions{} -> mempty
    DeprecationWarning{}       -> mempty
    UserWarning{}              -> mempty
    LibraryWarning{}           -> mempty
    ConfluenceCheckingIncompleteBecauseOfMeta{} -> confluenceErrorHighlighting w
    ConfluenceForCubicalNotSupported{} -> mempty
    RewriteNonConfluent{}      -> confluenceErrorHighlighting w
    RewriteMaybeNonConfluent{} -> confluenceErrorHighlighting w
    RewriteAmbiguousRules{}    -> confluenceErrorHighlighting w
    RewriteMissingRule{}       -> confluenceErrorHighlighting w
    IllegalRewriteRule x _     -> deadcodeHighlighting x
    NotARewriteRule x _        -> deadcodeHighlighting x
    PragmaCompileErased{}      -> deadcodeHighlighting w
    PragmaCompileList{}        -> deadcodeHighlighting w
    PragmaCompileMaybe{}       -> deadcodeHighlighting w
    PragmaCompileWrong{}       -> deadcodeHighlighting w
    PragmaCompileWrongName{}   -> deadcodeHighlighting w
    PragmaCompileUnparsable{}  -> deadcodeHighlighting w
    PragmaExpectsDefinedSymbol{}
                               -> deadcodeHighlighting w
    PragmaExpectsUnambiguousConstructorOrFunction{}
                               -> deadcodeHighlighting w
    PragmaExpectsUnambiguousProjectionOrFunction{}
                               -> deadcodeHighlighting w
    NoMain{}                   -> mempty
    NotInScopeW{}              -> deadcodeHighlighting w
    UnsupportedIndexedMatch{}  -> mempty
    AsPatternShadowsConstructorOrPatternSynonym{}
                               -> deadcodeHighlighting w
    PatternShadowsConstructor{}-> errorWarningHighlighting w  -- or mempty ?
    PlentyInHardCompileTimeMode o
                               -> deadcodeHighlighting o
    RecordFieldWarning w       -> recordFieldWarningHighlighting w
    OptionWarning w            -> mempty
    ParseWarning w             -> case w of
      Pa.MisplacedAttributes{}      -> deadcodeHighlighting w
      Pa.UnknownPolarity{}          -> deadcodeHighlighting w
      Pa.UnknownAttribute{}         -> deadcodeHighlighting w
      Pa.UnsupportedAttribute{}     -> deadcodeHighlighting w
      Pa.MultipleAttributes{}       -> deadcodeHighlighting w
      Pa.OverlappingTokensWarning{} -> mempty
    MissingTypeSignatureForOpaque{} -> errorWarningHighlighting w
    NotAffectedByOpaque{}           -> deadcodeHighlighting w
    UselessOpaque{}                 -> deadcodeHighlighting w
    UnfoldingWrongName x            -> deadcodeHighlighting x
    UnfoldTransparentName r         -> deadcodeHighlighting r
    FaceConstraintCannotBeHidden{}  -> deadcodeHighlighting w
    FaceConstraintCannotBeNamed{}   -> deadcodeHighlighting w
  
    HiddenNotInArgumentPosition{}   -> errorWarningHighlighting w
    InstanceNotInArgumentPosition{} -> errorWarningHighlighting w
    MacroInLetBindings{}            -> errorWarningHighlighting w
    AbstractInLetBindings{}         -> errorWarningHighlighting w
  
    NicifierIssue (DeclarationWarning _ w) -> case w of
      -- we intentionally override the binding of `w` here so that our pattern of
      -- using `getRange w` still yields the most precise range information we
      -- can get.
      NotAllowedInMutual{}             -> deadcodeHighlighting w
      DivergentModalityInClause{}      -> deadcodeHighlighting w
      EmptyAbstract{}                  -> deadcodeHighlighting w
      EmptyConstructor{}               -> deadcodeHighlighting w
      EmptyInstance{}                  -> deadcodeHighlighting w
      EmptyMacro{}                     -> deadcodeHighlighting w
      EmptyMutual{}                    -> deadcodeHighlighting w
      EmptyPostulate{}                 -> deadcodeHighlighting w
      EmptyPrimitive{}                 -> deadcodeHighlighting w
      EmptyPrivate{}                   -> deadcodeHighlighting w
      EmptyGeneralize{}                -> deadcodeHighlighting w
      EmptyField{}                     -> deadcodeHighlighting w
      EmptyPolarityPragma{}            -> deadcodeHighlighting w
      HiddenGeneralize{}               -> mempty
        -- Andreas, 2022-03-25, issue #5850
        -- We would like @deadcodeHighlighting w@ for the braces in
        -- @variable {x} : A@, but these have no range, so we cannot highlight them.
        -- Highlighting the variable instead might be misleading,
        -- suggesting that it is not generalized over.
      UselessAbstract{}                -> deadcodeHighlighting w
      UselessInstance{}                -> deadcodeHighlighting w
      UselessMacro{}                   -> deadcodeHighlighting w
      UselessPrivate{}                 -> deadcodeHighlighting w
      InvalidCatchallPragma{}          -> deadcodeHighlighting w
      InvalidNoPositivityCheckPragma{} -> deadcodeHighlighting w
      InvalidNoUniverseCheckPragma{}   -> deadcodeHighlighting w
      InvalidTerminationCheckPragma{}  -> deadcodeHighlighting w
      InvalidCoverageCheckPragma{}     -> deadcodeHighlighting w
      InvalidConstructorBlock{}        -> deadcodeHighlighting w
      InvalidTacticAttribute{}         -> deadcodeHighlighting w
      OpenImportAbstract{}             -> cosmeticProblemHighlighting w
      OpenImportPrivate{}              -> cosmeticProblemHighlighting w
      SafeFlagEta                   {} -> errorWarningHighlighting w
      SafeFlagInjective             {} -> errorWarningHighlighting w
      SafeFlagNoCoverageCheck       {} -> errorWarningHighlighting w
      SafeFlagNoPositivityCheck     {} -> errorWarningHighlighting w
      SafeFlagNoUniverseCheck       {} -> errorWarningHighlighting w
      SafeFlagNonTerminating        {} -> errorWarningHighlighting w
      SafeFlagPolarity              {} -> errorWarningHighlighting w
      SafeFlagTerminating           {} -> errorWarningHighlighting w
      W.ShadowingInTelescope nrs       -> foldMap
                                            (shadowingTelHighlighting . snd)
                                            nrs
      MissingDataDeclaration{}         -> missingDefinitionHighlighting w
      MissingDefinitions{}             -> missingDefinitionHighlighting w
      -- TODO: explore highlighting opportunities here!
      PolarityPragmasButNotPostulates{} -> mempty
      PragmaNoTerminationCheck{}        -> mempty
      PragmaCompiled{}                  -> errorWarningHighlighting w
      UnknownFixityInMixfixDecl{}       -> mempty
      UnknownNamesInFixityDecl{}        -> mempty
      UnknownNamesInPolarityPragmas{}   -> mempty
  
    -- Backends
    CustomBackendWarning{} -> mempty
  
    -- Polarities
    TooManyPolarities _x occs -> deadcodeHighlighting occs
    TopLevelPolarity{} -> errorWarningHighlighting w
  
  recordFieldWarningHighlighting ::
    RecordFieldWarning -> HighlightingInfoBuilder
  recordFieldWarningHighlighting = \case
    W.DuplicateFields xrs      -> sconcat $ fmap (dead . snd) xrs
    W.TooManyFields _q _ys xrs -> dead $ fmap snd xrs
    where
    dead :: List1 Range -> HighlightingInfoBuilder
    dead = sconcat . fmap deadcodeHighlighting
    -- Andreas, 2020-03-27 #3684: This variant seems to only highlight @x@:
    -- dead = mconcat . map f
    -- f (x, r) = deadcodeHighlighting (getRange x) `mappend` deadcodeHighlighting r
  
  -- | Generate syntax highlighting for termination errors.
  
  terminationErrorHighlighting ::
    List1 TerminationError -> HighlightingInfoBuilder
  terminationErrorHighlighting termErrs = functionDefs `mappend` callSites
    where
      m            = parserBased { otherAspects = Set.singleton TerminationProblem }
      functionDefs = foldMap (\x -> H.singleton (rToR $ bindingSite x) m) $
                     concatMap termErrFunctions termErrs
      callSites    = foldMap (\r -> H.singleton (rToR r) m) $
                     concatMap (map getRange . termErrCalls) termErrs
      bindingSite  = A.nameBindingSite . A.qnameName
  
  -- | Generate syntax highlighting for not-strictly-positive inductive
  -- definitions.
  
  positivityErrorHighlighting ::
    I.QName -> Seq OccursWhere -> HighlightingInfoBuilder
  positivityErrorHighlighting q os =
    several (rToR <$> getRange q : rs) m
    where
      rs = map (\(OccursWhere r _ _) -> r) (Fold.toList os)
      m  = parserBased { otherAspects = Set.singleton PositivityProblem }
  
  deadcodeHighlighting :: HasRange a => a -> HighlightingInfoBuilder
  deadcodeHighlighting a = H.singleton (rToR $ P.continuous $ getRange a) m
    where m = parserBased { otherAspects = Set.singleton Deadcode }
  
  coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
  coverageErrorHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m
    where m = parserBased { otherAspects = Set.singleton CoverageProblem }
  
  shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
  shadowingTelHighlighting =
    -- we do not want to highlight the one variable in scope so we take
    -- the @init@ segment of the ranges in question
    foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . List2.init
    where
    m = parserBased { otherAspects =
                        Set.singleton H.ShadowingInTelescope }
  
  catchallHighlighting :: Range -> HighlightingInfoBuilder
  catchallHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m
    where m = parserBased { otherAspects = Set.singleton CatchallClause }
  
  cosmeticProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
  cosmeticProblemHighlighting a = H.singleton (rToR $ P.continuousPerLine r) m
    where
      r = getRange a
      m = parserBased { otherAspects = Set.singleton CosmeticProblem }
  
  confluenceErrorHighlighting ::
    HasRange a => a -> HighlightingInfoBuilder
  confluenceErrorHighlighting a = H.singleton (rToR $ P.continuousPerLine $ getRange a) m
    where m = parserBased { otherAspects = Set.singleton ConfluenceProblem }
  
  instanceProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
  instanceProblemHighlighting a = H.singleton (rToR $ P.continuousPerLine r) m
    where
      r = getRange a
      m = parserBased { otherAspects = Set.singleton InstanceProblem }
  
  missingDefinitionHighlighting ::
    HasRange a => a -> HighlightingInfoBuilder
  missingDefinitionHighlighting a = H.singleton (rToR $ P.continuousPerLine $ getRange a) m
    where m = parserBased { otherAspects = Set.singleton Aspect.MissingDefinition }
  
  -- | Generates and prints syntax highlighting information for unsolved
  -- meta-variables and certain unsolved constraints.
  
  printUnsolvedInfo :: TCM ()
  printUnsolvedInfo = do
    info <- computeUnsolvedInfo
  
    printHighlightingInfo KeepHighlighting (convert info)
  
  computeUnsolvedInfo :: TCM HighlightingInfoBuilder
  computeUnsolvedInfo = do
    (rs, metaInfo) <- computeUnsolvedMetaWarnings
    constraintInfo <- computeUnsolvedConstraints rs
  
    return $ metaInfo `mappend` constraintInfo
  
  -- | Generates syntax highlighting information for unsolved meta
  -- variables.
  --   Also returns ranges of unsolved or interaction metas.
  computeUnsolvedMetaWarnings :: TCM ([Ranges], HighlightingInfoBuilder)
  computeUnsolvedMetaWarnings = do
    is <- getInteractionMetas
  
    -- We don't want to highlight blocked terms, since
    --   * there is always at least one proper meta responsible for the blocking
    --   * in many cases the blocked term covers the highlighting for this meta
    --   * for the same reason we skip metas with a twin, since the twin will be blocked.
    let notBlocked m = not <$> isBlockedTerm m
    let notHasTwin m = not <$> hasTwinMeta m
    ms <- filterM notHasTwin =<< filterM notBlocked =<< getOpenMetas
  
    let extend = map (rToR . P.continuousPerLine)
  
    rs <- extend <$> mapM getMetaRange (ms \\ is)
  
    rs' <- extend <$> mapM getMetaRange is
    return $ (rs ++ rs', metasHighlighting' rs)
  
  metasHighlighting :: [Range] -> HighlightingInfoBuilder
  metasHighlighting = metasHighlighting' . fmap (rToR . P.continuousPerLine)
  
  metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
  metasHighlighting' rs =
    several (List1.toList rs) parserBased{ otherAspects = Set.singleton UnsolvedMeta }
  
  -- | Generates syntax highlighting information for unsolved constraints
  --   (ideally: that are not connected to a meta variable).
  
  computeUnsolvedConstraints :: [Ranges] -- ^ does not add ranges that would overlap with these.
                             -> TCM HighlightingInfoBuilder
  computeUnsolvedConstraints ms = constraintsHighlighting ms <$> getAllConstraints
  
  constraintsHighlighting ::
    [Ranges] -> Constraints -> HighlightingInfoBuilder
  constraintsHighlighting ms cs =
    several (filter noOverlap $ map (rToR . P.continuousPerLine) rs)
            (parserBased { otherAspects = Set.singleton UnsolvedConstraint })
    where
    noOverlap r = not $ any (overlappings $ r) $ ms
    -- get ranges of interesting unsolved constraints
    rs = (`mapMaybe` (map theConstraint cs)) $ \case
      Closure{ clValue = IsEmpty r t           } -> Just r
      Closure{ clEnv = e, clValue = ValueCmp{} } -> Just $ getRange (envRange e)
      Closure{ clEnv = e, clValue = ElimCmp{}  } -> Just $ getRange (envRange e)
      Closure{ clEnv = e, clValue = SortCmp{}  } -> Just $ getRange (envRange e)
      Closure{ clEnv = e, clValue = LevelCmp{} } -> Just $ getRange (envRange e)
      Closure{ clEnv = e, clValue = CheckSizeLtSat{} } -> Just $ getRange (envRange e)
      _ -> Nothing
  
  
  -- * Disambiguation of constructors and projections.
  
  storeDisambiguatedField :: A.QName -> TCM ()
  storeDisambiguatedField = storeDisambiguatedName Field
  
  storeDisambiguatedProjection :: A.QName -> TCM ()
  storeDisambiguatedProjection = storeDisambiguatedField
  
  storeDisambiguatedConstructor :: Induction -> A.QName -> TCM ()
  storeDisambiguatedConstructor i = storeDisambiguatedName $ Constructor i
  
  -- TODO: move the following function to a new module TypeChecking.Overloading
  -- that gathers functions concerning disambiguation of overloading.
  
  -- | Remember a name disambiguation (during type checking).
  --   To be used later during syntax highlighting.
  --   Also: raise user warnings associated with the name.
  storeDisambiguatedName :: NameKind -> A.QName -> TCM ()
  storeDisambiguatedName k q = do
    raiseWarningsOnUsage q
    whenJust (start $ getRange q) $ \ i ->
      modifyTCLens stDisambiguatedNames $ IntMap.insert i $ DisambiguatedName k q
    where
    start r = fromIntegral . P.posPos <$> P.rStart' r
  
  -- | Store a disambiguation of record field tags for the purpose of highlighting.
  disambiguateRecordFields
    :: [C.Name]   -- ^ Record field names in a record expression.
    -> [A.QName]  -- ^ Record field names in the corresponding record type definition
    -> TCM ()
  disambiguateRecordFields cxs axs = forM_ cxs $ \ cx -> do
    caseMaybe (List.find ((cx ==) . A.nameConcrete . A.qnameName) axs) (return ()) $ \ ax -> do
      storeDisambiguatedField ax{ A.qnameName = (A.qnameName ax) { A.nameConcrete = cx } }
  