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>

16 files changed, 225 insertions, 160 deletions

diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
new file mode 100644
index 0000000000..75358ab4ad
--- /dev/null
+++ b/doc/changelog/02-specification-language/11579-inductive-params.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  Treatment of implicit inductive parameters in inductive declarations is less adhoc.
+  (`#11579 <https://github.com/coq/coq/pull/11579>`_,
+  by Maxime Dénès, Gaëtan Gilbert and Jasper Hugunin).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a071ba7ec9..9a69af0f64 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -57,9 +57,6 @@ type var_internalization_data =
     (* type of the "free" variable, for coqdoc, e.g. while typing the
        constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
     var_internalization_type *
-    (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
-       in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    Id.t list *
     (* signature of impargs of the variable *)
     Impargs.implicit_status list *
     (* subscopes of the args of the variable *)
@@ -180,20 +177,9 @@ let parsing_explicit = ref false
 
 let empty_internalization_env = Id.Map.empty
 
-let compute_explicitable_implicit imps = function
-  | Inductive (params,_) ->
-      (* In inductive types, the parameters are fixed implicit arguments *)
-      let sub_impl,_ = List.chop (List.length params) imps in
-      let sub_impl' = List.filter is_status_implicit sub_impl in
-      List.map name_of_implicit sub_impl'
-  | Recursive | Method | Variable ->
-      (* Unable to know in advance what the implicit arguments will be *)
-      []
-
 let compute_internalization_data env sigma ty typ impl =
   let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
-  let expls_impl = compute_explicitable_implicit impl ty in
-  (ty, expls_impl, impl, compute_arguments_scope sigma typ)
+  (ty, impl, compute_arguments_scope sigma typ)
 
 let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
   List.fold_left3
@@ -355,7 +341,7 @@ let impls_binder_list =
 let impls_type_list n ?(args = []) =
   let rec aux acc n c = match DAst.get c with
     | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
-    | _ -> (Variable,[],List.rev acc,[])
+    | _ -> (Variable,List.rev acc,[])
   in aux args n
 
 let impls_term_list n ?(args = []) =
@@ -365,7 +351,7 @@ let impls_term_list n ?(args = []) =
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
        aux acc' n bds.(nb)
-    |_ -> (Variable,[],List.rev acc,[])
+    |_ -> (Variable,List.rev acc,[])
   in aux args n
 
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
@@ -431,12 +417,12 @@ let locate_if_hole ?loc na c = match DAst.get c with
 
 let reset_hidden_inductive_implicit_test env =
   { env with impls = Id.Map.map (function
-         | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d)
+         | (Inductive (params,_),b,c) -> (Inductive (params,false),b,c)
          | x -> x) env.impls }
 
 let check_hidden_implicit_parameters ?loc id impls =
   if Id.Map.exists (fun _ -> function
-    | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams
+    | (Inductive (indparams,check),_,_) when check -> Id.List.mem id indparams
     | _ -> false) impls
   then
     user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++
@@ -492,7 +478,7 @@ let intern_generalized_binder intern_type ntnvars
   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
   let env' = List.fold_left
-    (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
+    (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x))
     env fvs in
   let b' = check_implicit_meaningful ?loc b' env in
   let bl = List.map
@@ -559,7 +545,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
       user_err ?loc (str "Unsupported nested \"as\" clause.");
     il,disjpat
   in
-  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in
+  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in
   let na = alias_of_pat (List.hd disjpat) in
   let ienv = Name.fold_right Id.Set.remove na env.ids in
   let id = Namegen.next_name_away_with_default "pat" na ienv in
@@ -615,7 +601,7 @@ let intern_generalization intern env ntnvars loc bk ak c =
             GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
     in
       List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
-        let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
+        let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in
           (env', abs lid acc)) fvs (env,c)
   in c'
 
@@ -706,7 +692,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_patvar pat in
-      let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
+      let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in
       (renaming,env), None, na
     else
       (* Interpret as a pattern *)
@@ -1031,27 +1017,25 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
   if Id.Map.mem id ntnvars then
     begin
       if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars;
-      gvar (loc,id) us, [], [], []
+      gvar (loc,id) us, [], []
     end
   else
   (* Is [id] registered with implicit arguments *)
   try
-    let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
-    let expl_impls = List.map
-      (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
+    let ty,impls,argsc = Id.Map.find id env.impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
-    gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
+    gvar (loc,id) us, make_implicits_list impls, argsc
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
   if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars
   then
-    gvar (loc,id) us, [], [], []
+    gvar (loc,id) us, [], []
   else if Id.equal id ldots_var
   (* Is [id] the special variable for recursive notations? *)
   then if Id.Map.is_empty ntnvars
     then error_ldots_var ?loc
-    else gvar (loc,id) us, [], [], []
+    else gvar (loc,id) us, [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err ?loc ~hdr:"intern_var"
@@ -1067,17 +1051,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
         let scopes = find_arguments_scope ref in
         Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
         (* Someday we should stop relying on Dumglob raising exceptions *)
-        DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
+        DAst.make ?loc @@ GRef (ref, us), impls, scopes
       with e when CErrors.noncritical e ->
         (* [id] a goal variable *)
-        gvar (loc,id) us, [], [], []
+        gvar (loc,id) us, [], []
 
 let find_appl_head_data c =
   match DAst.get c with
   | GRef (ref,_) ->
     let impls = implicits_of_global ref in
     let scopes = find_arguments_scope ref in
-      c, impls, scopes, []
+      c, impls, scopes
   | GApp (r, l) ->
     begin match DAst.get r with
     | GRef (ref,_) ->
@@ -1085,10 +1069,10 @@ let find_appl_head_data c =
       let impls = implicits_of_global ref in
       let scopes = find_arguments_scope ref in
         c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
-        List.skipn_at_least n scopes,[]
-    | _ -> c,[],[],[]
+        List.skipn_at_least n scopes
+    | _ -> c,[],[]
     end
-  | _ -> c,[],[],[]
+  | _ -> c,[],[]
 
 let error_not_enough_arguments ?loc =
   user_err ?loc  (str "Abbreviation is not applied enough.")
@@ -1196,13 +1180,12 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
       try
         let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
         check_applied_projection isproj realref qid;
-        let x, imp, scopes, l = find_appl_head_data r in
-          (x,imp,scopes,l), args2
+        find_appl_head_data r, args2
       with Not_found ->
         (* Extra allowance for non globalizing functions *)
         if !interning_grammar || env.unb then
           (* check_applied_projection ?? *)
-          (gvar (loc,qualid_basename qid) us, [], [], []), args
+          (gvar (loc,qualid_basename qid) us, [], []), args
         else Nametab.error_global_not_found qid
   else
     let r,realref,args2 =
@@ -1210,11 +1193,10 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
       with Not_found -> Nametab.error_global_not_found qid
     in
     check_applied_projection isproj realref qid;
-    let x, imp, scopes, l = find_appl_head_data r in
-    (x,imp,scopes,l), args2
+    find_appl_head_data r, args2
 
 let interp_reference vars r =
-  let (r,_,_,_),_ =
+  let (r,_,_),_ =
     intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env;
@@ -1882,18 +1864,6 @@ let intern_ind_pattern genv ntnvars scopes pat =
 (**********************************************************************)
 (* Utilities for application                                          *)
 
-let merge_impargs l args =
-  let test x = function
-  | (_, Some {v=y}) -> explicitation_eq x y
-  | _ -> false
-  in
-  List.fold_right (fun a l ->
-    match a with
-      | (_, Some {v=ExplByName id as x}) when
-          List.exists (test x) args -> l
-      | _ -> a::l)
-    l args
-
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
@@ -1954,11 +1924,11 @@ let extract_explicit_arg imps args =
 let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
   let rec intern env = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
-        let (c,imp,subscopes,l),_ =
+        let (c,imp,subscopes),_ =
           intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
             lvar us [] ref
         in
-          apply_impargs c env imp subscopes l loc
+          apply_impargs c env imp subscopes [] loc
 
     | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
         let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
@@ -2053,8 +2023,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (_,ntn,args) ->
         let c = intern_notation intern env ntnvars loc ntn args in
-        let x, impl, scopes, l = find_appl_head_data c in
-        apply_impargs x env impl scopes l loc
+        let x, impl, scopes = find_appl_head_data c in
+        apply_impargs x env impl scopes [] loc
     | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
     | CPrim p ->
@@ -2063,7 +2033,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         intern {env with tmp_scope = None;
                   scopes = find_delimiters_scope ?loc key :: env.scopes} e
     | CAppExpl ((isproj,ref,us), args) ->
-        let (f,_,args_scopes,_),args =
+        let (f,_,args_scopes),args =
           let args = List.map (fun a -> (a,None)) args in
           intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
             lvar us args ref
@@ -2074,25 +2044,24 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
-        let isproj,f,args = match f.CAst.v with
-          (* Compact notations like "t.(f args') args" *)
-          | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
-            isproj',f,args'@args
-          (* Don't compact "(f args') args" to resolve implicits separately *)
-          | _ -> isproj,f,args in
-        let (c,impargs,args_scopes,l),args =
-          match f.CAst.v with
-            | CRef (ref,us) ->
-               intern_applied_reference ~isproj intern env
-                 (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (_,ntn,ntnargs) ->
-                assert (Option.is_empty isproj);
-                let c = intern_notation intern env ntnvars loc ntn ntnargs in
-                let x, impl, scopes, l = find_appl_head_data c in
-                  (x,impl,scopes,l), args
-            | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
-          apply_impargs c env impargs args_scopes
-            (merge_impargs l args) loc
+      let isproj,f,args = match f.CAst.v with
+        (* Compact notations like "t.(f args') args" *)
+        | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
+          isproj',f,args'@args
+        (* Don't compact "(f args') args" to resolve implicits separately *)
+        | _ -> isproj,f,args in
+      let (c,impargs,args_scopes),args =
+        match f.CAst.v with
+        | CRef (ref,us) ->
+          intern_applied_reference ~isproj intern env
+            (Environ.named_context_val globalenv) lvar us args ref
+        | CNotation (_,ntn,ntnargs) ->
+          assert (Option.is_empty isproj);
+          let c = intern_notation intern env ntnvars loc ntn ntnargs in
+          find_appl_head_data c, args
+        | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in
+      apply_impargs c env impargs args_scopes
+        args loc
 
     | CRecord fs ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -2133,7 +2102,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             List.rev_append match_td matchs)
           tms ([],Id.Set.empty,Id.Map.empty,[]) in
         let env' = Id.Set.fold
-          (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
+          (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var))
           (Id.Set.union ex_ids as_in_vars)
           (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in
         (* PatVars before a real pattern do not need to be matched *)
@@ -2170,17 +2139,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
-          let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+          let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env')
             (CAst.make na') in
           intern_type (slide_binders env'') u) po in
         DAst.make ?loc @@
         GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
-          let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
+          let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env)
             (CAst.make na') in
           intern_type (slide_binders env'') p) po in
         DAst.make ?loc @@
@@ -2478,22 +2447,23 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c =
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls ?(program_mode=false) env sigma
+let interp_constr_evars_gen_impls ?(flags=Pretyping.all_no_fail_flags) env sigma
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env sigma c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-  let flags = { Pretyping.all_no_fail_flags with program_mode } in
   let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
   sigma, (c, imps)
 
-let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) c =
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  interp_constr_evars_gen_impls ~flags env sigma ~impls WithoutTypeConstraint c
 
-let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars_impls ?(program_mode=false) env evdref ?(impls=empty_internalization_env) c typ =
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  interp_constr_evars_gen_impls ~flags env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c
+let interp_type_evars_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls ~flags env sigma ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9d36bf2151..fb1c6684a1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -48,10 +48,6 @@ type var_internalization_data =
       (* type of the "free" variable, for coqdoc, e.g. while typing the
          constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
 
-    Id.t list *
-      (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
-         in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-
     Impargs.implicit_status list * (* signature of impargs of the variable *)
     Notation_term.scope_name option list (* subscopes of the args of the variable *)
 
@@ -132,7 +128,7 @@ val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map ->
+val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (types * Impargs.manual_implicits)
 
diff --git a/test-suite/bugs/closed/bug_11585.v b/test-suite/bugs/closed/bug_11585.v
new file mode 100644
index 0000000000..6294668323
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11585.v
@@ -0,0 +1,3 @@
+Fail Inductive type {type : Type} : Type := T : type.
+
+Inductive type {type : Type} : Type := T .
diff --git a/test-suite/bugs/closed/bug_5233.v b/test-suite/bugs/closed/bug_5233.v
index 06286c740d..63e33b63f7 100644
--- a/test-suite/bugs/closed/bug_5233.v
+++ b/test-suite/bugs/closed/bug_5233.v
@@ -1,2 +1,5 @@
 (* Implicit arguments on type were missing for recursive records *)
 Inductive foo {A : Type} : Type := { Foo : foo }.
+
+(* Implicit arguments can be overidden *)
+Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index ff2556c5dc..e6c2806433 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,10 @@
 The command has indeed failed with message:
-Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+In environment
+list' : Set -> Set
+A : Set
+a : A
+l : list' A
+Unable to unify "list' (A * A)%type" with "list' A".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
new file mode 100644
index 0000000000..9b787867fc
--- /dev/null
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -0,0 +1,10 @@
+Class C := {}.
+
+Definition useC {c:C} := nat.
+
+Inductive foo {a b : C} := CC : useC -> foo.
+(* If TC search runs before parameter unification it will pick the
+   wrong instance for the first parameter.
+
+   useC makes sure we don't completely skip TC search.
+*)
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