From 4a676036eef1d500f52544f40e27d3a1f1398ab4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 12 Aug 2026 21:00:53 +0000 Subject: [PATCH 1/2] Report a bad sort quality variance as an error, not an anomaly MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. Inductive t@{*s;u} : Prop := c (_ : Type@{s;u}). Anomaly "Uncaught exception InferCumulativity.BadVarianceQ(_, 0, 1)." infer_inductive converted BadVariance to a type error but left BadVarianceQ, its sort quality counterpart, uncaught. The universe analogue (t@{s;*u}) already reported "Incorrect variance for universe". Add BadQVariance to ptype_error and print it the same way: Incorrect variance for sort quality α1: expected * but cannot be less restrictive than +. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- checker/coqchk_main.ml | 1 + kernel/inferCumulativity.ml | 2 ++ kernel/type_errors.ml | 6 +++++- kernel/type_errors.mli | 3 +++ test-suite/success/CumulInd.v | 5 +++++ vernac/himsg.ml | 7 +++++++ 6 files changed, 23 insertions(+), 1 deletion(-) diff --git a/checker/coqchk_main.ml b/checker/coqchk_main.ml index 8ec2cf428ad2..01acdec9cb42 100644 --- a/checker/coqchk_main.ml +++ b/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" diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index ad6ab746d39b..43a5517428a4 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -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 diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 769882d5535d..2c9a8012f4bf 100644 --- a/kernel/type_errors.ml +++ b/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) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index c3698be298ab..b3745b81e94f 100644 --- a/kernel/type_errors.mli +++ b/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 diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v index 5f8f39be2db8..80e275e2af1e 100644 --- a/test-suite/success/CumulInd.v +++ b/test-suite/success/CumulInd.v @@ -63,6 +63,11 @@ 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 and check_covariant above *) +Fail Inductive not_irrelevant_qual@{*s;u} : Prop := nirrq (_ : Type@{s;u}). +Inductive check_covariant_qual@{+s;u} : Prop := covq (_ : Type@{s;u}). + Module Type Covariant. Inductive foo@{+s;+u} : Set := . End Covariant. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6878e4afbc6d..57d658613b70 100644 --- a/vernac/himsg.ml +++ b/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) -> From 627d8c7069c9cf4d1131c2b1926504fca958a07c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 12 Aug 2026 21:03:52 +0000 Subject: [PATCH 2/2] Allow delta unfolding when checking sort quality variance Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. Definition idT@{s;u} (A:Type@{s;u}) : Type@{s;u} := A. Inductive t@{*s;u} (A:Type@{s;u}) : Prop := c (_ : idT A). Anomaly "Uncaught exception InferCumulativity.BadVarianceQ(_, 0, 2)." The declaration is valid: unfolding idT satisfies the annotation. The FFlex handler in infer_cumul_stack retries after unfolding when the constant's variance check fails, but it only caught BadVariance, so the quality counterpart escaped. In Infer mode the same position raises NotInferring, which was caught, hence the anomaly only shows in Check mode -- reached either by an explicit variance annotation, or by rocqchk, which sets every recorded variance to Some v (checker/checkInductive.ml:99). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- kernel/inferCumulativity.ml | 2 +- test-suite/success/CumulInd.v | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 43a5517428a4..f75ae688935c 100644 --- a/kernel/inferCumulativity.ml +++ b/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 diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v index 80e275e2af1e..964439daac4a 100644 --- a/test-suite/success/CumulInd.v +++ b/test-suite/success/CumulInd.v @@ -64,10 +64,13 @@ 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 and check_covariant above *) + 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.