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>

9 files changed, 138 insertions, 63 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6e929de581..3d38713e09 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -514,7 +514,8 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
     else tclass
   in
   let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
-  let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in
+  let flags = Pretyping.{ all_no_fail_flags with program_mode } in
+  let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in
   let imps = imps @ imps' in
   let ctx', c = decompose_prod_assum sigma c' in
   let ctx'' = ctx' @ ctx in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 47ae03e0a3..1e2e2e53e2 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -70,7 +70,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   (gr,inst)
 
 let interp_assumption ~program_mode sigma env impls c =
-  let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in
   sigma, (ty, impls)
 
 (* When monomorphic the universe constraints and universe names are
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 8a91e9e63f..66d5a4f7f5 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,6 +79,7 @@ let protect_pattern_in_binder bl c ctypopt =
     (bl, c, ctypopt, fun f env evd c -> f env evd c)
 
 let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
+  let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -87,7 +88,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
   (* Build the type *)
   let evd, tyopt = Option.fold_left_map
-      (interp_type_evars_impls ~program_mode ~impls env_bl)
+      (interp_type_evars_impls ~flags ~impls env_bl)
       evd ctypopt
   in
   (* Build the body, and merge implicits from parameters and from type/body *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index cbf0affc12..e4fa212a23 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,7 +107,8 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
-  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in
+  let flags = Pretyping.{ all_no_fail_flags with program_mode } in
+  let sigma, (c, impl) = interp_type_evars_impls ~flags ~impls env sigma fix.Vernacexpr.rtype in
   let r = Retyping.relevance_of_type env sigma c in
   sigma, (c, r, impl)
 
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 =
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 2b9da1d4e5..984581152a 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -88,3 +88,9 @@ val template_polymorphism_candidate
    polymorphic. It should have at least one universe in its
    monomorphic universe context that can be made parametric in its
    conclusion sort, if one is given. *)
+
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+  -> EConstr.t -> Evd.evar_map
+(** [nparams] is the number of parameters which aren't treated as
+    uniform, ie the length of params (including letins) where the env
+    is [uniform params, inductives, params]. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 56780d00a6..80e7e6ab96 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -195,12 +195,12 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let lift_lets = lift_rel_context 1 letbinders in
   let sigma, intern_body =
     let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
-    let (r, l, impls, scopes) =
+    let (r, impls, scopes) =
       Constrintern.compute_internalization_data env sigma
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
+        (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
          scopes @ [None]) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/record.ml b/vernac/record.ml
index d974ead942..785ed89372 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -59,26 +59,37 @@ let () =
       optread  = (fun () -> !typeclasses_unique);
       optwrite = (fun b -> typeclasses_unique := b); }
 
-let interp_fields_evars env sigma impls_env nots l =
-  List.fold_left2
-    (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
-      let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
-      let r = Retyping.relevance_of_type env sigma t' in
-      let sigma, b' =
-        Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
-                      interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
-      let impls =
-        match i with
-        | Anonymous -> impls
-        | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
-      in
-      let d = match b' with
-              | None -> LocalAssum (make_annot i r,t')
-              | Some b' -> LocalDef (make_annot i r,b',t')
+let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
+  let _, sigma, impls, newfs, _ =
+    List.fold_left2
+      (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
+         let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
+         let r = Retyping.relevance_of_type env sigma t' in
+         let sigma, b' =
+           Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
+                         interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
+         let impls =
+           match i with
+           | Anonymous -> impls
+           | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
+         in
+         let d = match b' with
+           | None -> LocalAssum (make_annot i r,t')
+           | Some b' -> LocalDef (make_annot i r,b',t')
+         in
+         List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
+         (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
+      (env, sigma, [], [], impls_env) nots l
+  in
+  let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+      let sigma = RelDecl.fold_constr (fun c sigma ->
+          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+          f sigma
       in
-      List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
-      (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
-    (env, sigma, [], [], impls_env) nots l
+      EConstr.push_rel f env, sigma)
+      newfs
+  in
+  sigma, (impls, newfs)
 
 let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
@@ -165,9 +176,10 @@ let typecheck_params_and_fields finite def poly pl ps records =
     let imps = List.map (fun _ -> imps) arities in
     compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps
   in
+  let ninds = List.length arities in
+  let nparams = List.length newps in
   let fold sigma (_, _, nots, fs) arity =
-    let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in
-    (sigma, (impls, newfs))
+    interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs)
   in
   let (sigma, data) = List.fold_left2_map fold sigma records arities in
   let sigma =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4806c6bb9c..2e509921c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -486,11 +486,14 @@ let program_inference_hook env sigma ev =
 
 let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let env0 = Global.env () in
+  let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
-    let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in
-    let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in
+    let evd, (impls, ((env, ctx), imps)) =
+      Constrintern.interp_context_evars ~program_mode env0 evd bl
+    in
+    let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
     let flags = Pretyping.{ all_and_fail_flags with program_mode } in
     let inference_hook = if program_mode then Some program_inference_hook else None in
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in