Check subtyping of inductive types in Kernel

5 files changed, 39 insertions, 32 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index ad53bf898..51957e00a 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1129,12 +1129,3 @@ let univ_inf_ind_from_universe_context univcst =
       (Array.map (fun _ -> new_univ_level ())
          (Instance.to_array (UContext.instance univcst)))
   in UInfoInd.from_universe_context univcst freshunivs
-
-(** This function adds universe constraints to the universe
-    constraints of the given universe_info_ind. However one must be
-    CAUTIOUS as it resets the subtyping constraints to equality. *)
-let univ_inf_ind_union uinfind univcst' =
-  let freshunivs = Instance.of_array
-      (Array.map (fun _ -> new_univ_level ())
-         (Instance.to_array (UContext.instance univcst')))
-  in UInfoInd.union uinfind univcst' freshunivs
diff --git a/engine/universes.mli b/engine/universes.mli
index 17a9deb3a..1b9703c7b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -233,8 +233,3 @@ val solve_constraints_system : universe option array -> universe array -> univer
 (** Given a universe context representing constraints of an inductive
     this function produces a UInfoInd.t that with the trivial subtyping relation. *)
 val univ_inf_ind_from_universe_context : universe_context -> universe_info_ind
-
-(** This function adds universe constraints to the universe
-    constraints of the given universe_info_ind. However one must be
-    CAUTIOUS as it resets the subtyping constraints to equality. *)
-val univ_inf_ind_union : universe_info_ind -> universe_context -> universe_info_ind
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 94bf1a770..068332406 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -207,6 +207,24 @@ let param_ccls paramsctxt =
   in
   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_typ typ typ_env =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try 
+           basic_check 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 = Context.Rel.fold_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
 (* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -345,6 +363,22 @@ let typecheck_inductive env mie =
       in
 	(id,cn,lc,(sign,arity)))
     inds
+  in
+  (* 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 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
+    (* 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 true) lc
+        | TemplateArity _ -> ()
+          (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *)
+    ) inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f124bb39e..4a4cf1baa 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1049,7 +1049,7 @@ struct
   let empty = (UContext.empty, UContext.empty)
   let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst
 
-  let halve_context (ctx : Instance.t) : Instance.t * Instance.t =
+  let halve_context ctx =
     let len = Array.length (Instance.to_array ctx) in
     let halflen = len / 2 in
     (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
@@ -1084,17 +1084,9 @@ struct
     (univcst, UContext.make (Instance.append inst freshunivs,
                              create_trivial_subtyping inst freshunivs))
 
-  (** This function adds universe constraints to the universe
-      constraints of the given universe_info_ind. However one must be
-      CAUTIOUS as it resets the subtyping constraints to equality. It
-      also requires fresh universes for the newly introduced
-      universes *)
-  let union (univcst, _) univcst' freshunivs =
-    assert (Instance.length freshunivs = Instance.length (UContext.instance univcst'));
-    let (ctx, ctx') = halve_context (UContext.instance univcst) in
-    let newctx' = Instance.append ctx' freshunivs in
-    let univcstunion = UContext.union univcst univcst' in
-    (univcstunion, subtyp_context (from_universe_context univcstunion newctx'))
+  let subtyping_susbst (univcst, subtypcst) = 
+      let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in
+      Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
 
   let dest x = x
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 630d0d949..f139a8b33 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -345,12 +345,7 @@ sig
       trivial subtyping relation. *)
   val from_universe_context : universe_context -> universe_instance -> t
 
-  (** This function adds universe constraints to the universe
-      constraints of the given universe_info_ind. However one must be
-      CAUTIOUS as it resets the subtyping constraints to equality. It
-      also requires fresh universes for the newly introduced
-      universes *)
-  val union : t -> universe_context -> universe_instance -> t
+  val subtyping_susbst : t -> universe_level_subst
 
   val size : t -> int