Substitute terms for evars-as-goals as soon as they are solved in

typeclass resolution. Fixes a bug reported by Eelis van der Weegen.


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

1 files changed, 60 insertions, 0 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
new file mode 100644
index 000000000..55351a472
--- /dev/null
+++ b/test-suite/success/Typeclasses.v
@@ -0,0 +1,60 @@
+Generalizable All Variables.
+
+Module mon.
+
+Reserved Notation "'return' t" (at level 0).
+Reserved Notation "x >>= y" (at level 65, left associativity).
+
+
+
+Record Monad {m : Type -> Type} := {
+  unit : Π {α}, α -> m α where "'return' t" := (unit t) ;
+  bind : Π {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
+  bind_unit_left : Π {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
+
+Print Visibility.
+Print unit.
+Implicit Arguments unit [[m] [m0] [α]].
+Implicit Arguments Monad [].
+Notation "'return' t" := (unit t).
+
+(* Test correct handling of existentials and defined fields. *)
+
+Class A `(e: T) := { a := True }.
+Class B `(e_: T) := { e := e_; sg_ass :> A e }.
+
+Goal forall `{B T}, a.
+  intros. exact I.
+Defined.
+
+Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
+
+Goal forall `{B' T}, a.
+  intros. exact I.
+Defined.
+
+End mon.
+
+(* Correct treatment of dependent goals *) 
+
+(* First some preliminaries: *)
+
+Section sec.
+  Context {N: Type}.
+  Class C (f: N->N) := {}.
+  Class E := { e: N -> N }.
+  Context
+    (g: N -> N) `(E) `(C e)
+    `(forall (f: N -> N), C f -> C (fun x => f x))
+    (U: forall f: N -> N, C f -> False).
+
+(* Now consider the following: *)
+
+  Let foo := U (fun x => e x).
+  Check foo _.
+
+(* This type checks fine, so far so good. But now
+ let's try to get rid of the intermediate constant foo.
+ Surely we can just expand it inline, right? Wrong!: *)
+ Check U (fun x => e x) _.
+End sec.
\ No newline at end of file