Simplify implicit_quantifiers

After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.

Also remove unused functions.

3 files changed, 19 insertions, 86 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1a81dc41a1..4c8aff3f2e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -392,9 +392,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
     env {loc;v=na} b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
-    if t then ty, ids else
-      Implicit_quantifiers.implicit_application ids
-	Implicit_quantifiers.combine_params_freevar ty
+    if t then ty, ids
+    else Implicit_quantifiers.implicit_application ids ty
   in
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bac46c2d2f..e8d10488b2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -66,9 +66,6 @@ let declare_generalizable ~local gen =
 
 let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
 
-let ids_of_list l =
-  List.fold_right Id.Set.add l Id.Set.empty
-
 let is_global id =
   try ignore (Nametab.locate_extended (qualid_of_ident id)); true
   with Not_found -> false
@@ -105,26 +102,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
-let ids_of_names l =
-  List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l
-
-let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
-  let rec aux bdvars l c = match c with
-      ((CLocalAssum (n, _, c)) :: tl) ->
-	let bound = ids_of_names n in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
-
-    | ((CLocalDef (n, c, t)) :: tl) ->
-        let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in
-	  aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl
-
-    | CLocalPattern _ :: tl -> assert false
-    | [] -> bdvars, l
-  in aux bound l binders
-
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
   let rec vars bound vs c = match DAst.get c with
     | GVar id ->
@@ -149,7 +126,7 @@ 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 combine_params avoid fn applied needed =
+let combine_params avoid applied needed =
   let named, applied =
     List.partition
       (function
@@ -167,47 +144,30 @@ let combine_params avoid fn applied needed =
     (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false)
     named
   in
-  let is_unset (_, decl) = match decl with
-  | LocalAssum _ -> true
-  | LocalDef _ -> false
-  in
-  let needed = List.filter is_unset needed in
   let rec aux ids avoid app need =
     match app, need with
-	[], [] -> List.rev ids, avoid
 
-      | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named ->
+      | _, (_, LocalDef _) :: need -> aux ids avoid app need
+
+      | [], [] -> List.rev ids, avoid
+
+      | 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}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need ->
+      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
 	  aux (x :: ids) avoid app need
 
-      | _, (Some cl, _ as d) :: need ->
-	  let t', avoid' = fn avoid d in
-	    aux (t' :: ids) avoid' app need
-
       | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
 
-      | [], (None, _ as decl) :: need ->
-	  let t', avoid' = fn avoid decl in
-	    aux (t' :: 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
 
       | (x,_) :: _, [] ->
 	  user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
-  in aux [] avoid applied needed
-
-let combine_params_freevar avoid (_, decl) =
-  let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-  (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
-
-let destClassApp cl =
-  let open CAst in
-  let loc = cl.loc in
-  match cl.v with
-    | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst)
-    | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst)
-    | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
-    | _ -> raise Not_found
+  in
+  aux [] avoid applied needed
 
 let destClassAppExpl cl =
   let open CAst in
@@ -217,7 +177,7 @@ let destClassAppExpl cl =
     | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
     | _ -> raise Not_found
 
-let implicit_application env ?(allow_partial=true) f ty =
+let implicit_application env ty =
   let is_class =
     try
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
@@ -230,24 +190,13 @@ let implicit_application env ?(allow_partial=true) f ty =
   match is_class with
   | None -> ty, env
   | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
-    let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+    let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in
     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
-    if not allow_partial then
-      begin
-        let opt_succ x n = match x with
-          | None -> succ n
-          | Some _ -> n
-        in
-        let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-        let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-        if not (Int.equal needlen applen) then
-          mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-      end;
     let pars = List.rev (List.combine ci rd) in
-    let args, avoid = combine_params avoid f par pars in
+    let args, avoid = combine_params avoid par pars in
     CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 437fef1753..d28d35f3a1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -11,22 +11,14 @@
 open Names
 open Glob_term
 open Constrexpr
-open Libnames
 
 val declare_generalizable : local:bool -> lident list option -> unit
 
-val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
-
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
 val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
-val free_vars_of_binders :
-  ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
-
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurrence *)
 
@@ -37,14 +29,7 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
-val combine_params_freevar :
-  Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-  Constrexpr.constr_expr * Id.Set.t
-
-val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-    Constrexpr.constr_expr * Id.Set.t) ->
-  constr_expr -> constr_expr * Id.Set.t
+val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
 
 (* Should be likely located elsewhere *)
 exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)