Quick hack to fix interpretation of patterns in Ltac.

Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.

We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.

6 files changed, 51 insertions, 25 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 167501de2..20ad9fd4b 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -691,7 +691,9 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (_,c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  pattern_of_constr env sigma c
+  (** FIXME: it is necessary to be unsafe here because of the way we handle
+      evars in the pretyper. Sometimes they get solved eagerly. *)
+  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 
 (* Interprets a constr expression *)
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -736,7 +738,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
       try Inl (coerce_to_evaluable_ref env sigma x)
       with CannotCoerceTo _ ->
         let c = coerce_to_closed_constr env x in
-        Inr (pattern_of_constr env sigma c) in
+        Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
        error_global_not_found ~loc (qualid_of_ident id))
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index edf34607b..23069a9ab 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -214,9 +214,9 @@ let compute_rhs env sigma bodyi index_of_f =
           let i = destRel sigma (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pattern_of_constr env sigma f, Array.map aux args)
+          PApp (pattern_of_constr env sigma (EConstr.to_constr sigma f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr env sigma c
+      | _ -> pattern_of_constr env sigma (EConstr.to_constr sigma c)
   in
   aux bodyi
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 954aa6a94..823071e29 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -122,10 +122,9 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
 let pattern_of_constr env sigma t =
-  let open EConstr in
   let rec pattern_of_constr env t =
   let open Context.Rel.Declaration in
-  match EConstr.kind sigma t with
+  match kind_of_term t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
@@ -141,7 +140,7 @@ let pattern_of_constr env sigma t =
 				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
-          match EConstr.kind sigma f with
+          match kind_of_term f with
           | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
               Evar_kinds.MatchingVar (true,id) -> Some id
@@ -154,18 +153,14 @@ let pattern_of_constr env sigma t =
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
-      pattern_of_constr env (Retyping.expand_projection env sigma p c [])
+      pattern_of_constr env (EConstr.to_constr sigma (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
     | Evar (evk,ctxt as ev) ->
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
-	let ty = existential_type sigma ev in
-	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
-	let ty = existential_type sigma ev in
-	let () = ignore (pattern_of_constr env ty) in
 	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
@@ -179,13 +174,8 @@ let pattern_of_constr env sigma t =
 	in
 	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
 	       Array.to_list (Array.mapi branch_of_constr br))
-    | Fix (idx, (nas, cs, ts)) ->
-      let inj c = EConstr.to_constr sigma c in
-      PFix (idx, (nas, Array.map inj cs, Array.map inj ts))
-    | CoFix (idx, (nas, cs, ts)) ->
-      let inj c = EConstr.to_constr sigma c in
-      PCoFix (idx, (nas, Array.map inj cs, Array.map inj ts))
-  in
+    | Fix f -> PFix f
+    | CoFix f -> PCoFix f in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -228,7 +218,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pattern_of_constr env sigma c
+	  pattern_of_constr env sigma (EConstr.to_constr sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -253,7 +243,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr (Global.env()) Evd.empty (EConstr.of_constr t)
+	 pattern_of_constr (Global.env()) Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 93d2c859a..5694d345c 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,7 @@ val head_of_constr_reference : Evd.evar_map -> constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.constr -> constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5aacafd6f..a1c99c341 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -763,7 +763,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma cty in
+	let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -784,7 +784,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd c' in
+	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -934,7 +934,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
 	      name = name;
               db = None;
               secvars = secvars_of_constr env sigma c;
diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v
new file mode 100644
index 000000000..874abf49f
--- /dev/null
+++ b/test-suite/success/change_pattern.v
@@ -0,0 +1,34 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Axiom vector : Type -> nat -> Type.
+
+Record KleeneStore i j a := kleeneStore
+ { dim : nat
+ ; peek : vector j dim -> a
+ ; pos : vector i dim
+ }.
+
+Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b :=
+  kleeneStore (fun v => f (peek v)) (pos s).
+
+Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg
+  { coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }.
+
+Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x).
+Axiom t : Type -> Type.
+Axiom traverse : KleeneCoalg (fun x => x) t.
+
+Definition size a (x:t a) : nat := dim (traverse a a x).
+
+Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False.
+Proof.
+destruct y.
+pose (X := KSmap (traverse a unit) (traverse unit a x)).
+set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))).
+clearbody e.
+(** The pattern generated by change must have holes where there were implicit
+    arguments in the original user-provided term. This particular example fails
+    if this is not the case because the inferred argument does not coincide with
+    the one in the considered term. *)
+progress (change (dim (traverse unit a x)) with (dim X) in e).