1 files changed, 63 insertions, 1 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 6c38f38e29..54dec56b54 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -524,13 +524,67 @@ let check_positivity env_ar mind params nrecp inds =
   let wfp = Rtree.mk_rec irecargs in
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) 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') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = dest_prod env arcn in
+  let last_env = fold_rel_context_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+(* 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 check_subtyping cumi paramsctxt env_ar inds =
+  let numparams = rel_context_nhyps paramsctxt in
+  let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+  let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in
+  let dosubst = subst_univs_level_constr sbsubst in
+  let uctx = Univ.CumulativityInfo.univ_context cumi in
+  let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
+  let env = Environ.push_context uctx env_ar 
+  in
+  let env = Environ.push_context uctx_other env 
+  in
+  let env =  Environ.push_context 
+      (Univ.CumulativityInfo.subtyp_context cumi) env
+  in
+  (* process individual inductive types: *)
+  Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
+      match arity with
+      | RegularArity { mind_user_arity = full_arity} ->
+        check_subtyping_arity_constructor env dosubst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+      | TemplateArity _ -> ()
+    ) inds
+    
 (************************************************************************)
 (************************************************************************)
 
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in
+  let ind_ctx =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> ctx
+    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi -> 
+      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  in
+  let env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
@@ -547,6 +601,14 @@ let check_inductive env kn mib =
   let env_ar = typecheck_arity env params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  (* check the inferred subtyping relation *)
+  let () = 
+    match mib.mind_universes with
+    | Monomorphic_ind _ | Polymorphic_ind _ -> ()
+    | Cumulative_ind acumi ->
+      check_subtyping 
+        (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets
+  in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)