diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
index a70a793f31..9dc300794e 100644
--- a/base/src/test/java/org/aya/tyck/TyckTest.java
+++ b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -177,6 +177,12 @@ public void testVariableDefinition() {
       prim I prim Path
       variable A : Type
       variable a : A
+      open inductive K | kk
+      open inductive G (k : K) | gg
+      open inductive F (A : Type) (k : K) (n : G k) | ff
+      variable k : K
+      variable n : G k
+      variable xs : F A k n
       def infix = (a b : A) => Path (\\i => A) a b
     """).defs;
     assertTrue(result.isNotEmpty());