Merge PR #864: Some cleanups after cumulativity for inductive types

11 files changed, 147 insertions, 35 deletions

diff --git a/API/API.mli b/API/API.mli
index a0e77edd1..a99cd2a9a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3782,6 +3782,12 @@ sig
     | DefaultInline
     | InlineAt of int
 
+  type cumulative_inductive_parsing_flag =
+    | GlobalCumulativity
+    | GlobalNonCumulativity
+    | LocalCumulativity
+    | LocalNonCumulativity
+
   type vernac_expr =
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_expr Loc.located
@@ -3806,7 +3812,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 2bb1301c7..cd36d1d32 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -134,12 +134,14 @@ producing global universe constraints, one can use the
 \asection{{\tt Cumulative, NonCumulative}}
 \comindex{Cumulative}
 \comindex{NonCumulative}
-\optindex{Inductive Cumulativity}
+\optindex{Polymorphic Inductive Cumulativity}
 
-Inductive types, coinductive types, variants and records can be
+Polymorphic inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
-there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative. Consider the examples below.
+there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
+makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
+inductive types and the like can be enforced to be
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
 Polymorphic Cumulative Inductive list {A : Type} :=
 | nil : list
@@ -158,24 +160,61 @@ This also means that any two instances of \texttt{list} are convertible:
 $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
 furthermore their corresponding (when fully applied to convertible arguments) constructors.
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
-Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
+The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
-Polymorphic NonCumulative Inductive list' {A : Type} :=
-| nil' : list'
-| cons' : A -> list' -> list'.
+Polymorphic Cumulative Record packType := {pk : Type}.
 \end{coq_example*}
 \begin{coq_example}
-Print list'.
+Print packType.
+\end{coq_example}
+Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
+convertible if and only if \texttt{i $=$ j}.
+
+Cumulative inductive types, coninductive types, variants and records
+only make sense when they are universe polymorphic. Therefore, an
+error is issued whenever the user uses the \texttt{Cumulative} or
+\texttt{NonCumulative} prefix in a monomorphic context.
+Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
+That is, this option, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used)
+but has no effect on \emph{monomorphic} inductive declarations.
+Consider the following examples.
+\begin{coq_example}
+Monomorphic Cumulative Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
-The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
-Polymorphic Cumulative Record packType := {pk : Type}.
+Set Polymorphic Inductive Cumulativity.
+Inductive Unit := unit.
 \end{coq_example*}
 \begin{coq_example}
-Print packType.
+Print Unit.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
 
+\subsection*{An example of a proof using cumulativity}
+
+\begin{coq_example}
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
+  Proof.
+    exact H.
+  Defined.
+\end{coq_example}
 
 \asection{Global and local universes}
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 6ef9532ad..2adf522b7 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -305,6 +305,14 @@ type inline =
 type module_ast_inl = module_ast * inline
 type module_binder = bool option * lident list * module_ast_inl
 
+(** Cumulativity can be set globally, locally or unset locally and it
+   can not enabled at all. *)
+type cumulative_inductive_parsing_flag =
+  | GlobalCumulativity
+  | GlobalNonCumulativity
+  | LocalCumulativity
+  | LocalNonCumulativity
+
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
@@ -336,7 +344,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/lib/flags.ml b/lib/flags.ml
index 0bce22f58..027ba16f0 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -167,9 +167,9 @@ let use_polymorphic_flag () =
 let make_polymorphic_flag b =
   local_polymorphic_flag := Some b
 
-let inductive_cumulativity = ref false
-let make_inductive_cumulativity b = inductive_cumulativity := b
-let is_inductive_cumulativity () = !inductive_cumulativity
+let polymorphic_inductive_cumulativity = ref false
+let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
+let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
 
 (** [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
diff --git a/lib/flags.mli b/lib/flags.mli
index eb4c37a54..5af563b46 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,9 +119,9 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
-(** Global inductive cumulativity flag. *)
-val make_inductive_cumulativity : bool -> unit
-val is_inductive_cumulativity : unit -> bool
+(** Global polymorphic inductive cumulativity flag. *)
+val make_polymorphic_inductive_cumulativity : bool -> unit
+val is_polymorphic_inductive_cumulativity : unit -> bool
 
 val warn : bool ref
 val make_warn : bool -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d29fca77..93a778274 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -168,8 +168,13 @@ GEXTEND Gram
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
 	  let cum =
 	    match cum with
-	      Some b -> b
-	    | None -> Flags.is_inductive_cumulativity ()
+	      Some true -> LocalCumulativity
+            | Some false -> LocalNonCumulativity
+	    | None ->
+                if Flags.is_polymorphic_inductive_cumulativity () then
+                  GlobalCumulativity
+                else
+                  GlobalNonCumulativity
 	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8555a0b22..8cf5e8442 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1492,7 +1492,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1507,7 +1507,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a68b569cb..4c50c2f36 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -760,7 +760,11 @@ open Decl_kinds
                        | Class _ -> "Class" | Variant -> "Variant"
           in
           if p then
-            let cm = if cum then "Cumulative" else "NonCumulative" in
+            let cm =
+              match cum with
+              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
+              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+            in
             cm ^ " " ^ kind
           else kind
         in
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index a978f6b90..7906a5b15 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ebf817cfc..0ee85712e 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -1,5 +1,11 @@
+Polymorphic Cumulative Inductive T1 := t1 : T1.
+Fail Monomorphic Cumulative Inductive T2 := t2 : T2.
+
+Polymorphic Cumulative Record R1 := { r1 : T1 }.
+Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
+
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
@@ -62,4 +68,33 @@ End subtyping_test.
 
 Record A : Type := { a :> Type; }.
 
-Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
+Record B (X : A) : Type := { b : X; }.
+
+NonCumulative Inductive NCList (A: Type)
+  := ncnil | nccons : A -> NCList A -> NCList A.
+
+Section NCListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
+
+End NCListLift.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    : @funext_type@{a b e} A B -> @funext_type@{a b e'} A B.
+  Proof.
+    intros H f g Hfg. exact (H f g Hfg).
+  Defined.
+End down.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index adf24d23b..4f63ed6f4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,7 +522,21 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
+let should_treat_as_cumulative cum poly =
+  if poly then
+    match cum with
+    | GlobalCumulativity | LocalCumulativity -> true
+    | GlobalNonCumulativity | LocalNonCumulativity -> false
+  else
+    match cum with
+    | GlobalCumulativity | GlobalNonCumulativity -> false
+    | LocalCumulativity -> 
+      user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+    | LocalNonCumulativity ->
+      user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
+  let is_cumulative = should_treat_as_cumulative cum poly in
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -533,13 +547,14 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive cum poly lo finite indl =
+  let is_cumulative = should_treat_as_cumulative cum poly in
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -576,7 +591,7 @@ let vernac_inductive cum poly lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl cum poly lo finite
+    do_mutual_inductive indl is_cumulative poly lo finite
 
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
@@ -1363,10 +1378,10 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "inductive cumulativity";
-      optkey   = ["Inductive"; "Cumulativity"];
-      optread  = Flags.is_inductive_cumulativity;
-      optwrite = Flags.make_inductive_cumulativity }
+      optname  = "Polymorphic inductive cumulativity";
+      optkey   = ["Polymorphic"; "Inductive"; "Cumulativity"];
+      optread  = Flags.is_polymorphic_inductive_cumulativity;
+      optwrite = Flags.make_polymorphic_inductive_cumulativity }
 
 let _ =
   declare_int_option