Fixes #1484

src/Cryptol/TypeCheck/Monad.hs

@@ -857,7 +857,7 @@ lookupModule iname =
       do localMods <- getScope mSubmodules
          case Map.lookup m localMods of
            Just names ->
-              do n <- genIfaceWithNames names <$> getCurScope
+              do n <- genIfaceWithNames names <$> getCurDecls
                  pure (If.ifaceForgetName n)
 
            Nothing ->
@@ -1128,12 +1128,38 @@ getScope f =
      rw <- IM get
      pure (sconcat (f (iExtScope ro) :| map f (iScope rw)))
 
-getCurScope :: InferM (ModuleG ScopeName)
-getCurScope =
-  do rw <- IM get
-     case iScope rw of
-       m : _ -> pure m
-       []    -> panic "getCurScope" ["No current scope."]
+getCurDecls :: InferM (ModuleG ())
+getCurDecls =
+  do ro <- IM ask
+     rw <- IM get
+     pure (foldr (\m1 m2 -> mergeDecls (forget m1) m2)
+                (forget (iExtScope ro)) (iScope rw))
+
+  where
+  forget m = m { mName = () }
+
+  mergeDecls m1 m2 =
+    Module
+      { mName             = ()
+      , mDoc              = Nothing
+      , mExports          = mempty
+      , mParams           = mempty
+      , mParamTypes       = mempty
+      , mParamConstraints = mempty
+      , mParamFuns        = mempty
+      , mNested           = mempty
+
+      , mTySyns           = uni mTySyns
+      , mNewtypes         = uni mNewtypes
+      , mPrimTypes        = uni mPrimTypes
+      , mDecls            = uni mDecls
+      , mSubmodules       = uni mSubmodules
+      , mFunctors         = uni mFunctors
+      , mSignatures       = uni mSignatures
+      }
+    where
+    uni f = f m1 <> f m2
+
 
 addDecls :: DeclGroup -> InferM ()
 addDecls ds =

tests/modsys/functors/T037.cry

@@ -0,0 +1,19 @@
+module T037 where
+
+interface submodule I where
+  x : [8]
+
+submodule F where
+  import interface submodule I
+  y = x + 1
+
+submodule P where
+  x = 11
+
+submodule X where
+  submodule M = submodule F { submodule P }
+  import submodule M
+
+  z = y
+
+import submodule X

tests/modsys/functors/T037.icry

@@ -0,0 +1,2 @@
+:load T037.cry
+z

tests/modsys/functors/T037.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T037
+0x0c