Merge PR #10996: Refine Instance returns

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot

8 files changed, 124 insertions, 63 deletions

diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
new file mode 100644
index 0000000000..cd1a692f54
--- /dev/null
+++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
@@ -0,0 +1,4 @@
+- Added ``#[refine]`` attribute for :cmd:`Instance`, a more
+  predictable version of the old ``Refine Instance Mode`` which
+  unconditionally opens a proof (`#10996
+  <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 1bbf988505..57a2254100 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is:
          | tt, tt => eq_refl tt
          end }.
 
-Using :cmd:`Program Instance`, if one does not give all the members in
-the Instance declaration, Coq generates obligations for the remaining
-fields, e.g.:
+Using the attribute ``refine``, if the term is not sufficient to
+finish the definition (e.g. due to a missing field or non-inferable
+hole) it must be finished in proof mode. If it is sufficient a trivial
+proof mode with no open goals is started.
+
+.. coqtop:: in
+
+   #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }.
+   Proof. intros [] [];reflexivity. Defined.
+
+Note that if you finish the proof with :cmd:`Qed` the entire instance
+will be opaque, including the fields given in the initial term.
+
+Alternatively, in :flag:`Program Mode` if one does not give all the
+members in the Instance declaration, Coq generates obligations for the
+remaining fields, e.g.:
 
 .. coqtop:: in
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1493092f2f..6be358be21 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2023,7 +2023,8 @@ let add_morphism atts binders m s n =
   let _id, lemma = Classes.new_instance_interactive
       ~global:atts.global ~poly:atts.polymorphic
       instance_name binders instance_t
-      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
+      ~generalize:false ~tac ~hook:(declare_projection n instance_id)
+      Hints.empty_hint_info None
   in
   lemma (* no instance body -> always open proof *)
 
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 24976d8c1f..ff0bf0ac2a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -183,12 +183,16 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
     | VernacProofMode pm -> VtProofMode pm
-    | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee, idents_of_name name.CAst.v)
-    | VernacInstance ((name,_),_,_,_,_) ->
-      VtSideff (idents_of_name name.CAst.v, VtLater)
+    | VernacInstance ((name,_),_,_,props,_) ->
+      let program, refine =
+        Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
+      in
+      if program || (props <> None && not refine) then
+        VtSideff (idents_of_name name.CAst.v, VtLater)
+      else
+        let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+        let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (guarantee, idents_of_name name.CAst.v)
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v
new file mode 100644
index 0000000000..f4d2f07db5
--- /dev/null
+++ b/test-suite/success/RefineInstance.v
@@ -0,0 +1,23 @@
+
+
+Class Foo := foo { a : nat; b : bool }.
+
+Fail Instance bla : Foo := { b:= true }.
+
+#[refine] Instance bla : Foo := { b:= true }.
+Proof.
+exact 0.
+Defined.
+
+Instance bli : Foo := { a:=1; b := false}.
+Check bli.
+
+Fail #[program, refine] Instance bla : Foo := {b := true}.
+
+#[program] Instance blo : Foo := {b := true}.
+Next Obligation. exact 2. Qed.
+Check blo.
+
+#[refine] Instance xbar : Foo := {a:=4; b:=true}.
+Proof. Qed.
+Check xbar.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index e9a0ed7c34..0333b73ffe 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -401,7 +401,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx =
   let term = it_mkLambda_or_LetIn (Option.get app) ctx in
   term, termtype
 
-let do_instance_resolve_TC term termtype sigma env =
+let do_instance_resolve_TC termtype sigma env =
   let sigma = Evarutil.nf_evar_map sigma in
   let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
   (* Try resolving fields that are typeclasses automatically. *)
@@ -447,15 +447,37 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
         (push_rel_context ctx' env') sigma kcl_props props subst in
     res, sigma
 
-let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id =
-  let term, termtype =
-    if List.is_empty k.cl_props then
+let interp_props ~program_mode env' cty k u ctx ctx' subst sigma = function
+  | (true, { CAst.v = CRecord fs; loc }) ->
+    check_duplicate ?loc fs;
+    let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
+    let term, termtype =
+      do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+    term, termtype, sigma
+  | (_, term) ->
+    let sigma, def =
+      interp_casted_constr_evars ~program_mode env' sigma term cty in
+    let termtype = it_mkProd_or_LetIn cty ctx in
+    let term = it_mkLambda_or_LetIn def ctx in
+    term, termtype, sigma
+
+let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
+  let term, termtype, sigma = match opt_props with
+    | Some props ->
+      on_pi1 (fun x -> Some x)
+        (interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props)
+    | None ->
       let term, termtype =
-        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
-      Some term, termtype
-    else
-      None, it_mkProd_or_LetIn cty ctx in
-  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+        if List.is_empty k.cl_props then
+          let term, termtype =
+            do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+          Some term, termtype
+        else
+          None, it_mkProd_or_LetIn cty ctx
+      in
+      let termtype, sigma = do_instance_resolve_TC termtype sigma env in
+      term, termtype, sigma
+  in
   Flags.silently (fun () ->
       declare_instance_open sigma ?hook ~tac ~global ~poly
         id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
@@ -463,20 +485,9 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx'
 
 let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
   let term, termtype, sigma =
-    match props with
-    | (true, { CAst.v = CRecord fs; loc }) ->
-      check_duplicate ?loc fs;
-      let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in
-      let term, termtype =
-        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
-      term, termtype, sigma
-    | (_, term) ->
-      let sigma, def =
-        interp_casted_constr_evars ~program_mode:false env' sigma term cty in
-      let termtype = it_mkProd_or_LetIn cty ctx in
-      let term = it_mkLambda_or_LetIn def ctx in
-      term, termtype, sigma in
-  let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in
+    interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props
+  in
+  let termtype, sigma = do_instance_resolve_TC termtype sigma env in
   if Evd.has_undefined sigma then
     CErrors.user_err Pp.(str "Unsolved obligations remaining.")
   else
@@ -485,26 +496,15 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
 let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
     match opt_props with
-    | Some (true, { CAst.v = CRecord fs; loc }) ->
-      check_duplicate ?loc fs;
-      let subst, sigma =
-        do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
-      let term, termtype =
-        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
-      term, termtype, sigma
-    | Some (_, term) ->
-      let sigma, def =
-        interp_casted_constr_evars ~program_mode:true env' sigma term cty in
-      let termtype = it_mkProd_or_LetIn cty ctx in
-      let term = it_mkLambda_or_LetIn def ctx in
-      term, termtype, sigma
+    | Some props ->
+      interp_props ~program_mode:true env' cty k u ctx ctx' subst sigma props
     | None ->
       let subst, sigma =
         do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in
       let term, termtype =
         do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
       term, termtype, sigma in
-  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+  let termtype, sigma = do_instance_resolve_TC termtype sigma env in
   if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
     declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
   else
@@ -555,12 +555,13 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
 
 let new_instance_interactive ?(global=false)
     ~poly instid ctx cl
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook
+    pri opt_props =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     new_instance_common ~program_mode:false ~generalize env instid ctx cl in
-  id, do_instance_interactive env sigma ?hook ~tac ~global ~poly
-    cty k u ctx ctx' pri decl imps subst id
+  id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
+    cty k u ctx ctx' pri decl imps subst id opt_props
 
 let new_instance_program ?(global=false)
     ~poly instid ctx cl opt_props
@@ -589,3 +590,10 @@ let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri =
     interp_instance_context ~program_mode ~generalize:false env ctx pl cl
   in
   do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
+
+let refine_att =
+  let open Attributes in
+  let open Notations in
+  attribute_of_list ["refine",single_key_parser ~name:"refine" ~key:"refine" ()] >>= function
+  | None -> return false
+  | Some () -> return true
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 1247fdc8c1..594df52c70 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -35,6 +35,7 @@ val new_instance_interactive
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
+  -> (bool * constr_expr) option
   -> Id.t * Lemmas.t
 
 val new_instance
@@ -84,3 +85,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 (** For generation on names based on classes only *)
 
 val id_of_class : typeclass -> Id.t
+
+val refine_att : bool Attributes.attribute
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6dfba02ae9..128c30908b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1048,27 +1048,27 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 let vernac_instance_program ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), poly =
-    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  let locality, poly =
+    Attributes.(parse (Notations.(locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in
   ()
 
-let vernac_instance_interactive ~atts name bl t info =
+let vernac_instance_interactive ~atts name bl t info props =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), poly =
-    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  let locality, poly =
+    Attributes.(parse (Notations.(locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id, pstate =
-    Classes.new_instance_interactive ~global ~poly name bl t info in
+    Classes.new_instance_interactive ~global ~poly name bl t info props in
   pstate
 
 let vernac_instance ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), poly =
-    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  let locality, poly =
+    Attributes.(parse (Notations.(locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id : Id.t =
@@ -2094,16 +2094,21 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    let { DefAttributes.program } = DefAttributes.parse atts in
+    let atts, program = Attributes.(parse_with_extra program) atts in
     if program then
       VtDefault (fun () -> vernac_instance_program ~atts name bl t props info)
     else begin match props with
     | None ->
-       VtOpenProof(fun () ->
-        vernac_instance_interactive ~atts name bl t info)
+       VtOpenProof (fun () ->
+        vernac_instance_interactive ~atts name bl t info None)
     | Some props ->
-       VtDefault(fun () ->
-        vernac_instance ~atts name bl t props info)
+      let atts, refine = Attributes.parse_with_extra Classes.refine_att atts in
+      if refine then
+        VtOpenProof (fun () ->
+          vernac_instance_interactive ~atts name bl t info (Some props))
+      else
+        VtDefault (fun () ->
+          vernac_instance ~atts name bl t props info)
     end
 
   | VernacDeclareInstance (id, bl, inst, info) ->