Make imported signatures work

src/Cryptol/ModuleSystem/Renamer.hs

@@ -555,7 +555,7 @@ doModParam mp =
          loc     = srcRange sigName
      withLoc loc
        do nm <- resolveName NameUse NSSignature (thing sigName)
-          sigEnv <- lookupDefines (ImpNested nm)
+          sigEnv <- lookupSigDefines nm
           me <- getCurMod
           let newP x = do y <- lift (newModParam me (mpName mp) loc x)
                           sets_ (Map.insert y x)

src/Cryptol/ModuleSystem/Renamer/Monad.hs

@@ -448,7 +448,25 @@ lookupDefines nm =
   do ro <- RenameM ask
      case Map.lookup nm (roResolvedModules ro) of
        Just loc -> pure (rmodDefines loc)
-       Nothing  -> maybe mempty modDefines . ($ nm) <$> getLoadedModsMaybe
+       Nothing  ->
+         do loaded <- getLoadedMods
+            pure (modDefines (loaded nm))
+
+lookupSigDefines :: Name -> RenameM NamingEnv
+lookupSigDefines nm =
+  do ro <- RenameM ask
+     case Map.lookup (ImpNested nm) (roResolvedModules ro) of
+       Just loc -> pure (rmodDefines loc)
+       Nothing ->
+         do getIf <- RenameM (roIfaces <$> ask)
+            let top = nameTopModule nm
+                sigs = ifSignatures (ifPublic (getIf top))
+            case Map.lookup nm sigs of
+              Just s -> pure (modParamsNamingEnv s)
+              Nothing ->
+                panic "lookupSigDefines" [ "Missing signature "<> show nm]
+
+
 
 
 checkIsModule :: Range -> ImpName Name -> RenameM ()

tests/modsys/functors/T009.cry

@@ -0,0 +1,11 @@
+
+/* Test that importing signatures from another module works */
+
+import T009_S
+
+submodule F where
+  import signature A
+  y : [n]
+  y = 1
+
+

tests/modsys/functors/T009.icry

@@ -0,0 +1 @@
+:load T009.cry

tests/modsys/functors/T009.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T009_S
+Loading module Main

tests/modsys/functors/T009_S.cry

@@ -0,0 +1,8 @@
+module T009_S where
+
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+z = 0x22