Infrastructure for cumulative inductive syntax (no grammar extension yet)

12 files changed, 111 insertions, 43 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 7bb714aa17..7513564cf0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -69,6 +69,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   in
   let mind_entry_template = Array.exists check_template mb.mind_packets in
   let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
+  let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
@@ -76,7 +77,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_template;
-    mind_entry_cumulative= Option.has_some mb.mind_variance;
+    mind_entry_variance;
     mind_entry_private = mb.mind_private;
   }
 
diff --git a/checker/checker.ml b/checker/checker.ml
index e2c90e2b93..08d92bb7b3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -298,7 +298,9 @@ let explain_exn = function
       | DisallowedSProp -> str"DisallowedSProp"
       | BadRelevance -> str"BadRelevance"
       | BadInvert -> str"BadInvert"
-      | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
+      | UndeclaredUniverse _ -> str"UndeclaredUniverse"
+      | BadVariance _ -> str "BadVariance"
+      ))
 
   | InductiveError e ->
       hov 0 (str "Error related to inductive types")
diff --git a/kernel/entries.ml b/kernel/entries.ml
index ae64112e33..b0bb9cabef 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -50,9 +50,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
   mind_entry_template : bool; (* Use template polymorphism *)
-  mind_entry_cumulative : bool;
-  (* universe constraints and the constraints for subtyping of
-     inductive types in the block. *)
+  mind_entry_variance : Univ.Variance.t option array option;
+  (* [None] if non-cumulative, otherwise associates each universe of
+     the entry to [None] if to be inferred or [Some v] if to be
+     checked. *)
   mind_entry_private : bool option;
 }
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b2520b780f..33ee8c325a 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -369,15 +369,20 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  let variance = if not mie.mind_entry_cumulative then None
-    else match mie.mind_entry_universes with
+  let variance = match mie.mind_entry_variance with
+    | None -> None
+    | Some variances ->
+      match mie.mind_entry_universes with
       | Monomorphic_entry _ ->
         CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
       | Polymorphic_entry (_,uctx) ->
         let univs = Instance.to_array @@ UContext.instance uctx in
+        let univs = Array.map2 (fun a b -> a,b) univs variances in
         let univs = match sec_univs with
           | None -> univs
-          | Some sec_univs -> Array.append sec_univs univs
+          | Some sec_univs ->
+            let sec_univs = Array.map (fun u -> u, None) sec_univs in
+            Array.append sec_univs univs
         in
         let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
         Some variances
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 8191a5b0f3..2f9fb8686d 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -15,30 +15,74 @@ open Univ
 open Variance
 open Util
 
-type inferred = IrrelevantI | CovariantI
-
-(** Throughout this module we modify a map [variances] from local
-    universes to [inferred]. It starts as a trivial mapping to
-    [Irrelevant] and every time we encounter a local universe we
-    restrict it accordingly.
-    [Invariant] universes are removed from the map.
-*)
 exception TrivialVariance
+exception BadVariance of Level.t
 
-let maybe_trivial variances =
-  if LMap.is_empty variances then raise TrivialVariance
-  else variances
+module Inf : sig
+  type variances
+  val infer_level_eq : Level.t -> variances -> variances
+  val infer_level_leq : Level.t -> variances -> variances
+  val start : (Level.t * Variance.t option) array -> variances
+  val finish : variances -> Variance.t array
+end = struct
+  type inferred = IrrelevantI | CovariantI
+  type mode = Check | Infer
 
-let infer_level_eq u variances =
-  maybe_trivial (LMap.remove u variances)
+  (**
+     Each local universe is either in the [univs] map or is Invariant.
 
-let infer_level_leq u variances =
-  (* can only set Irrelevant -> Covariant so nontrivial *)
-  LMap.update u (function
-      | None -> None
-      | Some CovariantI as x -> x
-      | Some IrrelevantI -> Some CovariantI)
-    variances
+     If [univs] is empty all universes are Invariant and there is nothing more to do,
+     so we stop by raising [TrivialVariance]. The [soft] check comes before that.
+  *)
+  type variances = {
+    orig_array : (Level.t * Variance.t option) array;
+    univs : (mode * inferred) LMap.t;
+  }
+
+  let infer_level_eq u variances =
+    match LMap.find_opt u variances.univs with
+    | None -> variances
+    | Some (Check, _) -> raise (BadVariance u)
+    | Some (Infer, _) ->
+      let univs = LMap.remove u variances.univs in
+      if LMap.is_empty univs then raise TrivialVariance;
+      {variances with univs}
+
+  let infer_level_leq u variances =
+    (* can only set Irrelevant -> Covariant so no TrivialVariance *)
+    let univs =
+      LMap.update u (function
+          | None -> None
+          | Some (_,CovariantI) as x -> x
+          | Some (Infer,IrrelevantI) ->
+            Some (Infer,CovariantI)
+          | Some (Check,IrrelevantI) -> raise (BadVariance u))
+        variances.univs
+    in
+    if univs == variances.univs then variances else {variances with univs}
+
+  let start us =
+    let univs = Array.fold_left (fun univs (u,variance) ->
+        match variance with
+        | None -> LMap.add u (Infer,IrrelevantI) univs
+        | Some Invariant -> univs
+        | Some Covariant -> LMap.add u (Check,CovariantI) univs
+        | Some Irrelevant -> LMap.add u (Check,IrrelevantI) univs)
+        LMap.empty us
+    in
+    if LMap.is_empty univs then raise TrivialVariance;
+    {univs; orig_array=us}
+
+  let finish variances =
+    Array.map (fun (u,_check) ->
+        match LMap.find_opt u variances.univs with
+        | None -> Invariant
+        | Some (_,CovariantI) -> Covariant
+        | Some (_,IrrelevantI) -> Irrelevant)
+      variances.orig_array
+
+end
+open Inf
 
 let infer_generic_instance_eq variances u =
   Array.fold_left (fun variances u -> infer_level_eq u variances)
