Fix bug where highlighting is not kept when the file has a type error…

… and imports some other file (#2959)

Example file:
```
module error;

import empty; -- error only happens if we have at least one import

type T := t;

x : T := t t; -- type error
```
If one loads this file into emacs (or vscode) they'll get a type error
as expected, but name colors and go-to information is lost, which is
annoying. This pr fixes this.
I'm not sure why, but this bug only occurs when there is at least one
import.

app/Commands/Dev/Highlight.hs

@@ -13,3 +13,4 @@ runCommand HighlightOptions {..} = silenceProgressLog . runPipelineOptions $ do
       inputFile
       <$> runPipelineHighlight entry upToInternalTyped
   renderStdOutRaw (Highlight.highlight _highlightBackend hinput)
+  newline

src/Juvix/Compiler/Concrete/Data/Highlight.hs

@@ -1,14 +1,14 @@
 module Juvix.Compiler.Concrete.Data.Highlight
   ( module Juvix.Compiler.Concrete.Data.Highlight,
-    module Juvix.Compiler.Concrete.Data.Highlight.Input,
+    module Juvix.Compiler.Concrete.Data.Highlight.Builder,
     module Juvix.Compiler.Concrete.Data.Highlight.Properties,
   )
 where
 
 import Data.Aeson qualified as Aeson
 import Data.ByteString.Lazy qualified as ByteString
 import Data.Text.Encoding qualified as Text
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Data.Highlight.PrettyJudoc
 import Juvix.Compiler.Concrete.Data.Highlight.Properties
 import Juvix.Compiler.Concrete.Data.Highlight.RenderEmacs
@@ -40,11 +40,11 @@ buildProperties :: HighlightInput -> LocProperties
 buildProperties HighlightInput {..} =
   LocProperties
     { _propertiesFace =
-        map goFaceParsedItem _highlightParsed
+        map goFaceParsedItem _highlightParsedItems
           <> mapMaybe goFaceName _highlightNames
           <> map goFaceError _highlightErrors,
       _propertiesGoto = map goGotoProperty _highlightNames,
-      _propertiesDoc = mapMaybe (goDocProperty _highlightDoc _highlightTypes) _highlightNames
+      _propertiesDoc = mapMaybe (goDocProperty _highlightDocTable _highlightTypes) _highlightNames
     }
 
 goFaceError :: Interval -> WithLoc PropertyFace

src/Juvix/Compiler/Concrete/Data/Highlight/Builder.hs

@@ -0,0 +1,48 @@
+module Juvix.Compiler.Concrete.Data.Highlight.Builder
+  ( module Juvix.Compiler.Concrete.Data.Highlight.Input,
+    module Juvix.Compiler.Concrete.Data.ParsedItem,
+    module Juvix.Compiler.Concrete.Data.Highlight.Builder,
+  )
+where
+
+import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.ParsedItem
+import Juvix.Compiler.Concrete.Data.ScopedName
+import Juvix.Compiler.Concrete.Language.Base
+import Juvix.Compiler.Internal.Language qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
+import Juvix.Prelude
+
+data HighlightBuilder :: Effect where
+  HighlightError :: Interval -> HighlightBuilder m ()
+  HighlightDoc :: NameId -> Maybe (Judoc 'Scoped) -> HighlightBuilder m ()
+  HighlightName :: AName -> HighlightBuilder m ()
+  HighlightParsedItem :: ParsedItem -> HighlightBuilder m ()
+  HighlightType :: NameId -> Internal.Expression -> HighlightBuilder m ()
+
+makeSem ''HighlightBuilder
+
+runHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput, a)
+runHighlightBuilder = reinterpret (runStateShared emptyHighlightInput) $ \case
+  HighlightError e -> modifyShared (over highlightErrors (e :))
+  HighlightName a -> modifyShared (over (highlightNames) (a :))
+  HighlightParsedItem p -> modifyShared (over (highlightParsedItems) (p :))
+  HighlightDoc k md -> modifyShared (set (highlightDocTable . at k) md)
+  HighlightType uid ty -> modifyShared (set (highlightTypes . typesTable . at uid) (Just ty))
+
+ignoreHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r a
+ignoreHighlightBuilder = fmap snd . runHighlightBuilder
+
+runJuvixError :: (Members '[HighlightBuilder] r) => Sem (Error JuvixError ': r) a -> Sem r (Either JuvixError a)
+runJuvixError m = do
+  x <- runError m
+  case x of
+    r@Right {} -> return r
+    l@(Left err) -> do
+      let errs =
+            (^. genericErrorIntervals)
+              . run
+              . runReader defaultGenericOptions
+              $ genericError err
+      mapM_ highlightError errs
+      return l

src/Juvix/Compiler/Concrete/Data/Highlight/Input.hs

@@ -6,13 +6,14 @@ where
 
 import Juvix.Compiler.Concrete.Data.ParsedItem
 import Juvix.Compiler.Concrete.Data.ScopedName
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
 import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as Scoped
 import Juvix.Prelude
 
 data HighlightInput = HighlightInput
-  { _highlightParsed :: [ParsedItem],
-    _highlightDoc :: Scoped.DocTable,
+  { _highlightParsedItems :: [ParsedItem],
+    _highlightDocTable :: Scoped.DocTable,
     _highlightNames :: [AName],
     _highlightTypes :: Internal.TypesTable,
     _highlightErrors :: [Interval]
@@ -23,8 +24,8 @@ makeLenses ''HighlightInput
 emptyHighlightInput :: HighlightInput
 emptyHighlightInput =
   HighlightInput
-    { _highlightParsed = [],
-      _highlightDoc = mempty,
+    { _highlightParsedItems = [],
+      _highlightDocTable = mempty,
       _highlightNames = [],
       _highlightTypes = mempty,
       _highlightErrors = []
@@ -34,26 +35,8 @@ filterInput :: Path Abs File -> HighlightInput -> HighlightInput
 filterInput absPth HighlightInput {..} =
   HighlightInput
     { _highlightNames = filterByLoc absPth _highlightNames,
-      _highlightParsed = filterByLoc absPth _highlightParsed,
+      _highlightParsedItems = filterByLoc absPth _highlightParsedItems,
       _highlightErrors = filterByLoc absPth _highlightErrors,
       _highlightTypes,
-      _highlightDoc
+      _highlightDocTable
     }
-
-type HighlightBuilder = State HighlightInput
-
-runHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput, a)
-runHighlightBuilder = runState emptyHighlightInput
-
-ignoreHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r a
-ignoreHighlightBuilder = evalState emptyHighlightInput
-
-runJuvixError :: (Members '[HighlightBuilder] r) => Sem (Error JuvixError ': r) a -> Sem r (Either JuvixError a)
-runJuvixError m = do
-  x <- runError m
-  case x of
-    r@Right {} -> return r
-    l@(Left err) -> do
-      let errs = run (runReader defaultGenericOptions (genericError err)) ^. genericErrorIntervals
-      modify (over highlightErrors (errs ++))
-      return l

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -2,7 +2,7 @@ module Juvix.Compiler.Concrete.Data.InfoTableBuilder where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Data.Scope
 import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
@@ -40,9 +40,6 @@ registerBuiltin b sym = registerBuiltin' (toBuiltinPrim b) sym
 getBuiltinSymbol :: (IsBuiltin a, Member InfoTableBuilder r) => Interval -> a -> Sem r S.Symbol
 getBuiltinSymbol i = getBuiltinSymbol' i . toBuiltinPrim
 
-registerDoc :: forall r. (Members '[HighlightBuilder, State InfoTable] r) => NameId -> Maybe (Judoc 'Scoped) -> Sem r ()
-registerDoc k md = modify (set (highlightDoc . at k) md)
-
 evalInfoTableBuilder :: (Members '[Error ScoperError, HighlightBuilder] r) => InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r a
 evalInfoTableBuilder ini = fmap snd . runInfoTableBuilder ini
 
@@ -52,28 +49,25 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
     let j = d ^. axiomDoc
      in do
           modify' (over infoAxioms (HashMap.insert (d ^. axiomName . nameId) d))
-          registerDoc (d ^. axiomName . nameId) j
+          highlightDoc (d ^. axiomName . nameId) j
   RegisterConstructor c ->
     let j = c ^. constructorDoc
      in do
           modify' (over infoConstructors (HashMap.insert (c ^. constructorName . nameId) c))
-          registerDoc (c ^. constructorName . nameId) j
+          highlightDoc (c ^. constructorName . nameId) j
   RegisterInductive ity ->
     let j = ity ^. inductiveDoc
      in do
           modify' (over infoInductives (HashMap.insert (ity ^. inductiveName . nameId) ity))
-          registerDoc (ity ^. inductiveName . nameId) j
+          highlightDoc (ity ^. inductiveName . nameId) j
   RegisterFunctionDef f ->
     let j = f ^. signDoc
      in do
           modify' (over infoFunctions (HashMap.insert (f ^. signName . nameId) f))
-          registerDoc (f ^. signName . nameId) j
-  RegisterName n -> do
-    modify (over highlightNames (cons (S.anameFromName n)))
-  RegisterScopedIden n -> do
-    modify (over highlightNames (cons (anameFromScopedIden n)))
-  RegisterModuleDoc uid doc -> do
-    registerDoc uid doc
+          highlightDoc (f ^. signName . nameId) j
+  RegisterName n -> highlightName (S.anameFromName n)
+  RegisterScopedIden n -> highlightName (anameFromScopedIden n)
+  RegisterModuleDoc uid doc -> highlightDoc uid doc
   RegisterFixity f -> do
     let sid = f ^. fixityDefSymbol . S.nameId
     modify (over infoFixities (HashMap.insert sid f))
@@ -83,7 +77,7 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
   RegisterPrecedence l h ->
     modify (over infoPrecedenceGraph (HashMap.alter (Just . HashSet.insert h . fromMaybe mempty) l))
   RegisterHighlightDoc fid doc ->
-    registerDoc fid doc
+    highlightDoc fid doc
   RegisterNameSig uid sig ->
     modify (over infoNameSigs (HashMap.insert uid sig))
   RegisterConstructorSig uid sig ->

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -401,7 +401,6 @@ instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where
 instance (SingI s) => PrettyPrint (DoLet s) where
   ppCode DoLet {..} = do
     let letFunDefs' = blockIndent (ppBlock _doLetStatements)
-    -- blockIndent d = hardline <> indent d <> line
     ppCode _doLetKw
       <> letFunDefs'
       <> ppCode _doLetInKw

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -10,7 +10,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Data.List.NonEmpty qualified as NonEmpty
 import GHC.Base (maxInt, minInt)
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Data.InfoTableBuilder
 import Juvix.Compiler.Concrete.Data.Name qualified as N
 import Juvix.Compiler.Concrete.Data.NameSignature

src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs

@@ -1,6 +1,6 @@
 module Juvix.Compiler.Concrete.Translation.FromSource.ParserResultBuilder where
 
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.ParserState
@@ -84,7 +84,7 @@ runParserResultBuilder s =
   reinterpret (runState s) $ \case
     RegisterImport i -> modify' (over parserStateImports (i :))
     RegisterItem i -> do
-      modify (over highlightParsed (i :))
+      highlightParsedItem i
       registerItem' i
     RegisterSpaceSpan g -> do
       modify' (over parserStateComments (g :))

src/Juvix/Compiler/Concrete/Translation/ImportScanner/Megaparsec.hs

@@ -4,7 +4,7 @@ module Juvix.Compiler.Concrete.Translation.ImportScanner.Megaparsec
   )
 where
 
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.ParserState

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -3,7 +3,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal
   )
 where
 
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
 import Juvix.Compiler.Internal.Data.InfoTable as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context as Internal

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -125,7 +125,7 @@ registerConstructor ctr = do
 registerNameIdType :: (Members '[HighlightBuilder, ResultBuilder] r) => NameId -> Expression -> Sem r ()
 registerNameIdType uid ty = do
   addIdenType uid ty
-  modify (over (highlightTypes . typesTable) (HashMap.insert uid ty))
+  highlightType uid ty
 
 checkCoercionCycles ::
   (Members '[ResultBuilder, Error TypeCheckerError] r) =>

src/Juvix/Compiler/Pipeline.hs

@@ -22,7 +22,7 @@ import Juvix.Compiler.Casm.Data.Builtins qualified as Casm
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
 import Juvix.Compiler.Casm.Pipeline qualified as Casm
 import Juvix.Compiler.Casm.Translation.FromReg qualified as Casm
-import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser

src/Juvix/Compiler/Pipeline/Driver.hs

@@ -56,15 +56,15 @@ processModule = cacheGet
 
 evalModuleInfoCache ::
   forall r a.
-  (Members '[TaggedLock, TopModuleNameChecker, Error JuvixError, Files, PathResolver] r) =>
+  (Members '[TaggedLock, HighlightBuilder, TopModuleNameChecker, Error JuvixError, Files, PathResolver] r) =>
   Sem (ModuleInfoCache ': JvoCache ': r) a ->
   Sem r a
 evalModuleInfoCache = evalJvoCache . evalCacheEmpty processModuleCacheMiss
 
 -- | Used for parallel compilation
 evalModuleInfoCacheSetup ::
   forall r a.
-  (Members '[TaggedLock, TopModuleNameChecker, Error JuvixError, Files, PathResolver] r) =>
+  (Members '[TaggedLock, HighlightBuilder, TopModuleNameChecker, Error JuvixError, Files, PathResolver] r) =>
   (EntryIndex -> Sem (ModuleInfoCache ': JvoCache ': r) ()) ->
   Sem (ModuleInfoCache ': JvoCache ': r) a ->
   Sem r a
@@ -75,6 +75,7 @@ processModuleCacheMiss ::
   ( Members
       '[ ModuleInfoCache,
          TaggedLock,
+         HighlightBuilder,
          TopModuleNameChecker,
          Error JuvixError,
          Files,
@@ -240,7 +241,7 @@ processImports imports = do
 
 processModuleToStoredCore ::
   forall r.
-  (Members '[ModuleInfoCache, PathResolver, TopModuleNameChecker, Error JuvixError, Files] r) =>
+  (Members '[ModuleInfoCache, PathResolver, HighlightBuilder, TopModuleNameChecker, Error JuvixError, Files] r) =>
   Text ->
   EntryPoint ->
   Sem r (PipelineResult Store.ModuleInfo)
@@ -262,10 +263,10 @@ processModuleToStoredCore sha256 entry = over pipelineResult mkModuleInfo <$> pr
 
 processFileToStoredCore ::
   forall r.
-  (Members '[ModuleInfoCache, PathResolver, TopModuleNameChecker, Error JuvixError, Files] r) =>
+  (Members '[ModuleInfoCache, HighlightBuilder, PathResolver, TopModuleNameChecker, Error JuvixError, Files] r) =>
   EntryPoint ->
   Sem r (PipelineResult Core.CoreResult)
-processFileToStoredCore entry = ignoreHighlightBuilder . runReader entry $ do
+processFileToStoredCore entry = runReader entry $ do
   res <- processFileUpToParsing entry
   let pkg = entry ^. entryPointPackage
   mid <- runReader pkg (getModuleId (res ^. pipelineResult . Parser.resultModule . modulePath . to topModulePathKey))

src/Juvix/Compiler/Pipeline/DriverParallel.hs

@@ -9,6 +9,7 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Effectful.Concurrent
+import Juvix.Compiler.Concrete.Data.Highlight.Builder (HighlightBuilder)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource.TopModuleNameChecker
 import Juvix.Compiler.Concrete.Translation.ImportScanner (ImportScanStrategy)
@@ -151,6 +152,7 @@ evalModuleInfoCache ::
   forall r a.
   ( Members
       '[ Reader EntryPoint,
+         HighlightBuilder,
          IOE,
          ProgressLog,
          Reader ImportTree,

src/Juvix/Compiler/Pipeline/Repl.hs

@@ -168,6 +168,7 @@ compileReplInputIO fp txt = do
     . runLoggerIO defaultLoggerOptions
     . runReader defaultNumThreads
     . evalInternet hasInternet
+    . ignoreHighlightBuilder
     . runTaggedLockPermissive
     . runLogIO
     . runFilesIO

src/Juvix/Compiler/Pipeline/Run.hs

@@ -67,9 +67,7 @@ runIOEitherHelper ::
   EntryPoint ->
   Sem (PipelineEff r) a ->
   Sem r (HighlightInput, (Either JuvixError (ResolverState, PipelineResult a)))
-runIOEitherHelper entry a =
-  runIOEitherPipeline' entry $ do
-    processFileUpTo a
+runIOEitherHelper entry = runIOEitherPipeline' entry . processFileUpTo
 
 runIOEitherPipeline ::
   forall a r.
@@ -147,6 +145,7 @@ evalModuleInfoCacheHelper ::
          TaggedLock,
          TopModuleNameChecker,
          Error JuvixError,
+         HighlightBuilder,
          PathResolver,
          Reader ImportScanStrategy,
          Reader NumThreads,

src/Juvix/Formatter.hs

@@ -2,7 +2,7 @@
 
 module Juvix.Formatter where
 
-import Juvix.Compiler.Concrete.Data.Highlight.Input (ignoreHighlightBuilder)
+import Juvix.Compiler.Concrete.Data.Highlight.Builder (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print (ppOutDefault)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping (ScoperResult, getModuleId, scopeCheck)