Distinguish ASTs for Instance and Declare Instance

This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.

10 files changed, 105 insertions, 64 deletions

diff --git a/CHANGES.md b/CHANGES.md
index ae67eb5d1b..46de17106d 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -96,6 +96,8 @@ Vernacular commands
 - Computation of implicit arguments now properly handles local definitions in the
   binders for an `Instance`.
 
+- `Declare Instance` now requires an instance name.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/stm/stm.ml b/stm/stm.ml
index 169d608d2d..1641adbb70 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3006,7 +3006,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               let bname = VCS.mk_branch_name x in
               let opacity_of_produced_term = function
                 (* This AST is ambiguous, hence we check it dynamically *)
-                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
                 | _ -> Doesn'tGuaranteeOpacity in
               VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
               let proof_mode = default_proof_mode () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index bc5c14c9b1..09f531ce13 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -164,7 +164,8 @@ let classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacDeclareCustomEntry _
-    | VernacComments _ -> VtSideff [], VtLater
+    | VernacComments _
+    | VernacDeclareInstance _ -> VtSideff [], VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
 Require Import RelationClasses.
 
 Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
 
 Class bar := { x : False }.
 Record foo := { a : Prop ; b : bar }.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a342f5bf98..7c79c46fe2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -128,7 +128,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
   instance_hook k info global imps ?hook (ConstRef kn)
 