@@ -204,11 +248,7 @@ let infer_arity_constructor is_arity env variances arcn =
 open Entries
 
 let infer_inductive_core env univs entries =
-  if Array.is_empty univs then raise TrivialVariance;
-  let variances =
-    Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
-      LMap.empty univs
-  in
+  let variances = Inf.start univs in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -218,12 +258,10 @@ let infer_inductive_core env univs entries =
       variances
       entries
   in
-  Array.map (fun u -> match LMap.find u variances with
-      | exception Not_found -> Invariant
-      | IrrelevantI -> Irrelevant
-      | CovariantI -> Covariant)
-    univs
+  Inf.finish variances
 
 let infer_inductive ~env_params univs entries =
   try infer_inductive_core env_params univs entries
-  with TrivialVariance -> Array.make (Array.length univs) Invariant
+  with
+  | TrivialVariance -> Array.make (Array.length univs) Invariant
+  | BadVariance u -> Type_errors.error_bad_variance env_params u
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index db5539a0ff..99d8f0c98d 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -12,8 +12,8 @@ val infer_inductive
   : env_params:Environ.env
   (** Environment containing the polymorphic universes and the
      parameters. *)
-  -> Univ.Level.t array
-  (** Universes whose cumulativity we want to infer. *)
+  -> (Univ.Level.t * Univ.Variance.t option) array
+  (** Universes whose cumulativity we want to infer or check. *)
   -> Entries.one_inductive_entry list
   (** The inductive block data we want to infer cumulativity for.
       NB: we ignore the template bool and the names, only the terms
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index ae5c4b6880..624604976e 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
+  | BadVariance of Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -163,6 +164,9 @@ let error_bad_relevance env =
 let error_bad_invert env =
   raise (TypeError (env, BadInvert))
 
+let error_bad_variance env u =
+  raise (TypeError (env, BadVariance u))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -207,3 +211,4 @@ let map_ptype_error f = function
 | DisallowedSProp -> DisallowedSProp
 | BadRelevance -> BadRelevance
 | BadInvert -> BadInvert
+| BadVariance u -> BadVariance u
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b1f7eb8a34..7a7dba68b3 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -70,6 +70,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
+  | BadVariance of Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -146,5 +147,7 @@ val error_bad_relevance : env -> 'a
 
 val error_bad_invert : env -> 'a
 
+val error_bad_variance : env -> Level.t -> 'a
+
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..6b37958ab3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,6 +367,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
+let variance_of_entry ~cumulative = function
+  | Monomorphic_entry _ -> None
+  | Polymorphic_entry (nas,_) ->
+    Some (Array.map (fun _ -> None) nas)
+(* TODO syntax to have non-None elements *)
+
 let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
@@ -429,7 +435,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
       mind_entry_template = is_template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = variance_of_entry ~cumulative uctx;
     }
   in
   mind_ent, Evd.universe_binders sigma
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 91e8f609d5..1d9de11fcc 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -86,3 +86,6 @@ val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:
 (** [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, binders]. *)
+
+val variance_of_entry : cumulative:bool -> Entries.universes_entry
+  -> Univ.Variance.t option array option
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..c4f7e77714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,9 @@ let explain_bad_relevance env =
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."
 
+let explain_bad_variance env sigma u =
+  str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma u ++ str"."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -788,6 +791,7 @@ let explain_type_error env sigma err =
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
   | BadInvert -> explain_bad_invert env
+  | BadVariance u -> explain_bad_variance env sigma u
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/record.ml b/vernac/record.ml
index 891d7fcebe..e2e9bbd967 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -568,7 +568,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat
       mind_entry_private = None;
       mind_entry_universes = univs;
       mind_entry_template = template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = ComInductive.variance_of_entry ~cumulative univs;
     }
   in
   let impls = List.map (fun _ -> paramimpls, []) record_data in