Missing highlighting when interleaved mutual is used

[nad]

The last two occurrences of D are not highlighted properly:

interleaved mutual

  data D : Set where

  data D where
    c : D

If non-interactive highlighting is used, then you get proper highlighting the first time the module is loaded, but not when it is reloaded. If interactive highlighting is used, then you do not get proper highlighting the first or the second time.

[nad]

I noticed that the constructor c is also not highlighted correctly.

The LaTeX backend also produces incorrect output (if the code above is placed in a code environment). The following code corresponds to the last two lines of Agda code above:

\>[2]\AgdaKeyword{data}\ D\ \AgdaKeyword{where}
\ \ \ \ c\ \AgdaSymbol{:}\ D\<%

However, with --only-scope-checking you get the following code:

\>[2]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{D}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaInductiveConstructor{c}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{D}\<%

The reason for this discrepancy is presumably that when --only-scope-checking is used, then the result of the preliminary round of syntax highlighting (before the type-checker has disambiguated things) is stored in the state (onlyScope is True):

agda/src/full/Agda/Interaction/Imports.hs

Lines 1008 to 1009 in fc4e2fa

	ifTopLevelAndHighlightingLevelIsOr NonInteractive onlyScope $
	mapM_ (\ d -> generateAndPrintSyntaxInfo d Partial onlyScope) ds

So, why is the code not highlighted in the final round? Consider the following code:

agda/src/full/Agda/TypeChecking/Rules/Decl.hs

Lines 387 to 409 in fc4e2fa

	Bench.billTo [Bench.Highlighting] $ case d of
	A.Axiom{} -> highlight d
	A.Field{} -> __IMPOSSIBLE__
	A.Primitive{} -> highlight d
	A.Mutual i ds -> mapM_ (highlight_ DoHighlightModuleContents) $ deepUnscopeDecls ds
	A.Apply{} -> highlight d
	A.Import{} -> highlight d
	A.Pragma{} -> highlight d
	A.ScopedDecl{} -> return ()
	A.FunDef{} -> highlight d
	A.DataDef{} -> highlight d
	A.DataSig{} -> highlight d
	A.Open{} -> highlight d
	A.PatternSynDef{} -> highlight d
	A.Generalize{} -> highlight d
	A.UnquoteDecl{} -> highlight d
	A.UnquoteDef{} -> highlight d
	A.UnquoteData{} -> highlight d
	A.Section i x tel ds -> do
	highlight (A.Section i x tel [])
	when (hlmod == DoHighlightModuleContents) $ mapM_ (highlight_ hlmod) (deepUnscopeDecls ds)
	A.RecSig{} -> highlight d
	A.RecDef i x uc dir ps tel cs -> highlight (A.RecDef i x uc dir A.noDataDefParams dummy cs)

If return () is replaced by highlight d, then the code in the OP is highlighted correctly (and also the code from issue #6276). However, some test cases are broken. Why does the clause for A.ScopedDecl use return ()? Presumably because the declarations contained in such a declaration are checked separately:

agda/src/full/Agda/TypeChecking/Rules/Decl.hs

Line 155 in fc4e2fa

A.ScopedDecl scope ds -> none $ setScope scope >> mapM_ checkDeclCached ds

Apparently some declarations can escape the generation of highlighting information. The abstract syntax corresponding to the code in the OP has the following structure:

Section [ScopedDecl [Mutual [ScopedDecl [DataSig],ScopedDecl [DataDef]]]]

Syntax highlighting information is generated for the following parts: DataSig, Section []. Why is the DataSig treated differently from the DataDef? Presumably because it does not have a range:

agda/src/full/Agda/Interaction/Highlighting/Generate.hs

Line 130 in fc4e2fa

generateAndPrintSyntaxInfo decl _ _ | null $ getRange decl = return ()

If that line is removed, then proper highlighting is generated for the code in the OP (but not for the code from issue #6276). It seems as if some code constructs a DataDef without setting its range properly, and I found the culprit:

agda/src/full/Agda/Syntax/Concrete/Definitions/Types.hs

Lines 176 to 179 in fc4e2fa

	InterleavedData i d@(NiceDataSig _ acc abs pc uc _ pars _) ds ->
	let fpars = concatMap dropTypeAndModality pars
	ddef = NiceDataDef noRange UserWritten abs pc uc k fpars
	in (i,d) : maybe [] (\ (j, dss) -> [(j, ddef (sconcat (List1.reverse dss)))]) ds

I tried to preserve the ranges here, and that seems to fix the problem.