Fix refine and eapply to mark shelved goals as non-resolvable, always

Check that we don't regress on PR #10762 example

Fix regression discovered by Arthur in PR #10762

Fix script of #10298 which was relying on breaking semantics for `eapply`

Add doc

Add comment in clenvtac

Actually, always mark shelved goals as unresolvable

Update doc to reflect semantics w.r.t. shelved subgoals

10 files changed, 97 insertions, 18 deletions

diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
new file mode 100644
index 0000000000..2fef75dc7f
--- /dev/null
+++ b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  The tactics :tacn:`eapply`, :tacn:`refine` and its variants no
+  longer allows shelved goals to be solved by typeclass resolution.
+  (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 81e50c0834..878118c48a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -555,12 +555,14 @@ Applying theorems
    This tactic applies to any goal. It behaves like :tacn:`exact` with a big
    difference: the user can leave some holes (denoted by ``_``
    or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many
-   subgoals as there are holes in the term. The type of holes must be either
-   synthesized by the system or declared by an explicit cast
+   subgoals as there are remaining holes in the elaborated term. The type
+   of holes must be either synthesized by the system or declared by an explicit cast
    like ``(_ : nat -> Prop)``. Any subgoal that
    occurs in other subgoals is automatically shelved, as if calling
-   :tacn:`shelve_unifiable`. This low-level tactic can be
-   useful to advanced users.
+   :tacn:`shelve_unifiable`. The produced subgoals (shelved or not)
+   are *not* candidates for typeclass resolution, even if they have a type-class
+   type as conclusion, letting the user control when and how typeclass resolution
+   is launched on them. This low-level tactic can be useful to advanced users.
 
    .. example::
 
@@ -611,8 +613,9 @@ Applying theorems
    .. tacv:: simple notypeclasses refine @term
       :name: simple notypeclasses refine
 
-      This tactic behaves like :tacn:`simple refine` except it performs type checking
-      without resolution of typeclasses.
+      This tactic behaves like the combination of :tacn:`simple refine` and
+      :tacn:`notypeclasses refine`: it performs type checking without resolution of
+      typeclasses, does not perform beta reductions or shelve the subgoals.
 
    .. flag:: Debug Unification
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ed44372045..6f8e668e4e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1025,8 +1025,11 @@ module Unsafe = struct
 
   let undefined = undefined
 
-  let mark_as_unresolvable p gl =
-    { p with solution = mark_in_evm ~goal:false p.solution [gl] }
+  let mark_unresolvables evm evs =
+    mark_in_evm ~goal:false evm evs
+
+  let mark_as_unresolvables p evs =
+    { p with solution = mark_in_evm ~goal:false p.solution evs }
 
 end
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8ec53ac78c..a92179ab5b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -481,8 +481,13 @@ module Unsafe : sig
       and makes them unresolvable for type classes. *)
   val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
 
-  (** Make an evar unresolvable for type classes. *)
-  val mark_as_unresolvable : proofview -> Evar.t -> proofview
+  (** Make some evars unresolvable for type classes.
+      We need two functions as some functions use the proofview and others
+      directly manipulate the undelying evar_map.
+  *)
+  val mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map
+
+  val mark_as_unresolvables : proofview -> Evar.t list -> proofview
 
   (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
       the current avatar of [g] (for instance [g] was changed by [clear]
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 611671255d..c6a0299cf3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,7 +72,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
         Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
           ~fail:(not with_evars) clenv.env clenv.evd
       in
-      Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
+      (* After an apply, all the subgoals including those dependent shelved ones are in
+         the hands of the user and resolution won't be called implicitely on them. *)
+      Typeclasses.make_unresolvables (fun x -> true) evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2ee006631a..e9f93d0c8f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,12 +386,7 @@ let run_tactic env tac pr =
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
   let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
-  let proofview =
-    List.fold_left
-      Proofview.Unsafe.mark_as_unresolvable
-      proofview
-      to_shelve
-  in
+  let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace),result
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dd8b52e56c..ea42218aaa 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -94,6 +94,7 @@ let generic_refine ~typecheck f gl =
   in
   (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
diff --git a/proofs/refine.mli b/proofs/refine.mli
index bdcccae805..269382489d 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -25,7 +25,8 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand.
+    Shelved evars and goals are all marked as unresolvable for typeclasses. *)
 
 val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic
diff --git a/test-suite/bugs/closed/bug_10298.v b/test-suite/bugs/closed/bug_10298.v
new file mode 100644
index 0000000000..ad4778cc36
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10298.v
@@ -0,0 +1,35 @@
+Set Implicit Arguments.
+
+Generalizable Variables A.
+
+Parameter val : Type.
+
+Class Enc (A:Type) :=
+  make_Enc { enc : A -> val }.
+
+Global Instance Enc_dummy : Enc unit.
+Admitted.
+
+Definition FORM := forall A (EA:Enc A) (Q:A->Prop), Prop.
+
+Axiom FORM_intro : forall F : FORM, F unit Enc_dummy (fun _ : unit => True).
+
+Definition IDF (F:FORM) : FORM := F.
+
+Parameter ID : forall (G:Prop), G -> G.
+
+Parameter EID : forall A (EA:Enc A) (F:FORM) (Q:A->Prop),
+  F _ _ Q ->
+  F _ _ Q.
+
+Lemma bla : forall F,
+  (forall A (EA:Enc A), IDF F EA (fun (X:A) => True) -> True) ->
+  True.
+Proof.
+  intros F M.
+  notypeclasses refine (M _ _ _).
+  notypeclasses refine (EID _ _ _ _).
+  eapply (ID _).
+  Unshelve.
+  + apply FORM_intro.
+Qed.
diff --git a/test-suite/bugs/closed/bug_10762.v b/test-suite/bugs/closed/bug_10762.v
new file mode 100644
index 0000000000..d3991d4d38
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10762.v
@@ -0,0 +1,30 @@
+
+Set Implicit Arguments.
+
+Generalizable Variables A B.
+Parameter val: Type.
+
+Class Enc (A:Type) : Type :=
+  make_Enc { enc : A -> val }.
+
+Hint Mode Enc + : typeclass_instances.
+
+Parameter bar : forall A (EA:Enc A), EA = EA.
+
+Parameter foo : forall (P:Prop),
+   P ->
+   P = P ->
+   True.
+
+Parameter id : forall (P:Prop),
+  P -> P.
+
+  Check enc.
+
+  Lemma test : True.
+  eapply foo; [ eapply bar | apply id]. apply id.
+  (* eapply bar introduces an unresolved typeclass evar that is no longer
+     a candidate after the application (eapply should leave typeclass goals shelved).
+     We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
+      *)
+  Abort.