Imported Upstream version 8.5~beta1+dfsg

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_025.v b/test-suite/bugs/closed/HoTT_coq_025.v
new file mode 100644
index 00000000..b81b454d
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_025.v
@@ -0,0 +1,29 @@
+Module monomorphic.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+  (* Error: In environment
+A : Type
+B : Type
+iA : Inhabited A
+iB : Inhabited B
+The term "(A * B)%type" has type "Type" while it is expected to have type
+"Prop". *)
+End monomorphic.
+
+Module polymorphic.
+  Set Universe Polymorphism.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+End polymorphic.