Fix reachability analysis with imports in unreachable nested modules (#2062)

* Closes #2005

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs

@@ -10,9 +10,13 @@ import Juvix.Prelude
 -- adjacency set representation
 type DependencyGraph = HashMap Name (HashSet Name)
 
-type StartNodes = HashSet Name
+newtype VisitedModules = VisitedModules
+  { _visitedModulesSet :: HashSet Name
+  }
 
-type VisitedModules = HashSet Name
+makeLenses ''VisitedModules
+
+type StartNodes = HashSet Name
 
 type ExportsTable = HashSet NameId
 
@@ -40,7 +44,7 @@ buildDependencyInfoHelper tbl m = createDependencyInfo graph startNodes
     graph :: DependencyGraph
     (startNodes, graph) =
       run $
-        evalState (HashSet.empty :: VisitedModules) $
+        evalState (VisitedModules mempty) $
           runState HashSet.empty $
             execState HashMap.empty $
               runReader tbl m
@@ -86,8 +90,8 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
 guardNotVisited :: (Member (State VisitedModules) r) => Name -> Sem r () -> Sem r ()
 guardNotVisited n cont =
   unlessM
-    (HashSet.member n <$> get)
-    (modify (HashSet.insert n) >> cont)
+    (HashSet.member n . (^. visitedModulesSet) <$> get)
+    (modify (over visitedModulesSet (HashSet.insert n)) >> cont)
 
 goModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r) => Module -> Sem r ()
 goModule m = do

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

@@ -3,16 +3,15 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability wh
 import Juvix.Compiler.Abstract.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
--- import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as MicroTyped
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as MicroArity
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as MicroTyped
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed
 import Juvix.Prelude
 
-filterUnreachable :: MicroTyped.InternalTypedResult -> MicroTyped.InternalTypedResult
-filterUnreachable r = r {MicroTyped._resultModules = modules'}
+filterUnreachable :: Typed.InternalTypedResult -> Typed.InternalTypedResult
+filterUnreachable r = r {Typed._resultModules = modules'}
   where
-    depInfo = r ^. (MicroTyped.resultInternalArityResult . MicroArity.resultInternalResult . resultDepInfo)
-    modules = r ^. MicroTyped.resultModules
+    depInfo = r ^. (Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo)
+    modules = r ^. Typed.resultModules
     modules' = run $ runReader depInfo (mapM goModule modules)
 
 askIsReachable :: Member (Reader NameDependencyInfo) r => Name -> Sem r Bool
@@ -43,6 +42,4 @@ goStatement s = case s of
   StatementInclude i -> do
     m <- goModule (i ^. includeModule)
     return (Just (StatementInclude i {_includeModule = m}))
-  StatementModule m -> do
-    m' <- StatementModule <$> goModule m
-    returnIfReachable (m ^. moduleName) m'
+  StatementModule m -> Just . StatementModule <$> goModule m

test/Internal/Eval/Positive.hs

@@ -188,5 +188,10 @@ tests =
       "Case expression"
       $(mkRelDir ".")
       $(mkRelFile "Case.juvix")
-      $(mkRelFile "out/Case.out")
+      $(mkRelFile "out/Case.out"),
+    PosTest
+      "Import a module containing a nested module"
+      $(mkRelDir "NestedModuleScope")
+      $(mkRelFile "Import.juvix")
+      $(mkRelFile "out/NestedModuleScope.out")
   ]

tests/Internal/positive/NestedModuleScope/Base.juvix

@@ -0,0 +1,5 @@
+module Base;
+
+module NestedBase;
+  open import Base2 public;
+end;

tests/Internal/positive/NestedModuleScope/Base2.juvix

@@ -0,0 +1,3 @@
+module Base2;
+
+type Foo := foo : Foo;

tests/Internal/positive/NestedModuleScope/Import.juvix

@@ -0,0 +1,7 @@
+module Import;
+
+open import Base;
+open import Base2;
+
+main : Foo;
+main := foo;

tests/Internal/positive/NestedModuleScope/out/NestedModuleScope.out

@@ -0,0 +1 @@
+foo