-let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
@@ -144,7 +144,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
          (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
   in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook k pri global imps ?hook (ConstRef cst); id
+  instance_hook k pri global imps (ConstRef cst)
 
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -191,7 +191,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
         (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
 
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
     match props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -278,69 +278,78 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
   else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
   id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode
-    poly ctx (instid, bk, cl) props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
-  let env = Global.env() in
-  let ({CAst.loc;v=instid}, pl) = instid in
+let interp_instance_context env ctx ?(generalize=false) pl bk cl =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass, ids =
     match bk with
     | Decl_kinds.Implicit ->
-	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
-	  (fun avoid (clname, _) ->
-	    match clname with
-            | Some cl ->
-                let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
-		  t, avoid
-	    | None -> failwith ("new instance: under-applied typeclass"))
-	  cl
+      Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
+        (fun avoid (clname, _) ->
+           match clname with
+           | Some cl ->
+             let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
+             t, avoid
+           | None -> failwith ("new instance: under-applied typeclass"))
+        cl
     | Explicit -> cl, Id.Set.empty
   in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
     else tclass
   in
-  let sigma, k, u, cty, ctx', ctx, imps, subst =
-    let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
-    let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
-    let len = Context.Rel.nhyps ctx in
-    let imps = imps @ Impargs.lift_implicits len imps' in
-    let ctx', c = decompose_prod_assum sigma c' in
-    let ctx'' = ctx' @ ctx in
-    let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
-    let u_s = EInstance.kind sigma u in
-    let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
-    let args = List.map of_constr args in
-    let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
-    let _, args =
-      List.fold_right (fun decl (args, args') ->
-	match decl with
-	| LocalAssum _ -> (List.tl args, List.hd args :: args')
+  let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+  let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
+  let len = Context.Rel.nhyps ctx in
+  let imps = imps @ Impargs.lift_implicits len imps' in
+  let ctx', c = decompose_prod_assum sigma c' in
+  let ctx'' = ctx' @ ctx in
+  let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
+  let u_s = EInstance.kind sigma u in
+  let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
+  let args = List.map of_constr args in
+  let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+  let _, args =
+    List.fold_right (fun decl (args, args') ->
+        match decl with
+        | LocalAssum _ -> (List.tl args, List.hd args :: args')
         | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
-        cl_context (args, [])
-    in
-      sigma, cl, u, c', ctx', ctx, imps, args
+      cl_context (args, [])
+  in
+  let sigma = Evarutil.nf_evar_map sigma in
+  let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
+  sigma, cl, u, c', ctx', ctx, imps, args, decl
+
+
+let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+    poly ctx (instid, bk, cl) props
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let ({CAst.loc;v=instid}, pl) = instid in
+  let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    interp_instance_context env ~generalize ctx pl bk cl
   in
   let id =
     match instid with
-	Name id ->
-	  let sp = Lib.make_path id in
-	    if Nametab.exists_cci sp then
-	      user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
-	    id
-      | Anonymous ->
-	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
-	    Namegen.next_global_ident_away i (Termops.vars_of_env env)
+      Name id ->
+      let sp = Lib.make_path id in
+      if Nametab.exists_cci sp then
+        user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
+      id
+    | Anonymous ->
+      let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
+      Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  let sigma = Evarutil.nf_evar_map sigma in
-  let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
-  if abstract then
-    do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
-  else
-    do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
-      cty k u ctx ctx' pri decl imps subst id props
+  do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+    cty k u ctx ctx' pri decl imps subst id props
+
+let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri =
+  let env = Global.env() in
+  let ({CAst.loc;v=instid}, pl) = instid in
+  let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    interp_instance_context env ctx pl bk cl
+  in
+  do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
 
 let named_of_rel_context l =
   let open Vars in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eb6c0c92e1..6f61da66cf 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
   unit
 
 val new_instance :
-  ?abstract:bool (** Not abstract by default. *) ->
   ?global:bool (** Not global by default. *) ->
   ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
@@ -54,6 +53,14 @@ val new_instance :
   Hints.hint_info_expr ->
   Id.t
 
+val declare_new_instance :
+  ?global:bool (** Not global by default. *) ->
+  Decl_kinds.polymorphic ->
+  local_binder_expr list ->
+  ident_decl * Decl_kinds.binding_kind * constr_expr ->
+  Hints.hint_info_expr ->
+  unit
+
 (** Setting opacity *)
 
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 8ffdf74383..3bc4aecdb1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -683,7 +683,7 @@ GRAMMAR EXTEND Gram
 	 info = hint_info ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
 	     ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
-	   { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) }
+	   { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) }
 
       | IDENT "Existing"; IDENT "Instance"; id = global;
           info = hint_info ->
@@ -844,10 +844,10 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l }
 
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
-      | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+      | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
 	 expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
 	 info = hint_info ->
-	   { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+	   { VernacDeclareInstance (bl, (id, expl, t), info) }
 
       (* Should be in syntax, but camlp5 would not factorize *)
       | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3a3da8e2d8..5eeeaada2d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -887,10 +887,9 @@ open Pputils
               spc() ++ pr_class_rawexpr c2)
         )
 
-      | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+      | VernacInstance (sup, (instid, bk, cl), props, info) ->
         return (
           hov 1 (
-            (if abst then keyword "Declare" ++ spc () else mt ()) ++
             keyword "Instance" ++
             (match instid with
              | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
@@ -906,6 +905,16 @@ open Pputils
                 | None -> mt()))
         )
 
+      | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
+        return (
+          hov 1 (
+            keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
+            pr_and_type_binders_arg sup ++
+              str":" ++ spc () ++
+              (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+              pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+        )
+
       | VernacContext l ->
         return (
           hov 1 (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 910fb1a916..26859cd2cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1005,13 +1005,20 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~atts abst sup inst props pri =
+let vernac_instance ~atts sup inst props pri =
   let open DefAttributes in
   let atts = parse atts in
   let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
-  ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
+  ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+
+let vernac_declare_instance ~atts sup inst pri =
+  let open DefAttributes in
+  let atts = parse atts in
+  let global = not (make_section_locality atts.locality) in
+  Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
+  Classes.declare_new_instance ~global atts.polymorphic sup inst pri
 
 let vernac_context ~poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
@@ -2227,8 +2234,10 @@ let interp ?proof ~atts ~st c =
       vernac_identity_coercion ~atts id s t
 
   (* Type classes *)
-  | VernacInstance (abst, sup, inst, props, info) ->
-      vernac_instance ~atts abst sup inst props info
+  | VernacInstance (sup, inst, props, info) ->
+      vernac_instance ~atts sup inst props info
+  | VernacDeclareInstance (sup, inst, info) ->
+      vernac_declare_instance ~atts sup inst info
   | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
   | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
   | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 3eb90f0d30..68a17e316e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -300,12 +300,16 @@ type nonrec vernac_expr =
 
   (* Type classes *)
   | VernacInstance of
-      bool * (* abstract instance *)
       local_binder_expr list * (* super *)
         typeclass_constraint * (* instance name, class name, params *)
         (bool * constr_expr) option * (* props *)
         Hints.hint_info_expr
 
+  | VernacDeclareInstance of
+      local_binder_expr list * (* super *)
+        (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *)
+        Hints.hint_info_expr
+
   | VernacContext of local_binder_expr list
 
   | VernacExistingInstance of