diff --git a/tests/lean/run/issue11655.lean b/tests/lean/run/issue11655.lean
new file mode 100644
index 0000000000..a4bf37f0ae
--- /dev/null
+++ b/tests/lean/run/issue11655.lean
@@ -0,0 +1,7 @@
+inductive T : Bool → Type
+| mkTrue  : T true
+| mkFalse : T false
+
+def test2 : (b : Bool) → T b → (bif b then Nat else List Nat) → Nat
+  | .(true), T.mkTrue, Nat.zero  => 1
+  | _, _, _ => 0