diff --git a/tests/pkg/def_clash/.gitignore b/tests/pkg/def_clash/.gitignore
new file mode 100644
index 0000000000..10ed5ae23f
--- /dev/null
+++ b/tests/pkg/def_clash/.gitignore
@@ -0,0 +1 @@
+produced.out
diff --git a/tests/pkg/def_clash/TestFoo.lean b/tests/pkg/def_clash/TestFoo.lean
new file mode 100644
index 0000000000..730a5c09c4
--- /dev/null
+++ b/tests/pkg/def_clash/TestFoo.lean
@@ -0,0 +1,3 @@
+module
+import FooA
+import FooB
diff --git a/tests/pkg/def_clash/TestUse.lean b/tests/pkg/def_clash/TestUse.lean
new file mode 100644
index 0000000000..c03da91bd2
--- /dev/null
+++ b/tests/pkg/def_clash/TestUse.lean
@@ -0,0 +1,7 @@
+module
+import UseA
+import UseB
+
+def main : IO Unit := do
+  IO.println useA
+  IO.println useB
diff --git a/tests/pkg/def_clash/clean.sh b/tests/pkg/def_clash/clean.sh
new file mode 100755
index 0000000000..d0fc520759
--- /dev/null
+++ b/tests/pkg/def_clash/clean.sh
@@ -0,0 +1,2 @@
+rm -rf lake-manifest.json .lake/build produced.out
+rm -rf deps/fooA/.lake/build deps/fooB/.lake/build deps/useA/.lake/build deps/useB/.lake/build
diff --git a/tests/pkg/def_clash/deps/fooA/FooA.lean b/tests/pkg/def_clash/deps/fooA/FooA.lean
new file mode 100644
index 0000000000..ef3c1966dc
--- /dev/null
+++ b/tests/pkg/def_clash/deps/fooA/FooA.lean
@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooA"
diff --git a/tests/pkg/def_clash/deps/fooA/lakefile.toml b/tests/pkg/def_clash/deps/fooA/lakefile.toml
new file mode 100644
index 0000000000..337fe19f76
--- /dev/null
+++ b/tests/pkg/def_clash/deps/fooA/lakefile.toml
@@ -0,0 +1,5 @@
+name = "fooA"
+
+[[lean_lib]]
+name = "FooA"
+leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/fooB/FooB.lean b/tests/pkg/def_clash/deps/fooB/FooB.lean
new file mode 100644
index 0000000000..5eeb1fc4d0
--- /dev/null
+++ b/tests/pkg/def_clash/deps/fooB/FooB.lean
@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooB"
diff --git a/tests/pkg/def_clash/deps/fooB/lakefile.toml b/tests/pkg/def_clash/deps/fooB/lakefile.toml
new file mode 100644
index 0000000000..6e6d2d1fe9
--- /dev/null
+++ b/tests/pkg/def_clash/deps/fooB/lakefile.toml
@@ -0,0 +1,5 @@
+name = "fooB"
+
+[[lean_lib]]
+name = "FooB"
+leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/useA/UseA.lean b/tests/pkg/def_clash/deps/useA/UseA.lean
new file mode 100644
index 0000000000..07106dcc63
--- /dev/null
+++ b/tests/pkg/def_clash/deps/useA/UseA.lean
@@ -0,0 +1,4 @@
+module
+import FooA
+
+public def useA : String := foo
diff --git a/tests/pkg/def_clash/deps/useA/lakefile.toml b/tests/pkg/def_clash/deps/useA/lakefile.toml
new file mode 100644
index 0000000000..95a4a95f2a
--- /dev/null
+++ b/tests/pkg/def_clash/deps/useA/lakefile.toml
@@ -0,0 +1,9 @@
+name = "useA"
+
+[[lean_lib]]
+name = "UseA"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "fooA"
+path = "../fooA"
diff --git a/tests/pkg/def_clash/deps/useB/UseB.lean b/tests/pkg/def_clash/deps/useB/UseB.lean
new file mode 100644
index 0000000000..02cd1cbb9e
--- /dev/null
+++ b/tests/pkg/def_clash/deps/useB/UseB.lean
@@ -0,0 +1,4 @@
+module
+import FooB
+
+public def useB : String := foo
diff --git a/tests/pkg/def_clash/deps/useB/lakefile.toml b/tests/pkg/def_clash/deps/useB/lakefile.toml
new file mode 100644
index 0000000000..7a978c7ccd
--- /dev/null
+++ b/tests/pkg/def_clash/deps/useB/lakefile.toml
@@ -0,0 +1,9 @@
+name = "useB"
+
+[[lean_lib]]
+name = "UseB"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "fooB"
+path = "../fooB"
diff --git a/tests/pkg/def_clash/lakefile.toml b/tests/pkg/def_clash/lakefile.toml
new file mode 100644
index 0000000000..5bc1109c07
--- /dev/null
+++ b/tests/pkg/def_clash/lakefile.toml
@@ -0,0 +1,17 @@
+name = "test"
+
+[[lean_lib]]
+name = "TestFoo"
+leanOptions.experimental.module = true
+
+[[lean_exe]]
+name = "TestUse"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "useA"
+path = "deps/useA"
+
+[[require]]
+name = "useB"
+path = "deps/useB"
diff --git a/tests/pkg/def_clash/test.sh b/tests/pkg/def_clash/test.sh
new file mode 100755
index 0000000000..afb51b29ed
--- /dev/null
+++ b/tests/pkg/def_clash/test.sh
@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+
+# Tests the behavior of transitively importing multiple modules
+# that define the same symbol.
+
+# Currently, if two packages define the same Lean symbol (e.g., `foo`)
+# they cannot be in the same transitive import graph, even if the no module
+# can see both instances of the symbol.
+
+# In the example in this directory, `fooA` and `fooB` both define `foo`.
+# `useA` privately imports and uses `fooA`, and `useB` private imports and uses
+# `fooB`. When `TestUse` imports `useA` and `useB`, the linker will complain
+# even though the Lean file does not see both `foo` definitions.
+
+# See also https://github.com/leanprover/lean4/issues/222
+
+source ../../lake/tests/common.sh
+
+./clean.sh
+
+# Test the behavior when multiple copies of the same definition (`foo`)
+# are seen by Lean (e.g., via importing two modules which define them).
+test_err "environment already contains 'foo'" build TestFoo
+
+# Test the behavior when multiple copies of the same definition (`foo`) exist
+# but are not visible to any one module: a symbol clash between the two `foo`s.
+test_err "l_foo" build TestUse