Imported Upstream version 8.5~beta1+dfsg

1 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v
new file mode 100644
index 00000000..febb9c7b
--- /dev/null
+++ b/test-suite/bugs/closed/2362.v
@@ -0,0 +1,38 @@
+Set Implicit Arguments.
+
+Class Pointed (M:Type -> Type) := 
+{
+  creturn: forall {A: Type}, A -> M A
+}.
+
+Unset Implicit Arguments.
+Inductive FPair (A B:Type) (neutral: B) : Type:=
+ fpair : forall (a:A) (b:B), FPair A B neutral.
+Implicit Arguments fpair [[A] [B] [neutral]].
+
+Set Implicit Arguments.
+
+Notation "( x ,> y )" := (fpair x y) (at level 0).
+
+Instance Pointed_FPair B neutral:
+ Pointed (fun A => FPair A B neutral) :=
+ { creturn := fun A (a:A) => (a,> neutral) }.
+Definition blah_fail (x:bool) : FPair bool nat O :=
+  creturn x.
+Set Printing All. Print blah_fail.
+
+Definition blah_explicit (x:bool) : FPair bool nat O :=
+  @creturn _ (Pointed_FPair _ ) _ x.
+
+Print blah_explicit.
+
+
+Instance Pointed_FPair_mono:
+ Pointed (fun A => FPair A nat 0) :=
+ { creturn := fun A (a:A) => (a,> 0) }.
+
+
+Definition blah (x:bool) : FPair bool nat O :=
+  creturn x.
+
+