Adding test-case for bug #2362, which uses HO unification during

typeclass resolution.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13533 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
new file mode 100644
index 0000000000..897f7c456f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2362.v
@@ -0,0 +1,39 @@
+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.
+
+