diff --git a/tests/lean/run/deBruijn.lean b/tests/lean/run/deBruijn.lean
index 5a82bd7b0b..85e9a39594 100644
--- a/tests/lean/run/deBruijn.lean
+++ b/tests/lean/run/deBruijn.lean
@@ -1,4 +1,4 @@
-inductive HList {α : Type u} (β : α → Type u) : List α → Type u
+inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
   | nil  : HList β []
   | cons : β i → HList β is → HList β (i::is)