Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 19 insertions, 7 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 481ffc290c..c45fe1cf00 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -33,6 +33,7 @@ type 'constr pguard_error =
   | RecCallInCasePred of 'constr
   | NotGuardedForm of 'constr
   | ReturnPredicateNotCoInductive of 'constr
+  | FixpointOnIrrelevantInductive
 
 type guard_error = constr pguard_error
 
@@ -47,8 +48,8 @@ type ('constr, 'types) ptype_error =
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
-  | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
-      * (Sorts.family * Sorts.family * arity_error) option
+  | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
+      * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -59,11 +60,13 @@ type ('constr, 'types) ptype_error =
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
-  | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
+  | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
-      int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
+      int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.Constraint.t
   | UndeclaredUniverse of Univ.Level.t
+  | DisallowedSProp
+  | BadRelevance
 
 type type_error = (constr, types) ptype_error
 
@@ -102,8 +105,8 @@ let error_assumption env j =
 let error_reference_variables env id c =
   raise (TypeError (env, ReferenceVariables (id,c)))
 
-let error_elim_arity env ind aritylst c pj okinds =
-  raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds)))
+let error_elim_arity env ind c pj okinds =
+  raise (TypeError (env, ElimArity (ind,c,pj,okinds)))
 
 let error_case_not_inductive env j =
   raise (TypeError (env, CaseNotInductive j))
@@ -149,6 +152,12 @@ let error_unsatisfied_constraints env c =
 let error_undeclared_universe env l =
   raise (TypeError (env, UndeclaredUniverse l))
 
+let error_disallowed_sprop env =
+  raise (TypeError (env, DisallowedSProp))
+
+let error_bad_relevance env =
+  raise (TypeError (env, BadRelevance))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -165,6 +174,7 @@ let map_pguard_error f = function
 | RecCallInCasePred c -> RecCallInCasePred (f c)
 | NotGuardedForm c -> NotGuardedForm (f c)
 | ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
+| FixpointOnIrrelevantInductive -> FixpointOnIrrelevantInductive
 
 let map_ptype_error f = function
 | UnboundRel n -> UnboundRel n
@@ -172,7 +182,7 @@ let map_ptype_error f = function
 | NotAType j -> NotAType (on_judgment f j)
 | BadAssumption j -> BadAssumption (on_judgment f j)
 | ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
-| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar)
+| ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar)
 | CaseNotInductive j -> CaseNotInductive (on_judgment f j)
 | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
 | NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
@@ -189,3 +199,5 @@ let map_ptype_error f = function
   IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
 | UnsatisfiedConstraints g -> UnsatisfiedConstraints g
 | UndeclaredUniverse l -> UndeclaredUniverse l
+| DisallowedSProp -> DisallowedSProp
+| BadRelevance -> BadRelevance