diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 3deafd0a90..3bb2176ff6 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -72,7 +72,7 @@ import qualified Cryptol.Utils.Ident as C
   ( Ident, PrimIdent(..), mkIdent
   , prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
   , ModName, modNameToText, identText, interactiveName
-  , ModPath(..), modPathSplit, ogModule, Namespace(NSValue)
+  , ModPath(..), modPathSplit, ogModule, ogFromParam, Namespace(NSValue)
   , modNameChunksText
   )
 import qualified Cryptol.Utils.RecordMap as C
@@ -1375,10 +1375,18 @@ importName cnm =
           let (topMod, nested) = C.modPathSplit (C.ogModule og)
               topChunks = C.modNameChunksText topMod
               modNms    = topChunks ++ map C.identText nested
+              -- If the name came from a module parameter, add the module
+              -- parameter identifier to distinguish between names that have the
+              -- same identifier but come from different module parameters (see
+              -- #1892)
+              ifaceNms  = case C.ogFromParam og of
+                            Just i  -> [C.identText i]
+                            Nothing -> []
               shortNm   = C.identText (C.nameIdent cnm)
-              longNm    = Text.intercalate "::" (modNms ++ [shortNm])
+              nmParts   = modNms ++ ifaceNms ++ [shortNm]
+              longNm    = Text.intercalate "::" nmParts
               aliases   = [shortNm, longNm]
-              uri       = cryptolURI (modNms ++ [shortNm]) Nothing
+              uri       = cryptolURI nmParts Nothing
            in pure (ImportedName uri aliases)
 
 -- | Currently this imports declaration groups by inlining all the
diff --git a/intTests/test1892/A.cry b/intTests/test1892/A.cry
new file mode 100644
index 0000000000..4f725bfab5
--- /dev/null
+++ b/intTests/test1892/A.cry
@@ -0,0 +1,3 @@
+interface module A where
+
+a : [8]
diff --git a/intTests/test1892/F.cry b/intTests/test1892/F.cry
new file mode 100644
index 0000000000..1c60d0db61
--- /dev/null
+++ b/intTests/test1892/F.cry
@@ -0,0 +1,6 @@
+module F where
+
+import interface A as X
+import interface A as Y
+
+f = X::a + Y::a
diff --git a/intTests/test1892/I.cry b/intTests/test1892/I.cry
new file mode 100644
index 0000000000..145cfe0538
--- /dev/null
+++ b/intTests/test1892/I.cry
@@ -0,0 +1,3 @@
+module I where
+
+a = 1
diff --git a/intTests/test1892/J.cry b/intTests/test1892/J.cry
new file mode 100644
index 0000000000..05e944b5f4
--- /dev/null
+++ b/intTests/test1892/J.cry
@@ -0,0 +1,3 @@
+module J where
+
+a = 2
diff --git a/intTests/test1892/M.cry b/intTests/test1892/M.cry
new file mode 100644
index 0000000000..4c7c3de7dc
--- /dev/null
+++ b/intTests/test1892/M.cry
@@ -0,0 +1 @@
+module M = F { X = I, Y = J }
diff --git a/intTests/test1892/test.saw b/intTests/test1892/test.saw
new file mode 100644
index 0000000000..28bf4b974d
--- /dev/null
+++ b/intTests/test1892/test.saw
@@ -0,0 +1,2 @@
+import "M.cry";
+prove_print z3 {{ f == X::a + Y::a }};
diff --git a/intTests/test1892/test.sh b/intTests/test1892/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1892/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw