Fix bug #3732: firstorder was using detyping to build existential

instances and forgeting about the evars and universes that could appear
there... dirty hack gone, using the evar map properly and avoiding
needless constructions/deconstructions of terms.

3 files changed, 192 insertions, 19 deletions

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a88778c73..5912f0a0c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t=
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid=
-    if Int.equal n 0 then [] else
+  let rec aux n avoid env evmap decls =
+    if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
-	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
-  let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] env evmap nt in
-  let rec raux n t=
-    if Int.equal n 0 then t else
-      match t with
-	  GLambda(loc,name,k,_,t0)->
-	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
-	| _-> anomaly (Pp.str "can't happen") in
-  let ntt=try
-    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
-  with e when Errors.noncritical e ->
-    error "Untypable instance, maybe higher-order non-prenex quantification" in
-    decompose_lam_n_assum m ntt
+      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let decl = (Name nid,None,c) in
+	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+  let evmap, decls = aux m [] env evmap [] in
+    evmap, decls, revt
 
 (* tactics   *)
 
@@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq=
 	    if m>0 then
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
-		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let evmap,rc,ot = mk_open_instance id idc gl m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-		    generalize [gt] gl)
+		  let evmap, _ =
+		    try Typing.e_type_of (pf_env gl) evmap gt
+		    with e when Errors.noncritical e ->
+		      error "Untypable instance, maybe higher-order non-prenex quantification" in
+		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
 		generalize [mkApp(idc,[|t|])])
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
new file mode 100644
index 000000000..80695f382
--- /dev/null
+++ b/test-suite/bugs/closed/3513.v
@@ -0,0 +1,75 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
+Require Coq.Setoids.Setoid.
+Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end; unfold Basics.flip.
+  2: solve [ apply reflexivity ].
+  Undo.
+  2: reflexivity. (* Toplevel input, characters 18-29:
+Error:
+Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
new file mode 100644
index 000000000..6e5952a52
--- /dev/null
+++ b/test-suite/bugs/closed/3732.v
@@ -0,0 +1,104 @@
+(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
+Require Coq.Lists.List.
+
+Import Coq.Lists.List.
+
+Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+
+Section machine.
+  Variables pc state : Type.
+
+  Inductive propX (i := pc) (j := state) : list Type -> Type :=
+  | Inj : forall G, Prop -> propX G
+  | ExistsX : forall G A, propX (A :: G) -> propX G.
+
+  Implicit Arguments Inj [G].
+
+  Definition PropX := propX nil.
+  Fixpoint last (G : list Type) : Type.
+    exact (match G with
+             | nil => unit
+             | T :: nil => T
+             | _ :: G' => last G'
+           end).
+  Defined.
+  Fixpoint eatLast (G : list Type) : list Type.
+    exact (match G with
+             | nil => nil
+             | _ :: nil => nil
+             | x :: G' => x :: eatLast G'
+           end).
+  Defined.
+
+  Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
+    match p with
+      | Inj _ P => fun _ => Inj P
+      | ExistsX G A p1 => fun p' =>
+                            match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
+                              | nil => fun p1 _ => ExistsX p1
+                              | _ :: _ => fun _ rc => ExistsX rc
+                            end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with
+                                                | nil => fun _ _ => Inj True
+                                                | _ => fun p' => p'
+                                              end p'))
+    end.
+
+  Definition spec := state -> PropX.
+  Definition codeSpec := pc -> option spec.
+
+  Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P.
+  Definition interp specs := valid specs nil.
+End machine.
+Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope.
+Bind Scope PropX_scope with PropX propX.
+Variables pc state : Type.
+
+Inductive subs : list Type -> Type :=
+| SNil : subs nil
+| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts).
+
+Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) :=
+  match s in subs G return subs (T :: G) with
+    | SNil => SCons _ nil f SNil
+    | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f)
+  end.
+
+Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state :=
+  match s in subs G return propX pc state G -> PropX pc state with
+    | SNil => fun p => p
+    | SCons _ _ f s' => fun p => Substs s' (subst p f)
+  end.
+Variable specs : codeSpec pc state.
+
+Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)),
+                               interp specs (Substs s (ExX  : A, p))
+                               -> exists a, interp specs (Substs (SPush s a) p).
+admit.
+Defined.
+
+Goal    forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G))
+               (s : subs G)
+               (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p)))
+               (P : forall _ : subs (@cons Type A G), Prop)
+               (_ : forall (s0 : subs (@cons Type A G))
+                           (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)),
+                      P s0),
+          @ex (forall _ : A, PropX pc state)
+              (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)).
+  intros ? ? ? ? H ? H'.
+  apply simplify_fwd_ExistsX in H.
+  firstorder. 
+Qed.
+ (* Toplevel input, characters 15-19:
+Error: Illegal application:
+The term "cons" of type "forall A : Type, A -> list A -> list A"
+cannot be applied to the terms
+ "Type" : "Type"
+ "T" : "Type"
+ "G0" : "list Type"
+The 2nd term has type "Type@{Top.53}" which should be coercible to
+ "Type@{Top.12}".
+ *)
\ No newline at end of file