1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index dc22b03f2d..957612ef1d 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -308,3 +308,15 @@ Definition RLRL' : forall x : R, RL x = RL (RL x).
 Qed.
 
 End eta.
+
+Module Hurkens'.
+  Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
+Type)) eq_refl.
+
+End Hurkens'.
+\ No newline at end of file