diff --git a/tests/lean/run/2602.lean b/tests/lean/run/2602.lean
new file mode 100644
index 0000000000..c1d11599ab
--- /dev/null
+++ b/tests/lean/run/2602.lean
@@ -0,0 +1,13 @@
+inductive Units : Bool → Type where
+| seconds : Units false
+| hours : Units true
+
+open Units
+
+structure Quantity (d : Bool) : Type where
+  quantity : Unit
+  units : Units d
+
+instance (d : Bool) : ToString (Quantity d) where
+  toString q := match q.units with | seconds => "seconds" | hours => "hours"
+