Only grab public IfaceDecls from other modules.

src/Cryptol/ModuleSystem/Env.hs

@@ -278,23 +278,21 @@ modContextOf mname me =
      let localIface  = lmInterface lm
          localNames  = lmNamingEnv lm
 
-         -- XXX: do we want only public ones here?
-         loadedDecls = map (ifDefines . lmInterface)
+         loadedPublicDecls = map getPublicDecls
                      $ getLoadedModules (meLoadedModules me)
 
          params = ifParams localIface
      pure ModContext
        { mctxParams   = if Map.null params then NoParams
                                            else FunctorParams params
        , mctxExported = ifsPublic (ifNames localIface)
-       , mctxDecls    = mconcat (ifDefines localIface : loadedDecls)
+       , mctxDecls    = mconcat (ifDefines localIface : loadedPublicDecls)
        , mctxNames    = localNames
        , mctxNameDisp = R.toNameDisp localNames
        }
   `mplus`
   do lm <- lookupSignature mname me
      let localNames  = lmNamingEnv lm
-         -- XXX: do we want only public ones here?
          loadedDecls = map (ifDefines . lmInterface)
                      $ getLoadedModules (meLoadedModules me)
      pure ModContext
@@ -304,6 +302,12 @@ modContextOf mname me =
        , mctxNames    = localNames
        , mctxNameDisp = R.toNameDisp localNames
        }
+  where getPublicDecls :: LoadedModule -> IfaceDecls
+        getPublicDecls lm = 
+          do let allDecls = ifDefines (lmInterface lm)
+                 publicNames = ifsPublic (ifNames (lmInterface lm))
+                 publicDecls = filterIfaceDecls (`Set.member` publicNames) allDecls
+             publicDecls
 
 
 

tests/issues/issue1621/a.cry

@@ -0,0 +1,5 @@
+module a where
+
+private
+
+property x = True

tests/issues/issue1621/b.cry

@@ -0,0 +1,3 @@
+module b where
+
+import a

tests/issues/issue1621/issue1621.icry

@@ -0,0 +1,7 @@
+:m a
+x
+:m b
+x
+:check x
+:check a::x
+:check

tests/issues/issue1621/issue1621.icry.stdout

@@ -0,0 +1,17 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module a
+True
+Loading module Cryptol
+Loading module a
+Loading module b
+
+[error] at issue1621.icry:4:1--4:2
+    Value not in scope: x
+
+[error] at issue1621.icry:5:8--5:9
+    Value not in scope: x
+
+[error] at issue1621.icry:6:8--6:12
+    Value not in scope: a::x
+There are no properties in scope.