From c8c1723747c7e0eb748861cc12aecca411848f4c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Sep 2020 12:25:02 +0200
Subject: First list in cl_context is just booleans

Used only by implicit_quantifiers
---
 interp/implicit_quantifiers.ml |  6 +++---
 pretyping/typeclasses.ml       |  2 +-
 pretyping/typeclasses.mli      |  4 ++--
 vernac/classes.ml              | 13 +++++--------
 vernac/record.ml               |  8 ++++----
 5 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4016a3600e..c5324702dc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -150,12 +150,12 @@ let combine_params avoid applied needed =
       | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
           aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
+      | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need ->
           aux (x :: ids) avoid app need
 
-      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+      | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need
 
-      | _, (Some _, decl) :: need | [], (None, decl) :: need ->
+      | _, (true, decl) :: need | [], (false, 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
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fc71254a46..7479a63762 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 : bool list * Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Constr.rel_context;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f84d08a7e..ea67ca273e 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;
+  cl_context : bool 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. *)
+      The bool says whether we are at a class. *)
 
   cl_props : Constr.rel_context;
   (** Context of definitions and properties on defs, will not be shared *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a464eab127..31d04c1b0d 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 = on_snd 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;
@@ -202,10 +199,10 @@ let discharge_class (_,cl) =
     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'
+          match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with
+          | None -> false
+          | Some _ -> true)
+          ctx'
       in
       grs @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
diff --git a/vernac/record.ml b/vernac/record.ml
index 89acd79dda..54fd1b2c51 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -592,8 +592,8 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
     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)
+      | Some _ -> true
+      | None -> false)
       params, params
   in
   let univs, ctx_context, fields =
@@ -634,7 +634,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 = (List.map (const false) ctx, ctx);
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -656,7 +656,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 = List.map (const false) ctx, ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;
-- 
cgit v1.2.3


From 661d84228fa1a6750b4a80f41c3e012e6de763bf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Sep 2020 12:32:31 +0200
Subject: Simplify Implicit_quantifiers.combine_params a bit

---
 interp/implicit_quantifiers.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c5324702dc..0ed0b8a1a5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -127,10 +127,7 @@ let combine_params avoid applied needed =
     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
@@ -147,15 +144,13 @@ let combine_params avoid applied needed =
 
       | [], [] -> List.rev ids, avoid
 
-      | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
+      | _, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
           aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need ->
-          aux (x :: ids) avoid app need
+      | (x, _) :: app, (false, _) :: need -> aux (x :: ids) avoid app need
 
-      | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need
-
-      | _, (true, decl) :: need | [], (false, decl) :: need ->
+      | _, (true, decl) :: need
+      | [], (false, 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
-- 
cgit v1.2.3


From 07b7bd7f8358d199b0464a673aec50dedae0a45d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Sep 2020 12:50:37 +0200
Subject: Implicit_quantifiers don't use precomputed is_class data

Fix #13117

We alternatively could fix the generation of the data with Existing
Class but I prefer moving towards removing it.
---
 interp/implicit_quantifiers.ml     | 47 ++++++++++++++++++++++++--------------
 test-suite/bugs/closed/bug_13117.v | 23 +++++++++++++++++++
 2 files changed, 53 insertions(+), 17 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13117.v

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0ed0b8a1a5..0f05cc5e10 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -122,12 +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) = Name.equal (Name id) (RelDecl.get_name decl) 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
@@ -138,25 +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
+    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
 
-      | [], [] -> List.rev ids, avoid
+    | LocalDef _ :: need -> aux 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
 
-      | (x, _) :: app, (false, _) :: need -> aux (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
 
-      | _, (true, decl) :: need
-      | [], (false, 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
 
@@ -186,8 +200,7 @@ let implicit_application env ty =
     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 rd) in
     CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
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.
-- 
cgit v1.2.3


From e23be6ebc7d9c9842f8c1036e145fb15c3154e17 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Sep 2020 12:54:59 +0200
Subject: Remove unused is_class info from cl_context

---
 interp/implicit_quantifiers.ml |  3 +--
 pretyping/typeclasses.ml       |  6 +++---
 pretyping/typeclasses.mli      |  6 +++---
 vernac/classes.ml              | 25 ++++++++-----------------
 vernac/record.ml               | 23 +++++++----------------
 5 files changed, 22 insertions(+), 41 deletions(-)

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0f05cc5e10..2853eef5c5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -199,8 +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 args, avoid = combine_params avoid par (List.rev rd) 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 7479a63762..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 : bool 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 ea67ca273e..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 : bool list * Constr.rel_context;
-  (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-      The bool says whether we are at a class. *)
+  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/vernac/classes.ml b/vernac/classes.ml
index 31d04c1b0d..d5509e2697 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -165,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 = on_snd do_subst_ctx 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;
@@ -194,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 -> false
-          | Some _ -> true)
-          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;
@@ -321,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
@@ -396,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
@@ -527,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 54fd1b2c51..968d8aed30 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -587,26 +587,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 _ -> true
-      | None -> false)
-      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 =
@@ -614,7 +605,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
@@ -634,7 +625,7 @@ let add_constant_class env sigma cst =
   let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
-      cl_context = (List.map (const false) ctx, ctx);
+      cl_context = ctx;
       cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
@@ -656,7 +647,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 false) ctx, ctx;
+        cl_context = ctx;
         cl_props = [LocalAssum (make_annot Anonymous r, ty)];
         cl_projs = [];
         cl_strict = !typeclasses_strict;
-- 
cgit v1.2.3