From d0a98a545b35512f8fde4ec8a8c2dcd6ed85f1f0 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Wed, 3 Jul 2024 08:57:52 -0700
Subject: [PATCH] Make fixes for 1691 work with more nested modules.

---
 src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs |  8 +++++++-
 tests/issues/issue_1691_2.cry                       | 12 ++++++++++++
 tests/issues/issue_1691_2.icry                      |  2 ++
 tests/issues/issue_1691_2.icry.stdout               |  4 ++++
 4 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 tests/issues/issue_1691_2.cry
 create mode 100644 tests/issues/issue_1691_2.icry
 create mode 100644 tests/issues/issue_1691_2.icry.stdout

diff --git a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs
index 6d9646cbc..4c8e260f3 100644
--- a/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs
+++ b/src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs
@@ -76,7 +76,13 @@ processModule dcl =
                  Private -> []
              )
 
-        FunctorInstance {} -> ([dcl, mkImp loc [mname]], [])
+        FunctorInstance {} ->
+          let imps = [[mname]]
+          in ( dcl : map (mkImp loc) imps
+             , case tlExport m of
+                 Public  -> imps
+                 Private -> []
+             )
         InterfaceModule {} -> ([dcl], [])
     _ -> panic "processModule" ["Not a module"]
 
diff --git a/tests/issues/issue_1691_2.cry b/tests/issues/issue_1691_2.cry
new file mode 100644
index 000000000..9720f9e7b
--- /dev/null
+++ b/tests/issues/issue_1691_2.cry
@@ -0,0 +1,12 @@
+
+
+submodule F where
+  parameter x: Integer
+  y = x + 1
+
+submodule B = submodule F where x = 2
+
+submodule M where
+  submodule A where
+    a = 2
+  submodule B = submodule F where x = 2
diff --git a/tests/issues/issue_1691_2.icry b/tests/issues/issue_1691_2.icry
new file mode 100644
index 000000000..4b2037138
--- /dev/null
+++ b/tests/issues/issue_1691_2.icry
@@ -0,0 +1,2 @@
+:load issue_1691_2.cry
+:t M::B::y
diff --git a/tests/issues/issue_1691_2.icry.stdout b/tests/issues/issue_1691_2.icry.stdout
new file mode 100644
index 000000000..bb0fddd46
--- /dev/null
+++ b/tests/issues/issue_1691_2.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+M::B::y : Integer