Remove special case for implicit inductive parameters

Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

1 files changed, 84 insertions, 34 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 1f1700b4d6..895561324b 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -20,7 +20,6 @@ open Nameops
 open Constrexpr
 open Constrexpr_ops
 open Constrintern
-open Reductionops
 open Type_errors
 open Pretyping
 open Context.Rel.Declaration
@@ -51,20 +50,6 @@ let should_auto_template =
     if b then warn_auto_template id;
     b
 
-let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
-  | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
-  | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
-  | CHole (k, _, _) ->
-      let (has_no_args,name,params) = a in
-      if not has_no_args then
-        user_err ?loc
-         (strbrk"Cannot infer the non constant arguments of the conclusion of "
-          ++ Id.print cs ++ str ".");
-      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
-      CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
-  | c -> c
-  )
-
 let push_types env idl rl tl =
   List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env)
     env idl rl tl
@@ -93,10 +78,6 @@ let check_all_names_different indl =
   | [] -> ()
   | _ -> raise (InductiveError (SameNamesOverlap l))
 
-let mk_mltype_data sigma env assums arity indname =
-  let is_ml_type = is_sort env sigma arity in
-  (is_ml_type,indname,assums)
-
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
     This is really a hack to stay compatible with the semantics of template polymorphic
@@ -145,16 +126,50 @@ let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
     in
     sigma, (t, Retyping.relevance_of_sort s, concl, impls)
 
-let interp_cstrs env sigma impls mldata arity ind =
+(* ind_rel is the Rel for this inductive in the context without params.
+   n is how many arguments there are in the constructor. *)
+let model_conclusion env sigma ind_rel params n arity_indices =
+  let model_head = EConstr.mkRel (n + Context.Rel.length params + ind_rel) in
+  let model_params = Context.Rel.to_extended_vect EConstr.mkRel n params in
+  let sigma,model_indices =
+    List.fold_right
+      (fun (_,t) (sigma, subst) ->
+        let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) (EConstr.Vars.liftn 1 (List.length params + List.length subst + 1) t)) in
+        let sigma, c = Evarutil.new_evar env sigma t in
+        sigma, c::subst)
+      arity_indices (sigma, []) in
+  sigma, EConstr.mkApp (EConstr.mkApp (model_head, model_params), Array.of_list (List.rev model_indices))
+
+let interp_cstrs env (sigma, ind_rel) impls params ind arity =
   let cnames,ctyps = List.split ind.ind_lc in
-  (* Complete conclusions of constructor types if given in ML-style syntax *)
-  let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
+  let arity_indices, cstr_sort = Reductionops.splay_arity env sigma arity in
   (* Interpret the constructor types *)
-  let sigma, (ctyps'', cimpls) =
+  let interp_cstr sigma ctyp =
+    let flags =
+      Pretyping.{ all_no_fail_flags with
+                  use_typeclasses = false;
+                  solve_unification_constraints = false }
+    in
+    let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in
+    let ctx, concl = Reductionops.splay_prod_assum env sigma ctyp in
+    let concl_env = EConstr.push_rel_context ctx env in
+    let sigma_with_model_evars, model =
+      model_conclusion concl_env sigma ind_rel params (Context.Rel.length ctx) arity_indices
+    in
+    (* unify the expected with the provided conclusion *)
+    let sigma =
+      try Evarconv.unify concl_env sigma_with_model_evars Reduction.CONV concl model
+      with Evarconv.UnableToUnify (sigma,e) ->
+        user_err (Himsg.explain_pretype_error concl_env sigma
+                    (Pretype_errors.CannotUnify (concl, model, (Some e))))
+    in
+    sigma, (ctyp, cimpl)
+  in
+  let sigma, (ctyps, cimpls) =
     on_snd List.split @@
-    List.fold_left_map (fun sigma l ->
-        interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in
-  sigma, (cnames, ctyps'', cimpls)
+    List.fold_left_map interp_cstr sigma ctyps
+  in
+  (sigma, pred ind_rel), (cnames, ctyps, cimpls)
 
 let sign_level env evd sign =
   fst (List.fold_right
@@ -427,6 +442,30 @@ let interp_params env udecl uparamsl paramsl =
   sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
   List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
 
+(* When a hole remains for a param, pretend the param is uniform and
+   do the unification.
+   [env_ar_par] is [uparams; inds; params]
+ *)
+let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
+  let is_ind sigma k c = match EConstr.kind sigma c with
+    | Constr.Rel n ->
+      (* env is [uparams; inds; params; k other things] *)
+      n > k + nparams && n <= k + nparams + ninds
+    | _ -> false
+  in
+  let rec aux (env,k as envk) sigma c = match EConstr.kind sigma c with
+    | Constr.App (h,args) when is_ind sigma k h ->
+      Array.fold_left_i (fun i sigma arg ->
+          if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
+          else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)))
+        sigma args
+    | _ -> Termops.fold_constr_with_full_binders
+             sigma
+             (fun d (env,k) -> EConstr.push_rel d env, k+1)
+             aux envk sigma c
+  in
+  aux (env_ar_par,0) sigma c
+
 let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -466,18 +505,29 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
   let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
-  let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
 
-  let sigma, constructors =
+  let ninds = List.length indl in
+  let (sigma, _), constructors =
     Metasyntax.with_syntax_protection (fun () ->
-     (* Temporary declaration of notations and scopes *)
-     List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
-     (* Interpret the constructor types *)
-     List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl)
-     () in
+        (* Temporary declaration of notations and scopes *)
+        List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
+        (* Interpret the constructor types *)
+        List.fold_left2_map
+          (fun (sigma, ind_rel) -> interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params)
+          (sigma, ninds) indl arities)
+      ()
+  in
 
-  (* generalize over the uniform parameters *)
   let nparams = Context.Rel.length ctx_params in
+  let sigma =
+    List.fold_left (fun sigma (_,ctyps,_) ->
+        List.fold_left (fun sigma ctyp ->
+            maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp)
+          sigma ctyps)
+      sigma constructors
+  in
+
+  (* generalize over the uniform parameters *)
   let nuparams = Context.Rel.length ctx_uparams in
   let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in
   let uparam_subst =