Fixing the checker w.r.t. wrongly used abstract universe contexts.

It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.

This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.

1 files changed, 22 insertions, 22 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 92e94c1ab..22c843812 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -525,10 +525,10 @@ let check_positivity env_ar mind params nrecp inds =
   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 check_subtyping_arity_constructor env (subst : Univ.Instance.t) (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);
+    if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp);
     numchecked := !numchecked + 1
   in
   let check_typ typ typ_env =
@@ -548,26 +548,27 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 
 (* 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 check_subtyping cumi paramsctxt env inds =
+  let open Univ in
   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
+  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+      with the cumulativity constraints [ cumul_cst ]. *)
+  let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
+  let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+  let other_context = ACumulativityInfo.univ_context cumi in
+  let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
+  let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
+  let cumul_cst = UContext.constraints cumul_context in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.add_constraints cumul_cst 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
+        check_subtyping_arity_constructor env inst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc
       | TemplateArity _ -> ()
     ) inds
     
@@ -579,10 +580,10 @@ let check_inductive env kn mib =
   (* check mind_constraints: should be consistent with env *)
   let ind_ctx =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> ctx
-    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *)
+    | Polymorphic_ind auctx -> Univ.AUContext.repr auctx
     | Cumulative_ind cumi -> 
-      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+      Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
   in
   let env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -606,8 +607,7 @@ let check_inductive env kn mib =
     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
+      check_subtyping 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;