Merge PR coq#9032: checker: check inductive types by roundtrip throug…

…h the kernel.

checker/checkInductive.mli

@@ -8,10 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*i*)
 open Names
 open Environ
-(*i*)
+
+exception InductiveMismatch of MutInd.t * string
+(** Some field of the inductive is different from what the kernel infers. *)
 
 (*s The following function does checks on inductive declarations. *)
 

checker/checker.ml

@@ -302,6 +302,10 @@ let explain_exn = function
 (*      let ctx = Check.get_env() in
       hov 0
         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
+
+  | CheckInductive.InductiveMismatch (mind,field) ->
+    hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.")
+
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s = "" then mt ()

kernel/univ.ml

@@ -1034,6 +1034,8 @@ module ACumulativityInfo =
 struct
   type t = AUContext.t * Variance.t array
 
+  let repr (auctx,var) = AUContext.repr auctx, var
+
   let pr prl (univs, variance) =
     AUContext.pr prl ~variance univs
 

kernel/univ.mli

@@ -400,6 +400,7 @@ module ACumulativityInfo :
 sig
   type t
 
+  val repr : t -> CumulativityInfo.t
   val univ_context : t -> AUContext.t
   val variance : t -> Variance.t array
   val leq_constraints : t -> Instance.t constraint_function

test-suite/coqchk/inductive_functor_params.v

@@ -0,0 +1,16 @@
+
+Module Type T.
+  Parameter foo : nat -> nat.
+End T.
+
+Module F (A:T).
+  Inductive ind (n:nat) : nat -> Prop :=
+  | C : (forall x, x < n -> ind (A.foo n) x) -> ind n n.
+End F.
+
+Module A. Definition foo (n:nat) := n. End A.
+
+Module M := F A.
+(* Note: M.ind could be seen as having 1 recursively uniform
+   parameter, but module substitution does not recognize it, so it is
+   treated as a non-uniform parameter. *)

test-suite/coqchk/inductive_functor_template.v

@@ -0,0 +1,11 @@
+
+Module Type E. Parameter T : Type. End E.
+
+Module F (X:E).
+  #[universes(template)] Inductive foo := box : X.T -> foo.
+End F.
+
+Module ME. Definition T := nat. End ME.
+Module A := F ME.
+(* Note: A.foo could live in Set, and coqchk sees that (because of
+   template polymorphism implementation details) *)