diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index d3441abcbb..8db5f6778c 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -19,6 +19,8 @@ def EnvExtensionState : Type := EnvExtensionStateSpec.fst
 instance : Inhabited EnvExtensionState := EnvExtensionStateSpec.snd
 
 def ModuleIdx := Nat
+  deriving BEq, ToString
+
 abbrev ModuleIdx.toNat (midx : ModuleIdx) : Nat := midx
 
 instance : Inhabited ModuleIdx := inferInstanceAs (Inhabited Nat)
diff --git a/tests/pkg/misc/Misc.lean b/tests/pkg/misc/Misc.lean
new file mode 100644
index 0000000000..ec165e72ce
--- /dev/null
+++ b/tests/pkg/misc/Misc.lean
@@ -0,0 +1,11 @@
+import Misc.Foo
+import Lean
+
+open Lean Meta
+
+#eval id (α := MetaM Unit) do
+  assert! (← getEnv).getModuleIdxFor? ``foo == (← getEnv).getModuleIdxFor? `auxDecl1
+  IO.println <| (← getEnv).getModuleIdxFor? ``Lean.Environment
+  IO.println <| (← getEnv).getModuleIdxFor? ``foo
+  IO.println <| (← getEnv).getModuleIdxFor? `auxDecl1
+  IO.println "worked"
diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean
new file mode 100644
index 0000000000..077786d034
--- /dev/null
+++ b/tests/pkg/misc/Misc/Foo.lean
@@ -0,0 +1,9 @@
+import Lean
+
+open Lean Meta
+
+#eval id (α := MetaM Unit) do
+  modifyEnv fun env => env.addExtraName `auxDecl1
+  return ()
+
+def foo := 42
diff --git a/tests/pkg/misc/lakefile.lean b/tests/pkg/misc/lakefile.lean
new file mode 100644
index 0000000000..dfd791ca28
--- /dev/null
+++ b/tests/pkg/misc/lakefile.lean
@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package misc
+@[defaultTarget] lean_lib Misc
diff --git a/tests/pkg/misc/test.sh b/tests/pkg/misc/test.sh
new file mode 100755
index 0000000000..438bb1c522
--- /dev/null
+++ b/tests/pkg/misc/test.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build