Propagate nested relation when instantiating functors (#1720)

src/Cryptol/TypeCheck/Module.hs

@@ -106,6 +106,7 @@ doFunctorInst m f as instMap0 enclosingInScope doc =
      mapM_ addNominal   (Map.elems (mNominalTypes m2))
      addSignatures      (mSignatures m2)
      addSubmodules      (mSubmodules m2)
+     setNested          (mNested m2)
      addFunctors        (mFunctors m2)
      mapM_ addDecls     (mDecls m2)
 

src/Cryptol/TypeCheck/Monad.hs

@@ -1194,7 +1194,9 @@ addFunctors :: Map Name (ModuleG Name) -> InferM ()
 addFunctors mp =
   updScope \r -> r { mFunctors = Map.union mp (mFunctors r) }
 
-
+setNested :: Set Name -> InferM ()
+setNested names =
+  updScope \r -> r { mNested = names }
 
 
 -- | The sub-computation is performed with the given abstract function in scope.

tests/docstrings/T06.cry

@@ -0,0 +1,23 @@
+module T06 where
+
+interface submodule I where
+  type N : #
+
+submodule N1 where
+  type N = 1
+
+submodule C where
+  import interface submodule I
+
+  /**
+   * ```repl
+   * let x = lost
+   * ```
+   */
+  lost = ()
+
+submodule B where
+  import interface submodule I
+  submodule C_ = submodule C { submodule N1 }
+
+submodule A = submodule B { submodule N1 }

tests/docstrings/T06.icry

@@ -0,0 +1,2 @@
+:m T06
+:check-docstrings

tests/docstrings/T06.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T06
+
+let x = lost
+
+Successes: 1, Failures: 0