    -- | 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 (Semigroup(..))
    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 :: TCWarning -> TCM ()
    highlightWarning TCWarning
    tcwarn = do
      let h :: HighlightingInfo
    h = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    False TCWarning
    tcwarn
      -- Highlighting for warnings coming from the Happy parser is placed
      -- together with token highlighting.
      case TCWarning -> Warning
    tcWarning TCWarning
    tcwarn of
        ParseWarning{} -> Lens' TCState HighlightingInfo
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
    Lens' TCState HighlightingInfo
    stTokens     (HighlightingInfo
    h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>)
        Warning
    _              -> Lens' TCState HighlightingInfo
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
    Lens' TCState HighlightingInfo
    stSyntaxInfo (HighlightingInfo
    h HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>)
      HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingInfo
    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 :: Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    _ Bool
    _ | Range -> Bool
    forall a. Null a => a -> Bool
    null (Range -> Bool) -> Range -> Bool
    forall a b. (a -> b) -> a -> b
    $ Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    decl = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    hlLevel Bool
    updateState = do
      top <- TopLevelModuleName
    -> Maybe TopLevelModuleName -> TopLevelModuleName
    forall a. a -> Maybe a -> a
    fromMaybe TopLevelModuleName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
    -> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe TopLevelModuleName)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe TopLevelModuleName)
    currentTopLevelModule

      reportSDoc "import.iface.create" 15 $
        TCM.fwords
          ("Generating syntax info for the following declaration " ++
           case hlLevel of
             Full   {} -> [Char]
    "(final):"
             Partial{} -> [Char]
    "(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{} -> TopLevelModuleName
    -> NameKinds -> Declaration -> TCMT IO HighlightingInfoBuilder
    generateConstructorInfo TopLevelModuleName
    top NameKinds
    kinds Declaration
    decl
          Level
    _      -> HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

        -- Main source of scope-checker generated highlighting:
        let nameInfo = TopLevelModuleName
    -> NameKinds -> Declaration -> HighlightingInfoBuilder
    forall a.
    Hilite a =>
    TopLevelModuleName -> NameKinds -> a -> HighlightingInfoBuilder
    runHighlighter TopLevelModuleName
    top NameKinds
    kinds Declaration
    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 = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder
    constructorInfo HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Semigroup a => a -> a -> a
    <> HighlightingInfoBuilder
    nameInfo)
                           HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>
                         HighlightingInfo
    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 :: AbsolutePath -> TCMT IO HighlightingInfo
    generateTokenInfo AbsolutePath
    file =
      RangeFile -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromSource RangeFile
    rf ([Char] -> TCMT IO HighlightingInfo)
    -> (Text -> [Char]) -> Text -> TCMT IO HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> [Char]
    Text.unpack (Text -> TCMT IO HighlightingInfo)
    -> TCMT IO Text -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
        PM Text -> TCMT IO Text
    forall a. PM a -> TCM a
    runPM (RangeFile -> PM Text
    Pa.readFilePM RangeFile
    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 :: RangeFile
    rf = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
    P.mkRangeFile AbsolutePath
    file Maybe TopLevelModuleName
    forall a. Maybe a
    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 :: RangeFile -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromSource RangeFile
    file [Char]
    input =
      PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a. PM a -> TCM a
    runPM (PM HighlightingInfo -> TCMT IO HighlightingInfo)
    -> PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ [Token] -> HighlightingInfo
    tokenHighlighting ([Token] -> HighlightingInfo)
    -> ((([Token], Attributes), FileType) -> [Token])
    -> (([Token], Attributes), FileType)
    -> HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Token], Attributes) -> [Token]
    forall a b. (a, b) -> a
    fst (([Token], Attributes) -> [Token])
    -> ((([Token], Attributes), FileType) -> ([Token], Attributes))
    -> (([Token], Attributes), FileType)
    -> [Token]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Token], Attributes), FileType) -> ([Token], Attributes)
    forall a b. (a, b) -> a
    fst ((([Token], Attributes), FileType) -> HighlightingInfo)
    -> PM (([Token], Attributes), FileType) -> PM HighlightingInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              Parser [Token]
    -> RangeFile -> [Char] -> PM (([Token], Attributes), FileType)
    forall a.
    Show a =>
    Parser a -> RangeFile -> [Char] -> PM ((a, Attributes), FileType)
    Pa.parseFile Parser [Token]
    Pa.tokensParser RangeFile
    file [Char]
    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 :: Range -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromString Range
    r [Char]
    _ | Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    forall a. Range' a
    noRange = HighlightingInfo -> TCMT IO HighlightingInfo
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfo
    forall a. Monoid a => a
    mempty
    generateTokenInfoFromString Range
    r [Char]
    s = do
      PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a. PM a -> TCM a
    runPM (PM HighlightingInfo -> TCMT IO HighlightingInfo)
    -> PM HighlightingInfo -> TCMT IO HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ [Token] -> HighlightingInfo
    tokenHighlighting ([Token] -> HighlightingInfo)
    -> (([Token], Attributes) -> [Token])
    -> ([Token], Attributes)
    -> HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Token], Attributes) -> [Token]
    forall a b. (a, b) -> a
    fst (([Token], Attributes) -> HighlightingInfo)
    -> PM ([Token], Attributes) -> PM HighlightingInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              Parser [Token] -> Position -> [Char] -> PM ([Token], Attributes)
    forall a. Parser a -> Position -> [Char] -> PM (a, Attributes)
    Pa.parsePosString Parser [Token]
    Pa.tokensParser Position
    p [Char]
    s
      where
        Just Position
    p = Range -> Maybe Position
    forall a. Range' a -> Maybe (Position' a)
    P.rStart Range
    r

    -- | Compute syntax highlighting for the given tokens.
    tokenHighlighting :: [T.Token] -> HighlightingInfo
    tokenHighlighting :: [Token] -> HighlightingInfo
    tokenHighlighting = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> ([Token] -> HighlightingInfoBuilder)
    -> [Token]
    -> HighlightingInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [HighlightingInfoBuilder] -> HighlightingInfoBuilder
    forall a. Monoid a => [a] -> a
    mconcat ([HighlightingInfoBuilder] -> HighlightingInfoBuilder)
    -> ([Token] -> [HighlightingInfoBuilder])
    -> [Token]
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Token -> HighlightingInfoBuilder)
    -> [Token] -> [HighlightingInfoBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map Token -> HighlightingInfoBuilder
    tokenToHI
      where
      -- Converts an aspect and a range to a file.
      aToF :: Aspect -> Range -> m
    aToF Aspect
    a Range
    r = Ranges -> Aspects -> m
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r) (Aspects
    forall a. Monoid a => a
    mempty { aspect = Just a })

      tokenToHI :: T.Token -> HighlightingInfoBuilder
      tokenToHI :: Token -> HighlightingInfoBuilder
    tokenToHI (T.TokKeyword Keyword
    T.KwForall Interval
    i)  = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Symbol (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokKeyword Keyword
    T.KwREWRITE Interval
    _) = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty  -- #4361, REWRITE is not always a Keyword
      tokenToHI (T.TokKeyword Keyword
    _ Interval
    i)           = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Keyword (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokSymbol Symbol
    T.SymQuestionMark Interval
    i) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Hole (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokSymbol  Symbol
    _ Interval
    i)                = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Symbol (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitNat    Integer
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitWord64 Word64
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitFloat  Double
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Number Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitString Text
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitChar   Char
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitQName  QName
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokLiteral (Ranged Range
    r (L.LitMeta TopLevelModuleName
    _ MetaId
    _))) = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    String Range
    r
      tokenToHI (T.TokComment (Interval
    i, [Char]
    _))            = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Comment (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokTeX (Interval
    i, [Char]
    _))                = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Background (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokMarkup (Interval
    i, [Char]
    _))             = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Markup (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokId {})                     = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokQId {})                    = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokString (Interval
    i,[Char]
    s))              = Aspect -> Range -> HighlightingInfoBuilder
    forall {m}. IsBasicRangeMap Aspects m => Aspect -> Range -> m
    aToF Aspect
    Pragma (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i)
      tokenToHI (T.TokDummy {})                  = HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      tokenToHI (T.TokEOF {})                    = HighlightingInfoBuilder
    forall a. Monoid a => a
    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 :: Level -> Declaration -> TCM NameKinds
    nameKinds Level
    hlLevel Declaration
    decl = do
      imported <- Lens' TCState (HashMap QName Definition)
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Lens' TCState (HashMap QName Definition)
     -> TCMT IO (HashMap QName Definition))
    -> Lens' TCState (HashMap QName Definition)
    -> TCMT IO (HashMap QName Definition)
    forall a b. (a -> b) -> a -> b
    $ (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stImports ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions
      local    <- case hlLevel of
        Full{} -> Lens' TCState (HashMap QName Definition)
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Lens' TCState (HashMap QName Definition)
     -> TCMT IO (HashMap QName Definition))
    -> Lens' TCState (HashMap QName Definition)
    -> TCMT IO (HashMap QName Definition)
    forall a b. (a -> b) -> a -> b
    $ (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions
        Level
    _      -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HashMap QName Definition
    forall k v. HashMap k v
    HMap.empty
      impPatSyns <- useTC stPatternSynImports
      locPatSyns <- case hlLevel of
        Full{} -> Lens' TCState (Map QName PatternSynDefn)
    -> TCMT IO (Map QName PatternSynDefn)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map QName PatternSynDefn -> f (Map QName PatternSynDefn))
    -> TCState -> f TCState
    Lens' TCState (Map QName PatternSynDefn)
    stPatternSyns
        Level
    _      -> Map QName PatternSynDefn -> TCMT IO (Map QName PatternSynDefn)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map QName PatternSynDefn
    forall a. Null a => a
    empty
          -- Traverses the syntax tree and constructs a map from qualified
          -- names to name kinds. TODO: Handle open public.
      let syntax :: NameKindMap
          syntax = NameKindBuilder -> NameKindMap -> NameKindMap
    runBuilder (Declaration -> NameKindBuilder
    forall m. Collection KName m => Declaration -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames Declaration
    decl :: NameKindBuilder) NameKindMap
    forall k v. HashMap k v
    HMap.empty
      return $ \ QName
    n -> (NameKind -> NameKind -> NameKind)
    -> [Maybe NameKind] -> Maybe NameKind
    forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
    unionsMaybeWith NameKind -> NameKind -> NameKind
    mergeNameKind
        [ Defn -> NameKind
    defnToKind (Defn -> NameKind)
    -> (Definition -> Defn) -> Definition -> NameKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n HashMap QName Definition
    local
        , NameKind
    con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    n Map QName PatternSynDefn
    locPatSyns
        , Defn -> NameKind
    defnToKind (Defn -> NameKind)
    -> (Definition -> Defn) -> Definition -> NameKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n HashMap QName Definition
    imported
        , NameKind
    con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    n Map QName PatternSynDefn
    impPatSyns
        , QName -> NameKindMap -> Maybe NameKind
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    n NameKindMap
    syntax
        ]
      where
      defnToKind :: TCM.Defn -> NameKind
      defnToKind :: Defn -> NameKind
    defnToKind   TCM.Axiom{}                           = NameKind
    Postulate
      defnToKind   TCM.DataOrRecSig{}                    = NameKind
    Postulate
      defnToKind   TCM.GeneralizableVar{}                = NameKind
    Generalizable
      defnToKind d :: Defn
    d@TCM.Function{}
        | Defn -> Bool
    isProperProjection Defn
    d                           = NameKind
    Field
        | Defn -> Bool
    isMacro Defn
    d                                      = NameKind
    Macro          -- AIM XL, issue #7324
        | Bool
    otherwise                                      = NameKind
    Function
      defnToKind   TCM.Datatype{}                        = NameKind
    Datatype
      defnToKind   TCM.Record{}                          = NameKind
    Record
      defnToKind   TCM.Constructor{ conSrcCon :: Defn -> ConHead
    TCM.conSrcCon = ConHead
    c }  = Induction -> NameKind
    Constructor (Induction -> NameKind) -> Induction -> NameKind
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Induction
    I.conInductive ConHead
    c
      defnToKind   TCM.Primitive{}                       = NameKind
    Primitive
      defnToKind   TCM.PrimitiveSort{}                   = NameKind
    Primitive
      defnToKind   TCM.AbstractDefn{}                    = NameKind
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      con :: NameKind
      con :: NameKind
    con = Induction -> NameKind
    Constructor Induction
    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 :: NameKind -> NameKind -> NameKind
    mergeNameKind NameKind
    Postulate NameKind
    k = NameKind
    k
    mergeNameKind NameKind
    _     NameKind
    Macro = NameKind
    Macro  -- If the abstract syntax says macro, it's a macro.
    mergeNameKind NameKind
    k         NameKind
    _ = NameKind
    k

    -- Auxiliary types for @nameKinds@ generation

    type NameKindMap     = HashMap A.QName NameKind
    data NameKindBuilder = NameKindBuilder
      { NameKindBuilder -> NameKindMap -> NameKindMap
    runBuilder :: NameKindMap -> NameKindMap
      }

    instance Semigroup (NameKindBuilder) where
      NameKindBuilder NameKindMap -> NameKindMap
    f <> :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    <> NameKindBuilder NameKindMap -> NameKindMap
    g = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
    -> (NameKindMap -> NameKindMap) -> NameKindBuilder
    forall a b. (a -> b) -> a -> b
    $ NameKindMap -> NameKindMap
    f (NameKindMap -> NameKindMap)
    -> (NameKindMap -> NameKindMap) -> NameKindMap -> NameKindMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NameKindMap -> NameKindMap
    g

    instance Monoid (NameKindBuilder) where
      mempty :: NameKindBuilder
    mempty = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder NameKindMap -> NameKindMap
    forall a. a -> a
    id
      mappend :: NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    mappend = NameKindBuilder -> NameKindBuilder -> NameKindBuilder
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Singleton KName NameKindBuilder where
      singleton :: KName -> NameKindBuilder
    singleton (WithKind KindOfName
    k QName
    q) = (NameKindMap -> NameKindMap) -> NameKindBuilder
    NameKindBuilder ((NameKindMap -> NameKindMap) -> NameKindBuilder)
    -> (NameKindMap -> NameKindMap) -> NameKindBuilder
    forall a b. (a -> b) -> a -> b
    $
        (NameKind -> NameKind -> NameKind)
    -> QName -> NameKind -> NameKindMap -> NameKindMap
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith NameKind -> NameKind -> NameKind
    mergeNameKind QName
    q (NameKind -> NameKindMap -> NameKindMap)
    -> NameKind -> NameKindMap -> NameKindMap
    forall a b. (a -> b) -> a -> b
    $ KindOfName -> NameKind
    kindOfNameToNameKind KindOfName
    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 :: TopLevelModuleName
    -> NameKinds -> Declaration -> TCMT IO HighlightingInfoBuilder
    generateConstructorInfo TopLevelModuleName
    top NameKinds
    kinds Declaration
    decl = do

      -- Get boundaries of current declaration.
      -- @noRange@ should be impossible, but in case of @noRange@
      -- it makes sense to return mempty.
      [IntervalWithoutFile]
    -> TCMT IO HighlightingInfoBuilder
    -> (IntervalWithoutFile
        -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    forall a b. [a] -> b -> (a -> [a] -> b) -> b
    caseList (Range -> [IntervalWithoutFile]
    forall a. Range' a -> [IntervalWithoutFile]
    P.rangeIntervals (Range -> [IntervalWithoutFile]) -> Range -> [IntervalWithoutFile]
    forall a b. (a -> b) -> a -> b
    $ Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    decl)
               (HighlightingInfoBuilder -> TCMT IO HighlightingInfoBuilder
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty) ((IntervalWithoutFile
      -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
     -> TCMT IO HighlightingInfoBuilder)
    -> (IntervalWithoutFile
        -> [IntervalWithoutFile] -> TCMT IO HighlightingInfoBuilder)
    -> TCMT IO HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ \ IntervalWithoutFile
    i [IntervalWithoutFile]
    is -> do
        let start :: Key
    start = Word32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32 -> Key) -> Word32 -> Key
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Word32
    forall a. Position' a -> Word32
    P.posPos (Position' () -> Word32) -> Position' () -> Word32
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> Position' ()
    forall a. Interval' a -> Position' a
    P.iStart IntervalWithoutFile
    i
            end :: Key
    end   = Word32 -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32 -> Key) -> Word32 -> Key
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Word32
    forall a. Position' a -> Word32
    P.posPos (Position' () -> Word32) -> Position' () -> Word32
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> Position' ()
    forall a. Interval' a -> Position' a
    P.iEnd (IntervalWithoutFile -> Position' ())
    -> IntervalWithoutFile -> Position' ()
    forall a b. (a -> b) -> a -> b
    $ IntervalWithoutFile -> [IntervalWithoutFile] -> IntervalWithoutFile
    forall a. a -> [a] -> a
    last1 IntervalWithoutFile
    i [IntervalWithoutFile]
    is

        -- Get all disambiguated names that fall within the range of decl.
        m0 <- Lens' TCState (IntMap DisambiguatedName)
    -> TCMT IO (IntMap DisambiguatedName)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (IntMap DisambiguatedName -> f (IntMap DisambiguatedName))
    -> TCState -> f TCState
    Lens' TCState (IntMap DisambiguatedName)
    stDisambiguatedNames
        let (_, m1) = IntMap.split (pred start) m0
            (m2, _) = IntMap.split end m1
            constrs = IntMap DisambiguatedName -> [DisambiguatedName]
    forall a. IntMap a -> [a]
    IntMap.elems IntMap DisambiguatedName
    m2

        -- Return suitable syntax highlighting information.
        return $ foldMap (runHighlighter top kinds) constrs

    printSyntaxInfo :: Range -> TCM ()
    printSyntaxInfo :: Range -> TCM ()
    printSyntaxInfo Range
    r = do
      syntaxInfo <- Lens' TCState HighlightingInfo -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
    Lens' TCState HighlightingInfo
    stSyntaxInfo
      ifTopLevelAndHighlightingLevelIs NonInteractive $
        printHighlightingInfo KeepHighlighting
          (restrictTo (rangeToRange r) syntaxInfo)

    -- | Prints syntax highlighting info for an error.

    printErrorInfo :: TCErr -> TCM ()
    printErrorInfo :: TCErr -> TCM ()
    printErrorInfo TCErr
    e =
      RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (HighlightingInfo -> TCM ())
    -> (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> TCM ())
    -> TCMT IO HighlightingInfoBuilder -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
        TCErr -> TCMT IO HighlightingInfoBuilder
    errorHighlighting TCErr
    e

    -- | Generate highlighting for error.

    errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
    errorHighlighting :: TCErr -> TCMT IO HighlightingInfoBuilder
    errorHighlighting TCErr
    e = Range -> [Char] -> HighlightingInfoBuilder
    errorHighlighting' (TCErr -> Range
    forall a. HasRange a => a -> Range
    getRange TCErr
    e) ([Char] -> HighlightingInfoBuilder)
    -> TCMT IO [Char] -> TCMT IO HighlightingInfoBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCErr -> TCMT IO [Char]
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
    TCM.renderError TCErr
    e

    errorHighlighting'
      :: Range     -- ^ Error range.
      -> String    -- ^ Error message for tooltip.
      -> HighlightingInfoBuilder
    errorHighlighting' :: Range -> [Char] -> HighlightingInfoBuilder
    errorHighlighting' Range
    r [Char]
    s = [HighlightingInfoBuilder] -> HighlightingInfoBuilder
    forall a. Monoid a => [a] -> a
    mconcat
      [ -- Erase previous highlighting.
        Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    forall a. Monoid a => a
    mempty
      , -- Print new highlighting.
        Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r)
             (Aspects -> HighlightingInfoBuilder)
    -> Aspects -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ Aspects
    parserBased { otherAspects = Set.singleton Error
                           , note         = s
                           }
      ]

    -- | Highlighting for warnings that are considered fatal.

    errorWarningHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting a
    w =
      Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    w) (Aspects -> HighlightingInfoBuilder)
    -> Aspects -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
        Aspects
    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 :: TCWarning -> HighlightingInfoBuilder
    warningHighlighting = Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    True

    warningHighlighting' :: Bool -- ^ should we generate highlighting for unsolved metas and constrains?
                         -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' :: Bool -> TCWarning -> HighlightingInfoBuilder
    warningHighlighting' Bool
    b TCWarning
    w = case TCWarning -> Warning
    tcWarning TCWarning
    w of
      TerminationIssue List1 TerminationError
    terrs     -> List1 TerminationError -> HighlightingInfoBuilder
    terminationErrorHighlighting List1 TerminationError
    terrs
      NotStrictlyPositive QName
    d Seq OccursWhere
    ocs  -> QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting QName
    d Seq OccursWhere
    ocs
      ConstructorDoesNotFitInData DataOrRecord_
    _dataOrRecord QName
    c Sort
    _s1 Sort
    _s2 TCErr
    _err -> Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
         QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    c Range -> Range -> Range
    forall a. Null a => a -> a -> a
    `catchNull` TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      CoinductiveEtaRecord QName
    _x    -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      -- #3965 highlight each unreachable clause independently: they
      -- may be interleaved with actually reachable clauses!
      UnreachableClauses QName
    _ List1 Range
    rs    -> (Range -> HighlightingInfoBuilder)
    -> List1 Range -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 Range
    rs
      CoverageIssue{}            -> Range -> HighlightingInfoBuilder
    coverageErrorHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      CoverageNoExactSplit{}     -> Range -> HighlightingInfoBuilder
    catchallHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      InlineNoExactSplit{}       -> Range -> HighlightingInfoBuilder
    catchallHighlighting (Range -> HighlightingInfoBuilder)
    -> Range -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Range
    forall a. HasRange a => a -> Range
    getRange TCWarning
    w
      UnsolvedConstraints List1 ProblemConstraint
    cs     -> if Bool
    b then [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [] (Constraints -> HighlightingInfoBuilder)
    -> Constraints -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ List1 ProblemConstraint -> Constraints
    forall a. NonEmpty a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList List1 ProblemConstraint
    cs else HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UnsolvedMetaVariables Set1 Range
    rs   -> if Bool
    b then [Range] -> HighlightingInfoBuilder
    metasHighlighting          ([Range] -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ Set1 Range -> [Range]
    forall a. NESet a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList Set1 Range
    rs else HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      AbsurdPatternRequiresAbsentRHS{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      DuplicateRecordDirective{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      ModuleDoesntExport QName
    _ [Name]
    _ [Name]
    _ List1 ImportedName
    xs  -> (ImportedName -> HighlightingInfoBuilder)
    -> List1 ImportedName -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ImportedName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 ImportedName
    xs
      DuplicateUsing List1 ImportedName
    xs            -> (ImportedName -> HighlightingInfoBuilder)
    -> List1 ImportedName -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ImportedName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 ImportedName
    xs
      FixityInRenamingModule List1 Range
    rs    -> (Range -> HighlightingInfoBuilder)
    -> List1 Range -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 Range
    rs
      -- expanded catch-all case to get a warning for new constructors
      CantGeneralizeOverSorts{}  -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UnsolvedInteractionMetas{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      InteractionMetaBoundaries{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      OldBuiltin{}                -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      BuiltinDeclaresIdentifier{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      EmptyRewritePragma{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      EmptyWhere{}               -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      -- TODO: linearity
      -- FixingQuantity _ q _       -> if null r then cosmeticHighlighting w else deadcodeHighlighting r
      --   where r = getRange q
      FixingRelevance [Char]
    _ Relevance
    q Relevance
    _      -> if Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r then TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting TCWarning
    w else Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Range
    r
        where r :: Range
    r = Relevance -> Range
    forall a. HasRange a => a -> Range
    getRange Relevance
    q
      FixingCohesion [Char]
    _ Cohesion
    q Cohesion
    _       -> if Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r then TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting TCWarning
    w else Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Range
    r
        where r :: Range
    r = Cohesion -> Range
    forall a. HasRange a => a -> Range
    getRange Cohesion
    q
      FixingPolarity [Char]
    _ PolarityModality
    q PolarityModality
    _       -> if Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r then TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting TCWarning
    w else Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Range
    r
        where r :: Range
    r = PolarityModality -> Range
    forall a. HasRange a => a -> Range
    getRange PolarityModality
    q
      IllformedAsClause{}        -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessPragma Range
    r Doc
    _          -> Range -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Range
    r
      UselessPublic{}            -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessHiding List1 ImportedName
    xs           -> (ImportedName -> HighlightingInfoBuilder)
    -> List1 ImportedName -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ImportedName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 ImportedName
    xs
      UselessInline{}            -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UselessPatternDeclarationForRecord{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessTactic{}            -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      ClashesViaRenaming NameOrModule
    _ Set1 Name
    xs    -> (Name -> HighlightingInfoBuilder)
    -> Set1 Name -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NESet a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Name -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting Set1 Name
    xs
        -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
        -- Should we have a different color?
      WrongInstanceDeclaration{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting TCWarning
    w
      InstanceWithExplicitArg{}    -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting TCWarning
    w
      InstanceNoOutputTypeName{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting TCWarning
    w
      InstanceArgWithExplicitArg{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting TCWarning
    w
      InversionDepthReached{}    -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      -- Andreas, 2020-03-21, issue #4456:
      -- Error warnings that do not have dedicated highlighting
      -- are highlighted as errors.
      InvalidCharacterLiteral{}             -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      SafeFlagPostulate{}                   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      SafeFlagPragma{}                      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      Warning
    SafeFlagWithoutKFlagPrimEraseEquality -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      InfectiveImport{}                     -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      CoInfectiveImport{}                   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      InvalidDisplayForm{}                  -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UnusedVariablesInDisplayForm List1 Name
    xs       -> (Name -> HighlightingInfoBuilder)
    -> List1 Name -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Name -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting List1 Name
    xs
      TooManyArgumentsToSort QName
    _ List1 (NamedArg Expr)
    args         -> List1 (NamedArg Expr) -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting List1 (NamedArg Expr)
    args
      Warning
    RewritesNothing                       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting TCWarning
    w
      WithClauseProjectionFixityMismatch NamedArg Pattern
    p ProjOrigin
    _ NamedArg DeBruijnPattern
    _ ProjOrigin
    _ -> NamedArg Pattern -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting NamedArg Pattern
    p
      Warning
    WithoutKFlagPrimEraseEquality -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      ConflictingPragmaOptions{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      DeprecationWarning{}       -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      UserWarning{}              -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      LibraryWarning{}           -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      ConfluenceCheckingIncompleteBecauseOfMeta{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      ConfluenceForCubicalNotSupported{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      RewriteNonConfluent{}      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteMaybeNonConfluent{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteAmbiguousRules{}    -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      RewriteMissingRule{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting TCWarning
    w
      IllegalRewriteRule QName
    x IllegalRewriteRuleReason
    _     -> QName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting QName
    x
      NotARewriteRule QName
    x IsAmbiguous
    _        -> QName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting QName
    x
      PragmaCompileErased{}      -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaCompileList{}        -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaCompileMaybe{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaCompileWrong{}       -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaCompileWrongName{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaCompileUnparsable{}  -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaExpectsDefinedSymbol{}
                                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaExpectsUnambiguousConstructorOrFunction{}
                                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PragmaExpectsUnambiguousProjectionOrFunction{}
                                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      NoMain{}                   -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      NotInScopeW{}              -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UnsupportedIndexedMatch{}  -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      AsPatternShadowsConstructorOrPatternSynonym{}
                                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      PatternShadowsConstructor{}-> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w  -- or mempty ?
      PlentyInHardCompileTimeMode QωOrigin
    o
                                 -> QωOrigin -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting QωOrigin
    o
      RecordFieldWarning RecordFieldWarning
    w       -> RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting RecordFieldWarning
    w
      OptionWarning OptionWarning
    w            -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      ParseWarning ParseWarning
    w             -> case ParseWarning
    w of
        Pa.MisplacedAttributes{}      -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.UnknownPolarity{}          -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.UnknownAttribute{}         -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.UnsupportedAttribute{}     -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.MultipleAttributes{}       -> ParseWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting ParseWarning
    w
        Pa.OverlappingTokensWarning{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
      MissingTypeSignatureForOpaque{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      NotAffectedByOpaque{}           -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UselessOpaque{}                 -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      UnfoldingWrongName QName
    x            -> QName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting QName
    x
      UnfoldTransparentName QName
    r         -> QName -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting QName
    r
      FaceConstraintCannotBeHidden{}  -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w
      FaceConstraintCannotBeNamed{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting TCWarning
    w

      HiddenNotInArgumentPosition{}   -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      InstanceNotInArgumentPosition{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      MacroInLetBindings{}            -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w
      AbstractInLetBindings{}         -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w

      NicifierIssue (DeclarationWarning CallStack
    _ DeclarationWarning'
    w) -> case DeclarationWarning'
    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{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyAbstract{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyConstructor{}               -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyInstance{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyMacro{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyMutual{}                    -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPostulate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPrimitive{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPrivate{}                   -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyGeneralize{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyField{}                     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        EmptyPolarityPragma{}            -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        HiddenGeneralize{}               -> HighlightingInfoBuilder
    forall a. Monoid a => a
    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{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessInstance{}                -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessMacro{}                   -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        UselessPrivate{}                 -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidCatchallPragma{}          -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidNoPositivityCheckPragma{} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidNoUniverseCheckPragma{}   -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidTerminationCheckPragma{}  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidCoverageCheckPragma{}     -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        InvalidConstructorBlock{}        -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting DeclarationWarning'
    w
        OpenImportAbstract{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting DeclarationWarning'
    w
        OpenImportPrivate{}              -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting DeclarationWarning'
    w
        SafeFlagEta                   {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagInjective             {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagNoCoverageCheck       {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagNoPositivityCheck     {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagNoUniverseCheck       {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagNonTerminating        {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagPolarity              {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        SafeFlagTerminating           {} -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        W.ShadowingInTelescope List1 (Name, List2 Range)
    nrs       -> ((Name, List2 Range) -> HighlightingInfoBuilder)
    -> List1 (Name, List2 Range) -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap
                                              (List2 Range -> HighlightingInfoBuilder
    shadowingTelHighlighting (List2 Range -> HighlightingInfoBuilder)
    -> ((Name, List2 Range) -> List2 Range)
    -> (Name, List2 Range)
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, List2 Range) -> List2 Range
    forall a b. (a, b) -> b
    snd)
                                              List1 (Name, List2 Range)
    nrs
        MissingDataDeclaration{}         -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting DeclarationWarning'
    w
        MissingDefinitions{}             -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting DeclarationWarning'
    w
        -- TODO: explore highlighting opportunities here!
        PolarityPragmasButNotPostulates{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        PragmaNoTerminationCheck{}        -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        PragmaCompiled{}                  -> DeclarationWarning' -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting DeclarationWarning'
    w
        UnknownFixityInMixfixDecl{}       -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        UnknownNamesInFixityDecl{}        -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty
        UnknownNamesInPolarityPragmas{}   -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

      -- Backends
      CustomBackendWarning{} -> HighlightingInfoBuilder
    forall a. Monoid a => a
    mempty

      -- Polarities
      TooManyPolarities QName
    _x PragmaPolarities
    occs -> PragmaPolarities -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting PragmaPolarities
    occs
      TopLevelPolarity{} -> TCWarning -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    errorWarningHighlighting TCWarning
    w

    recordFieldWarningHighlighting ::
      RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting :: RecordFieldWarning -> HighlightingInfoBuilder
    recordFieldWarningHighlighting = \case
      W.DuplicateFields List1 (Name, Range)
    xrs      -> List1 (Name, Range) -> HighlightingInfoBuilder
    dead List1 (Name, Range)
    xrs
      W.TooManyFields QName
    _q [Name]
    _ys List1 (Name, Range)
    xrs -> List1 (Name, Range) -> HighlightingInfoBuilder
    dead List1 (Name, Range)
    xrs
      where
      dead :: List1 (C.Name, Range) -> HighlightingInfoBuilder
      dead :: List1 (Name, Range) -> HighlightingInfoBuilder
    dead = NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (NonEmpty HighlightingInfoBuilder -> HighlightingInfoBuilder)
    -> (List1 (Name, Range) -> NonEmpty HighlightingInfoBuilder)
    -> List1 (Name, Range)
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, Range) -> HighlightingInfoBuilder)
    -> List1 (Name, Range) -> NonEmpty HighlightingInfoBuilder
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, Range) -> HighlightingInfoBuilder
    forall a. HasRange a => a -> HighlightingInfoBuilder
    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 :: List1 TerminationError -> HighlightingInfoBuilder
    terminationErrorHighlighting List1 TerminationError
    termErrs = HighlightingInfoBuilder
    functionDefs HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Monoid a => a -> a -> a
    `mappend` HighlightingInfoBuilder
    callSites
      where
        m :: Aspects
    m            = Aspects
    parserBased { otherAspects = Set.singleton TerminationProblem }
        functionDefs :: HighlightingInfoBuilder
    functionDefs = (QName -> HighlightingInfoBuilder)
    -> [QName] -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\QName
    x -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    bindingSite QName
    x) Aspects
    m) ([QName] -> HighlightingInfoBuilder)
    -> [QName] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
                       (TerminationError -> [QName]) -> List1 TerminationError -> [QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap TerminationError -> [QName]
    termErrFunctions List1 TerminationError
    termErrs
        callSites :: HighlightingInfoBuilder
    callSites    = (Range -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\Range
    r -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR Range
    r) Aspects
    m) ([Range] -> HighlightingInfoBuilder)
    -> [Range] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $
                       (TerminationError -> [Range]) -> List1 TerminationError -> [Range]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((CallInfo -> Range) -> [CallInfo] -> [Range]
    forall a b. (a -> b) -> [a] -> [b]
    map CallInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ([CallInfo] -> [Range])
    -> (TerminationError -> [CallInfo]) -> TerminationError -> [Range]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TerminationError -> [CallInfo]
    termErrCalls) List1 TerminationError
    termErrs
        bindingSite :: QName -> Range
    bindingSite  = Name -> Range
    A.nameBindingSite (Name -> Range) -> (QName -> Name) -> QName -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName

    -- | Generate syntax highlighting for not-strictly-positive inductive
    -- definitions.

    positivityErrorHighlighting ::
      I.QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting :: QName -> Seq OccursWhere -> HighlightingInfoBuilder
    positivityErrorHighlighting QName
    q Seq OccursWhere
    os =
      [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several (Range -> Ranges
    rToR (Range -> Ranges) -> [Range] -> [Ranges]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    : [Range]
    rs) Aspects
    m
      where
        rs :: [Range]
    rs = (OccursWhere -> Range) -> [OccursWhere] -> [Range]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(OccursWhere Range
    r Seq Where
    _ Seq Where
    _) -> Range
    r) (Seq OccursWhere -> [OccursWhere]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList Seq OccursWhere
    os)
        m :: Aspects
    m  = Aspects
    parserBased { otherAspects = Set.singleton PositivityProblem }

    deadcodeHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    deadcodeHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Range' a -> Range' a
    P.continuous (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton Deadcode }

    coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
    coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
    coverageErrorHighlighting Range
    r = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton CoverageProblem }

    shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
    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
      (Range -> HighlightingInfoBuilder)
    -> List1 Range -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (\Range
    r -> Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Range' a -> Range' a
    P.continuous Range
    r) Aspects
    m) (List1 Range -> HighlightingInfoBuilder)
    -> (List2 Range -> List1 Range)
    -> List2 Range
    -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List2 Range -> List1 Range
    forall a. List2 a -> List1 a
    List2.init
      where
      m :: Aspects
    m = Aspects
    parserBased { otherAspects =
                          Set.singleton H.ShadowingInTelescope }

    catchallHighlighting :: Range -> HighlightingInfoBuilder
    catchallHighlighting :: Range -> HighlightingInfoBuilder
    catchallHighlighting Range
    r = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton CatchallClause }

    cosmeticProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    cosmeticProblemHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where
        r :: Range
    r = a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a
        m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton CosmeticProblem }

    confluenceErrorHighlighting ::
      HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    confluenceErrorHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton ConfluenceProblem }

    instanceProblemHighlighting :: HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    instanceProblemHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r) Aspects
    m
      where
        r :: Range
    r = a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a
        m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton InstanceProblem }

    missingDefinitionHighlighting ::
      HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting :: forall a. HasRange a => a -> HighlightingInfoBuilder
    missingDefinitionHighlighting a
    a = Ranges -> Aspects -> HighlightingInfoBuilder
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    H.singleton (Range -> Ranges
    rToR (Range -> Ranges) -> Range -> Ranges
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ a -> Range
    forall a. HasRange a => a -> Range
    getRange a
    a) Aspects
    m
      where m :: Aspects
    m = Aspects
    parserBased { otherAspects = Set.singleton Aspect.MissingDefinition }

    -- | Generates and prints syntax highlighting information for unsolved
    -- meta-variables and certain unsolved constraints.

    printUnsolvedInfo :: TCM ()
    printUnsolvedInfo :: TCM ()
    printUnsolvedInfo = do
      info <- TCMT IO HighlightingInfoBuilder
    computeUnsolvedInfo

      printHighlightingInfo KeepHighlighting (convert info)

    computeUnsolvedInfo :: TCM HighlightingInfoBuilder
    computeUnsolvedInfo :: TCMT IO HighlightingInfoBuilder
    computeUnsolvedInfo = do
      (rs, metaInfo) <- TCM ([Ranges], HighlightingInfoBuilder)
    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 :: TCM ([Ranges], HighlightingInfoBuilder)
    computeUnsolvedMetaWarnings = do
      is <- TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    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 MetaId
    m = Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Bool
    isBlockedTerm MetaId
    m
      let notHasTwin MetaId
    m = Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Bool
    hasTwinMeta MetaId
    m
      ms <- filterM notHasTwin =<< filterM notBlocked =<< getOpenMetas

      let extend = (Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine)

      rs <- extend <$> mapM getMetaRange (ms \\ is)

      rs' <- extend <$> mapM getMetaRange is
      return $ (rs ++ rs', metasHighlighting' rs)

    metasHighlighting :: [Range] -> HighlightingInfoBuilder
    metasHighlighting :: [Range] -> HighlightingInfoBuilder
    metasHighlighting = [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' ([Ranges] -> HighlightingInfoBuilder)
    -> ([Range] -> [Ranges]) -> [Range] -> HighlightingInfoBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine)

    metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' :: [Ranges] -> HighlightingInfoBuilder
    metasHighlighting' [Ranges]
    rs =
      [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several ([Ranges] -> [Item [Ranges]]
    forall l. IsList l => l -> [Item l]
    List1.toList [Ranges]
    rs) Aspects
    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 :: [Ranges] -> TCMT IO HighlightingInfoBuilder
    computeUnsolvedConstraints [Ranges]
    ms = [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [Ranges]
    ms (Constraints -> HighlightingInfoBuilder)
    -> TCMT IO Constraints -> TCMT IO HighlightingInfoBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    getAllConstraints

    constraintsHighlighting ::
      [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting :: [Ranges] -> Constraints -> HighlightingInfoBuilder
    constraintsHighlighting [Ranges]
    ms Constraints
    cs =
      [Ranges] -> Aspects -> HighlightingInfoBuilder
    forall a hl.
    (IsBasicRangeMap a hl, Monoid hl) =>
    [Ranges] -> a -> hl
    several ((Ranges -> Bool) -> [Ranges] -> [Ranges]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Ranges -> Bool
    noOverlap ([Ranges] -> [Ranges]) -> [Ranges] -> [Ranges]
    forall a b. (a -> b) -> a -> b
    $ (Range -> Ranges) -> [Range] -> [Ranges]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Ranges
    rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine) [Range]
    rs)
              (Aspects
    parserBased { otherAspects = Set.singleton UnsolvedConstraint })
      where
      noOverlap :: Ranges -> Bool
    noOverlap Ranges
    r = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Ranges -> Bool) -> [Ranges] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Ranges -> Ranges -> Bool
    overlappings (Ranges -> Ranges -> Bool) -> Ranges -> Ranges -> Bool
    forall a b. (a -> b) -> a -> b
    $ Ranges
    r) ([Ranges] -> Bool) -> [Ranges] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Ranges]
    ms
      -- get ranges of interesting unsolved constraints
      rs :: [Range]
    rs = ((Closure Constraint -> Maybe Range)
    -> [Closure Constraint] -> [Range]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    `mapMaybe` ((ProblemConstraint -> Closure Constraint)
    -> Constraints -> [Closure Constraint]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> Closure Constraint
    theConstraint Constraints
    cs)) ((Closure Constraint -> Maybe Range) -> [Range])
    -> (Closure Constraint -> Maybe Range) -> [Range]
    forall a b. (a -> b) -> a -> b
    $ \case
        Closure{ clValue :: forall a. Closure a -> a
    clValue = IsEmpty Range
    r Type
    t           } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    r
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = ValueCmp{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = ElimCmp{}  } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = SortCmp{}  } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = LevelCmp{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure{ clEnv :: forall a. Closure a -> TCEnv
    clEnv = TCEnv
    e, clValue :: forall a. Closure a -> a
    clValue = CheckSizeLtSat{} } -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    forall a. HasRange a => a -> Range
    getRange (TCEnv -> Range
    envRange TCEnv
    e)
        Closure Constraint
    _ -> Maybe Range
    forall a. Maybe a
    Nothing

    -- * Disambiguation of constructors and projections.

    storeDisambiguatedField :: A.QName -> TCM ()
    storeDisambiguatedField :: QName -> TCM ()
    storeDisambiguatedField = NameKind -> QName -> TCM ()
    storeDisambiguatedName NameKind
    Field

    storeDisambiguatedProjection :: A.QName -> TCM ()
    storeDisambiguatedProjection :: QName -> TCM ()
    storeDisambiguatedProjection = QName -> TCM ()
    storeDisambiguatedField

    storeDisambiguatedConstructor :: Induction -> A.QName -> TCM ()
    storeDisambiguatedConstructor :: Induction -> QName -> TCM ()
    storeDisambiguatedConstructor Induction
    i = NameKind -> QName -> TCM ()
    storeDisambiguatedName (NameKind -> QName -> TCM ()) -> NameKind -> QName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Induction -> NameKind
    Constructor Induction
    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 :: NameKind -> QName -> TCM ()
    storeDisambiguatedName NameKind
    k QName
    q = do
      QName -> TCM ()
    forall (m :: * -> *).
    (MonadWarning m, ReadTCState m) =>
    QName -> m ()
    raiseWarningsOnUsage QName
    q
      Maybe Key -> (Key -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Range -> Maybe Key
    forall {b} {a}. Num b => Range' a -> Maybe b
    start (Range -> Maybe Key) -> Range -> Maybe Key
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q) ((Key -> TCM ()) -> TCM ()) -> (Key -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Key
    i ->
        Lens' TCState (IntMap DisambiguatedName)
    -> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (IntMap DisambiguatedName -> f (IntMap DisambiguatedName))
    -> TCState -> f TCState
    Lens' TCState (IntMap DisambiguatedName)
    stDisambiguatedNames ((IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ())
    -> (IntMap DisambiguatedName -> IntMap DisambiguatedName) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Key
    -> DisambiguatedName
    -> IntMap DisambiguatedName
    -> IntMap DisambiguatedName
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (DisambiguatedName
     -> IntMap DisambiguatedName -> IntMap DisambiguatedName)
    -> DisambiguatedName
    -> IntMap DisambiguatedName
    -> IntMap DisambiguatedName
    forall a b. (a -> b) -> a -> b
    $ NameKind -> QName -> DisambiguatedName
    DisambiguatedName NameKind
    k QName
    q
      where
      start :: Range' a -> Maybe b
    start Range' a
    r = Word32 -> b
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32 -> b) -> (Position' () -> Word32) -> Position' () -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Position' () -> Word32
    forall a. Position' a -> Word32
    P.posPos (Position' () -> b) -> Maybe (Position' ()) -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Range' a -> Maybe (Position' ())
    forall a. Range' a -> Maybe (Position' ())
    P.rStart' Range' a
    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 :: [Name] -> [QName] -> TCM ()
    disambiguateRecordFields [Name]
    cxs [QName]
    axs = [Name] -> (Name -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Name]
    cxs ((Name -> TCM ()) -> TCM ()) -> (Name -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Name
    cx -> do
      Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ((QName -> Bool) -> [QName] -> Maybe QName
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Name
    cx Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Name -> Bool) -> (QName -> Name) -> QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Name
    A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName) [QName]
    axs) (() -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    ax -> do
        QName -> TCM ()
    storeDisambiguatedField QName
    ax{ A.qnameName = (A.qnameName ax) { A.nameConcrete = cx } }