Merge pull request #1650 from GaloisInc/iss-1649

#1649
GaloisInc · Apr 1, 2024 · a849b97 · a849b97
2 parents 2b0812f + fe5e9bd
commit a849b97
Show file tree

Hide file tree

Showing 12 changed files with 37 additions and 41 deletions.
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
@@ -278,21 +278,23 @@ modContextOf mname me =
      let localIface  = lmInterface lm
          localNames  = lmNamingEnv lm
 
-         loadedPublicDecls = map getPublicDecls
+         -- XXX: do we want only public ones here?
+         loadedDecls = map (ifDefines . lmInterface)
                      $ 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 : loadedPublicDecls)
+       , mctxDecls    = mconcat (ifDefines localIface : loadedDecls)
        , 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
@@ -302,12 +304,6 @@ 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
 
 
 

diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
@@ -772,7 +772,7 @@ lookupVar x =
               Just a -> pure (ExtVar a)
               Nothing ->
                 do mp <- IM $ asks iVars
-                   panic "lookupVar" $ [ "Undefined vairable"
+                   panic "lookupVar" $ [ "Undefined variable"
                                      , show x
                                      , "IVARS"
                                      ] ++ map (show . debugShowUniques . pp) (Map.keys mp)

diff --git a/tests/issues/issue1621/a.cry b/tests/issues/issue1621/a.cry
diff --git a/tests/issues/issue1621/b.cry b/tests/issues/issue1621/b.cry
diff --git a/tests/issues/issue1621/issue1621.icry b/tests/issues/issue1621/issue1621.icry
diff --git a/tests/issues/issue1621/issue1621.icry.stdout b/tests/issues/issue1621/issue1621.icry.stdout
diff --git a/tests/issues/issue1649/A.cry b/tests/issues/issue1649/A.cry
@@ -0,0 +1,5 @@
+// A.cry
+module A where
+
+submodule B = BFunctor where
+  type BTy = ()
diff --git a/tests/issues/issue1649/BFunctor.cry b/tests/issues/issue1649/BFunctor.cry
@@ -0,0 +1,9 @@
+// BFunctor.cry
+module BFunctor where
+
+import interface BInterface as BI
+
+type BTy = BI::BTy
+
+b : BTy -> ()
+b _ = ()
diff --git a/tests/issues/issue1649/BInterface.cry b/tests/issues/issue1649/BInterface.cry
@@ -0,0 +1,4 @@
+// BInterface.cry
+interface module BInterface where
+
+type BTy : *
diff --git a/tests/issues/issue1649/Test.cry b/tests/issues/issue1649/Test.cry
@@ -0,0 +1,5 @@
+// Test.cry
+module Test where
+
+import A as A
+import submodule A::B as B
diff --git a/tests/issues/issue1649/issue1649.icry b/tests/issues/issue1649/issue1649.icry
@@ -0,0 +1,2 @@
+:l Test.cry
+B::b ()
diff --git a/tests/issues/issue1649/issue1649.icry.stdout b/tests/issues/issue1649/issue1649.icry.stdout
@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module BInterface
+Loading module BFunctor
+Loading module A
+Loading module Test
+()