Fix two BadVarianceQ anomalies in inductive cumulativity

checker/coqchk_main.ml

@@ -317,6 +317,7 @@ let explain_exn = function
       | UndeclaredQualities _ -> str"UndeclaredQualities"
       | UndeclaredUniverses _ -> str"UndeclaredUniverse"
       | BadVariance _ -> str "BadVariance"
+      | BadQVariance _ -> str "BadQVariance"
       | UndeclaredUsedVariables _ -> str "UndeclaredUsedVariables"
       | IllFormedConstant _ -> str "IllFormedConstant"
       | IllFormedInductive _ -> str "IllFormedInductive"

kernel/inferCumulativity.ml

@@ -281,7 +281,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
         let variances = infer_constant (info_env (fst infos)) variances con in
         let variances = infer_stack infos variances stk in
         set_infer_mode infer_mode variances
-      with BadVariance _ | NotInferring as e ->
+      with BadVariance _ | BadVarianceQ _ | NotInferring as e ->
       match def with
       | None -> raise e
       | Some (hd,stk) -> infer_fterm cv_pb infos variances hd stk
@@ -409,3 +409,5 @@ let infer_inductive ~env_params ~env_ar_par ~arities ~ctors quals univs =
     Array.make (Array.length quals) Invariant, Array.make (Array.length univs) Invariant
   | BadVariance (lev, expected, actual) ->
     Type_errors.error_bad_variance env_params ~lev ~expected ~actual
+  | BadVarianceQ (qvar, expected, actual) ->
+    Type_errors.error_bad_qvariance env_params ~qvar ~expected ~actual

kernel/type_errors.ml

@@ -80,6 +80,7 @@ type ('constr, 'types, 'r) ptype_error =
   | BadCaseRelevance of 'r * 'constr
   | BadInvert
   | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
+  | BadQVariance of { qvar : Sorts.QVar.t; expected : Variance.t; actual : Variance.t }
   | UndeclaredUsedVariables of { declared_vars : Id.Set.t; inferred_vars : Id.Set.t }
   | IllFormedConstant of Constant.t * KerName.t
   | IllFormedInductive of MutInd.t * KerName.t
@@ -184,6 +185,9 @@ let error_bad_invert env =
 let error_bad_variance env ~lev ~expected ~actual =
   raise (TypeError (env, BadVariance {lev;expected;actual}))
 
+let error_bad_qvariance env ~qvar ~expected ~actual =
+  raise (TypeError (env, BadQVariance {qvar;expected;actual}))
+
 let error_undeclared_used_variables env ~declared_vars ~inferred_vars =
   raise (TypeError (env, UndeclaredUsedVariables {declared_vars; inferred_vars}))
 
@@ -221,7 +225,7 @@ let map_ptype_error fr f = function
 | UndeclaredQualities _ | UndeclaredUniverses _ | NotAllowedSProp
 | UnsatisfiedUnivConstraints _
 | UnsatisfiedPConstraints _
-| ReferenceVariables _ | BadInvert | BadVariance _ | UndeclaredUsedVariables _ | IllFormedConstant _ | IllFormedInductive _ as e -> e
+| ReferenceVariables _ | BadInvert | BadVariance _ | BadQVariance _ | UndeclaredUsedVariables _ | IllFormedConstant _ | IllFormedInductive _ as e -> e
 | NotAType j -> NotAType (on_judgment f j)
 | BadAssumption j -> BadAssumption (on_judgment f j)
 | ElimArity (pi, c, ar) -> ElimArity (pi, f c, ar)

kernel/type_errors.mli

@@ -82,6 +82,7 @@ type ('constr, 'types, 'r) ptype_error =
   | BadCaseRelevance of 'r * 'constr
   | BadInvert
   | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
+  | BadQVariance of { qvar : Sorts.QVar.t; expected : Variance.t; actual : Variance.t }
   | UndeclaredUsedVariables of { declared_vars : Id.Set.t; inferred_vars : Id.Set.t }
   | IllFormedConstant of Constant.t * KerName.t
   | IllFormedInductive of MutInd.t * KerName.t
@@ -170,6 +171,8 @@ val error_bad_invert : env -> 'a
 
 val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
 
+val error_bad_qvariance : env -> qvar:Sorts.QVar.t -> expected:Variance.t -> actual:Variance.t -> 'a
+
 val error_undeclared_used_variables : env -> declared_vars:Id.Set.t -> inferred_vars:Id.Set.t -> 'a
 
 val error_ill_formed_constant : env -> Constant.t -> KerName.t -> 'a

test-suite/success/CumulInd.v

@@ -63,6 +63,14 @@ Inductive E@{s;} : Prop := .
 Fail Check fun x:E@{SProp;} => x:E@{Prop;}.
 Check fun x:E@{Prop;} => x:E@{Type;}.
 
+(* quality variance is checked like universe variance: analogues of
+   not_irrelevant, check_covariant and must_unfold above *)
+Fail Inductive not_irrelevant_qual@{*s;u} : Prop := nirrq (_ : Type@{s;u}).
+Inductive check_covariant_qual@{+s;u} : Prop := covq (_ : Type@{s;u}).
+
+Definition idT@{s;u} (A:Type@{s;u}) : Type@{s;u} := A.
+Inductive must_unfold_qual@{*s;u} (A:Type@{s;u}) : Prop := cmustq (_ : idT A).
+
 Module Type Covariant.
   Inductive foo@{+s;+u} : Set := .
 End Covariant.

vernac/himsg.ml

@@ -970,6 +970,12 @@ let explain_bad_variance env sigma ~lev ~expected ~actual =
     (fun () -> UVars.Variance.pr expected)
     (fun () -> UVars.Variance.pr actual)
 
+let explain_bad_qvariance env sigma ~qvar ~expected ~actual =
+  fmt "Incorrect variance for sort quality %t:@ expected %t@ but cannot be less restrictive than %t."
+    (fun () -> Termops.pr_evd_qvar sigma qvar)
+    (fun () -> UVars.Variance.pr expected)
+    (fun () -> UVars.Variance.pr actual)
+
 let explain_undeclared_used_variables env sigma ~declared_vars ~inferred_vars =
   let l = Id.Set.elements (Id.Set.diff inferred_vars declared_vars) in
   let n = List.length l in
@@ -1050,6 +1056,7 @@ let explain_type_error env sigma err =
   | BadCaseRelevance (rlv, case) -> explain_bad_case_relevance env sigma rlv case
   | BadInvert -> explain_bad_invert env
   | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual
+  | BadQVariance {qvar;expected;actual} -> explain_bad_qvariance env sigma ~qvar ~expected ~actual
   | UndeclaredUsedVariables {declared_vars;inferred_vars} ->
       explain_undeclared_used_variables env sigma ~declared_vars ~inferred_vars
   | IllFormedConstant (cst, kn) ->