Handle some more cases where fake names caused problems.

See #1440
GaloisInc · Sep 29, 2022 · 39c6026 · 39c6026
1 parent 12967c4
commit 39c6026
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 5 deletions.
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -52,7 +52,8 @@ import Cryptol.Parser.AST
 import Cryptol.Parser.Selector(selName)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.RecordMap
-import Cryptol.Utils.Ident(allNamespaces,OrigName(..),modPathCommon,preludeName)
+import Cryptol.Utils.Ident(allNamespaces,OrigName(..),modPathCommon,
+                              undefinedModName)
 import Cryptol.Utils.PP
 
 import Cryptol.ModuleSystem.Interface
@@ -275,12 +276,16 @@ checkFunctorArgs args =
 
   checkArg l =
       case thing l of
-        ModuleArg m -> checkIsModule (srcRange l) m AModule
+        ModuleArg m
+          | isFakeName m -> pure ()
+          | otherwise    -> checkIsModule (srcRange l) m AModule
         ParameterArg {} -> pure () -- we check these in the type checker
 
 mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name ->
   RenameM (Map Name Name)
-mkInstMap checkFun acc0 ogname iname =
+mkInstMap checkFun acc0 ogname iname
+  | isFakeName ogname = pure Map.empty
+  | otherwise =
   do case checkFun of
        Nothing -> pure ()
        Just r  -> checkIsModule r ogname AFunctor
@@ -857,6 +862,14 @@ reportUnboundName expected qn =
 
      mkFakeName expected qn
 
+isFakeName :: ImpName Name -> Bool
+isFakeName m =
+  case m of
+    ImpTop x -> x == undefinedModName
+    ImpNested x ->
+      case nameTopModuleMaybe x of
+        Just y  -> y == undefinedModName
+        Nothing -> False
 
 
 -- | Resolve a name, and report error on failure
@@ -881,8 +894,8 @@ renameType nt = resolveName nt NSType
 mkFakeName :: Namespace -> PName -> RenameM Name
 mkFakeName ns pn =
   do ro <- RenameM ask
-     liftSupply (mkDeclared ns (TopModule preludeName) SystemName (getIdent pn)
-                                                       Nothing (roLoc ro))
+     liftSupply (mkDeclared ns (TopModule undefinedModName)
+                               SystemName (getIdent pn) Nothing (roLoc ro))
 
 -- | Rename a schema, assuming that none of its type variables are already in
 -- scope.

diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs
@@ -26,6 +26,7 @@ module Cryptol.Utils.Ident
   , packModName
   , preludeName
   , preludeReferenceName
+  , undefinedModName
   , floatName
   , suiteBName
   , arrayName
@@ -204,6 +205,9 @@ modSep  = "::"
 preludeName :: ModName
 preludeName  = packModName ["Cryptol"]
 
+undefinedModName :: ModName
+undefinedModName = packModName ["Undefined module"]
+
 preludeReferenceName :: ModName
 preludeReferenceName = packModName ["Cryptol","Reference"]
 

diff --git a/tests/issues/T1440.cry b/tests/issues/T1440.cry
@@ -1 +1,14 @@
 import interface submodule X
+
+interface submodule I where
+  type n : #
+
+submodule M where
+  import interface submodule I
+
+submodule N where
+  x = 2
+
+submodule M1 = submodule M { submodule U1 }
+submodule M2 = submodule U2 { submodule N }
+
diff --git a/tests/issues/T1440.icry.stdout b/tests/issues/T1440.icry.stdout
@@ -4,3 +4,7 @@ Loading module Main
 
 [error] at T1440.cry:1:28--1:29
     Module not in scope: X
+[error] at T1440.cry:12:40--12:42
+    Module not in scope: U1
+[error] at T1440.cry:13:26--13:28
+    Module not in scope: U2