Merge PR #13118: [type classes] Simplify cl_context

Reviewed-by: ppedrot

6 files changed, 74 insertions, 65 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4016a3600e..2853eef5c5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -122,15 +122,24 @@ let next_name_away_from na avoid =
   | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon")
   | Name id -> make_fresh avoid (Global.env ()) id
 
+let rec is_class_arg c =
+  let open Constr in
+  match kind c with
+  | Prod (_,_,c)
+  | Cast (c,_,_)
+  | LetIn (_,_,_,c) -> is_class_arg c
+  | _ ->
+    let c, _ = decompose_appvect c in
+    match destRef c with
+    | exception DestKO -> false
+    | r, _ -> is_class r
+
 let combine_params avoid applied needed =
   let named, applied =
     List.partition
       (function
           (t, Some {CAst.loc;v=ExplByName id}) ->
-            let is_id (_, decl) = match RelDecl.get_name decl with
-            | Name id' -> Id.equal id id'
-            | Anonymous -> false
-            in
+            let is_id decl = Name.equal (Name id) (RelDecl.get_name decl) in
             if not (List.exists is_id needed) then
               user_err ?loc  (str "Wrong argument name: " ++ Id.print id);
             true
@@ -141,27 +150,27 @@ let combine_params avoid applied needed =
     named
   in
   let rec aux ids avoid app need =
-    match app, need with
-
-      | _, (_, LocalDef _) :: need -> aux ids avoid app need
-
-      | [], [] -> List.rev ids, avoid
+    match need with
+    | [] -> begin match app with
+        | [] -> List.rev ids, avoid
+        | (x, _) :: _ -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+      end
 
-      | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
-          aux (Id.List.assoc id named :: ids) avoid app need
+    | LocalDef _ :: need -> aux ids avoid app need
 
-      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
-          aux (x :: ids) avoid app need
 
-      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+    | LocalAssum ({binder_name=Name id}, _) :: need when Id.List.mem_assoc id named ->
+      aux (Id.List.assoc id named :: ids) avoid app need
 
-      | _, (Some _, decl) :: need | [], (None, decl) :: need ->
-        let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-        let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
-        aux (t' :: ids) (Id.Set.add id' avoid) app need
+    | decl :: need ->
+      begin match app, is_class_arg (get_type decl) with
+        | (x, _) :: app, false -> aux (x :: ids) avoid app need
 
-      | (x,_) :: _, [] ->
-          user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+        | [], false | _, true ->
+          let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+          let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
+          aux (t' :: ids) (Id.Set.add id' avoid) app need
+      end
   in
   aux [] avoid applied needed
 
@@ -190,9 +199,7 @@ let implicit_application env ty =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let c = class_info env sigma gr in
-    let (ci, rd) = c.cl_context in
-    let pars = List.rev (List.combine ci rd) in
-    let args, avoid = combine_params avoid par pars in
+    let args, avoid = combine_params avoid par (List.rev c.cl_context) in
     CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fc71254a46..51b228a640 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -56,7 +56,7 @@ type typeclass = {
   cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : GlobRef.t option list * Constr.rel_context;
+  cl_context : Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Constr.rel_context;
@@ -97,7 +97,7 @@ let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
 let typeclass_univ_instance (cl, u) =
   assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
   let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
-    { cl with cl_context = on_snd subst_ctx cl.cl_context;
+    { cl with cl_context = subst_ctx cl.cl_context;
       cl_props = subst_ctx cl.cl_props}
 
 let class_info env sigma c =
@@ -178,7 +178,7 @@ let remove_instance inst =
 
 
 let instance_constructor (cl,u) args =
-  let lenpars = List.count is_local_assum (snd cl.cl_context) in
+  let lenpars = List.count is_local_assum cl.cl_context in
   let open EConstr in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f84d08a7e..b749b978c3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -36,9 +36,9 @@ type typeclass = {
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
 
-  cl_context : GlobRef.t option list * Constr.rel_context;
-  (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-      The global reference gives a direct link to the class itself. *)
+  cl_context : Constr.rel_context;
+  (** Context in which the definitions are typed.
+      Includes both typeclass parameters and superclasses. *)
 
   cl_props : Constr.rel_context;
   (** Context of definitions and properties on defs, will not be shared *)
diff --git a/test-suite/bugs/closed/bug_13117.v b/test-suite/bugs/closed/bug_13117.v
new file mode 100644
index 0000000000..5db3f9fadc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13117.v
@@ -0,0 +1,23 @@
+
+Class A := {}.
+
+Class B (x:A) := {}.
+Class B' (a:=A) (x:a) := {}.
+
+Fail Definition foo a `{B a} := 0.
+Definition foo a `{B' a} := 0.
+
+Record C (x:A) := {}.
+Existing Class C.
+
+Fail Definition bar a `{C a} := 0.
+
+
+Definition X := Type.
+
+Class Y (x:X) := {}.
+
+Definition before `{Y Set} := 0.
+
+Existing Class X.
+Fail Definition after `{Y Set} := 0.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a464eab127..d5509e2697 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -152,9 +152,6 @@ let subst_class (subst,cl) =
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
   let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
-  let do_subst_context (grs,ctx) =
-    List.Smart.map (Option.Smart.map do_subst_gr) grs,
-    do_subst_ctx ctx in
   let do_subst_meth m =
     let c = Option.Smart.map do_subst_con m.meth_const in
     if c == m.meth_const then m
@@ -168,7 +165,7 @@ let subst_class (subst,cl) =
   let do_subst_projs projs = List.Smart.map do_subst_meth projs in
   { cl_univs = cl.cl_univs;
     cl_impl = do_subst_gr cl.cl_impl;
-    cl_context = do_subst_context cl.cl_context;
+    cl_context = do_subst_ctx cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
     cl_projs = do_subst_projs cl.cl_projs;
     cl_strict = cl.cl_strict;
@@ -197,25 +194,16 @@ let discharge_class (_,cl) =
       | VarRef _ | ConstructRef _ -> assert false
       | ConstRef cst -> Lib.section_segment_of_constant cst
       | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
-  let discharge_context ctx' subst (grs, ctx) =
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let grs' =
-      let newgrs = List.map (fun decl ->
-                             match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with
-                             | None -> None
-                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
-                            ctx'
-      in
-      grs @ newgrs
-    in grs', discharge_rel_context subst 1 ctx @ ctx' in
+  let discharge_context ctx' subst ctx =
+    discharge_rel_context subst 1 ctx @ ctx'
+  in
   try
     let info = abs_context cl in
     let ctx = info.Section.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
-    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    let props = discharge_rel_context (subst, usubst) (succ (List.length cl.cl_context)) cl.cl_props in
     let discharge_proj x = x in
     { cl_univs = cl_univs';
       cl_impl = cl.cl_impl;
@@ -324,7 +312,7 @@ let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma t
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-      [] subst (snd k.cl_context)
+      [] subst k.cl_context
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
@@ -399,7 +387,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx =
   let subst =
     List.fold_left2 (fun subst' s decl ->
       if is_local_assum decl then s :: subst' else subst')
-    [] subst (k.cl_props @ snd k.cl_context)
+    [] subst (k.cl_props @ k.cl_context)
   in
   let (app, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr ctx in
@@ -530,7 +518,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   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 cl_context = List.map (Termops.map_rel_decl of_constr) cl.cl_context in
   let _, args =
     List.fold_right (fun decl (args, args') ->
         match decl with
diff --git a/vernac/record.ml b/vernac/record.ml
index a4bf9893d9..acc97f61c1 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -582,26 +582,17 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       in
       List.map map inds
   in
-  let ctx_context =
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    List.map (fun decl ->
-      match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with
-      | Some (_, ((cl,_), _)) -> Some cl.cl_impl
-      | None -> None)
-      params, params
-  in
-  let univs, ctx_context, fields =
+  let univs, params, fields =
     match univs with
     | Polymorphic_entry (nas, univs) ->
       let usubst, auctx = Univ.abstract_universes nas univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
-      let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
-      auctx, ctx_context, fields
+      let params = Context.Rel.map map params in
+      auctx, params, fields
     | Monomorphic_entry _ ->
-      Univ.AUContext.empty, ctx_context, fields
+      Univ.AUContext.empty, params, fields
   in
   let map (impl, projs) =
     let k =
@@ -609,7 +600,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
         cl_impl = impl;
         cl_strict = !typeclasses_strict;
         cl_unique = !typeclasses_unique;
-        cl_context = ctx_context;
+        cl_context = params;
         cl_props = fields;
         cl_projs = projs }
     in
@@ -629,7 +620,7 @@ let add_constant_class env sigma cst =
   let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
-      cl_context = (List.map (const None) ctx, ctx);
+      cl_context = ctx;
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -651,7 +642,7 @@ let add_inductive_class env sigma ind =
     let r = Inductive.relevance_of_inductive env ind in
       { cl_univs = univs;
         cl_impl = GlobRef.IndRef ind;
-        cl_context = List.map (const None) ctx, ctx;
+        cl_context = ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;