diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 3e48d6122..2ae2c0cb0 100644 --- 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 index b72466b30..8bf70e80f 100644 --- 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 index aebda4334..24d990642 100644 --- 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 index 121b00ca2..80c1586c1 100644 --- 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