Add subtyping inference for inductive types

2 files changed, 69 insertions, 6 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 17ce5483c7..15fe908359 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -208,8 +208,12 @@ let param_ccls paramsctxt =
   List.fold_left fold [] paramsctxt
 
 (* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity =
-  let basic_check ev tp = conv_leq ev tp (subst tp) in
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity =
+  let numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    numchecked := !numchecked + 1
+  in
   let check_typ typ typ_env =
    match typ with
      | LocalAssum (_, typ') ->
@@ -367,15 +371,22 @@ let typecheck_inductive env mie =
   (* Check that the subtyping information inferred for inductive types in the block is correct. *)
   (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
   let () =
+    let numparams = List.length paramsctxt in
     let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
     let dosubst = subst_univs_level_constr sbsubst in
-    let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in
+    let uctx = UInfoInd.univ_context mie.mind_entry_universes in
+    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+    let env' = Environ.push_context uctx env_ar_par in
+    let env'' = Environ.push_context uctx_other env' in
+    let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
     (* process individual inductive types: *)
     Array.iter (fun (id,cn,lc,(sign,arity)) ->
       match arity with
         | RegularArity (_, full_arity, _) ->
-           check_subtyping_arity_constructor envsb dosubst full_arity true;
-           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc
+           check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
+           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
         | TemplateArity _ -> ()
           (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *)
     ) inds
diff --git a/vernac/command.ml b/vernac/command.ml
index b76c2247b3..b23eb9e6bf 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,6 +573,32 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
+let infer_inductive_subtyping_arity_constructor
+  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
+  let update_contexts (env, evd, csts) csts' =
+    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
+  in
+  let basic_check (env, evd, csts) tp =
+    let csts' =
+      Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+    in update_contexts (env, evd, csts) csts'
+  in
+  let infer_typ typ ctxs =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try
+           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
+         with Reduction.NotConvertible -> 
+           anomaly ~label:"inference of record/inductive subtyping relation failed"
+             (Pp.str "Can't infer subtyping for record/inductive type")
+       end
+     | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = Reduction.dest_prod env arcn in
+  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
+  if not is_arity then basic_check last_contexts codom else last_contexts
+
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -649,6 +675,32 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
+  let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
+  let uinfind =
+    let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
+    let dosubst = subst_univs_level_constr sbsubst in
+    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+    let env' = Environ.push_context uctx env_ar_params in
+    let env' = Environ.push_context uctx_other env' in
+    let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
+    let (_, _, subtyp_constraints) =
+      List.fold_left
+       (fun ctxs indentry ->
+          let ctxs' = infer_inductive_subtyping_arity_constructor
+                        ctxs dosubst indentry.mind_entry_arity true
+          in
+          List.fold_left
+           (fun ctxs cons ->
+              infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
+           ctxs' indentry.mind_entry_lc
+       ) (env', evd', Univ.Constraint.empty) entries
+    in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
+         Univ.UContext.make
+           (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
+             subtyp_constraints))
+  in
   (* Build the mutual inductive entry *)
   { mind_entry_params = List.map prepare_param ctx_params;
     mind_entry_record = None;
@@ -656,7 +708,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx;
+    mind_entry_universes = uinfind;
   },
     pl, impls