Module Type_errors

Type errors. \label{typeerrors}

type 'constr pfix_guard_error =
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * Environ.env * 'constr * (int list * int list) Stdlib.Lazy.t
| NotEnoughArgumentsForFixCall of int
| FixpointOnIrrelevantInductive
type 'constr pcofix_guard_error =
| CodomainNotInductiveType of 'constr
| NestedRecursiveOccurrences
| UnguardedRecursiveCall of 'constr
| RecCallInTypeOfAbstraction of 'constr
| RecCallInNonRecArgOfConstructor of 'constr
| RecCallInTypeOfDef of 'constr
| RecCallInCaseFun of 'constr
| RecCallInCaseArg of 'constr
| RecCallInCasePred of 'constr
| NotGuardedForm of 'constr
| ReturnPredicateNotCoInductive of 'constr
type 'constr pguard_error =
| FixGuardError of 'constr pfix_guard_error
| CoFixGuardError of 'constr pcofix_guard_error
type fix_guard_error = Constr.constr pfix_guard_error
type cofix_guard_error = Constr.constr pcofix_guard_error
type guard_error = Constr.constr pguard_error
type ('constr, 'types) ptype_error =
| UnboundRel of int
| UnboundVar of Names.variable
| NotAType of ('constr, 'types) Environ.punsafe_judgment
| BadAssumption of ('constr, 'types) Environ.punsafe_judgment
| ReferenceVariables of Names.Id.t * Names.GlobRef.t
| ElimArity of Constr.pinductive * 'constr * (('constr, 'types) Environ.punsafe_judgment * Sorts.family * Sorts.family * Sorts.family) option
| CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
| WrongCaseInfo of Constr.pinductive * Constr.case_info
| NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
| IllFormedBranch of 'constr * Constr.pconstructor * 'constr * 'constr
| Generalization of Names.Name.t * 'types * ('constr, 'types) Environ.punsafe_judgment
| ActualType of ('constr, 'types) Environ.punsafe_judgment * 'types
| IncorrectPrimitive of (CPrimitives.op_or_type, 'types) Environ.punsafe_judgment * 'types
| CantApplyBadType of int * 'constr * 'constr * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * Names.Name.t Context.binder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
| IllTypedRecBody of int * Names.Name.t Context.binder_annot array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.Constraints.t
| UndeclaredUniverse of Univ.Level.t
| DisallowedSProp
| BadRelevance
| BadInvert
| BadVariance of {
lev : Univ.Level.t;
expected : Univ.Variance.t;
actual : Univ.Variance.t;
}
type type_error = (Constr.constr, Constr.types) ptype_error
exception TypeError of Environ.env * type_error
type inductive_error =
| NonPos of Environ.env * Constr.constr * Constr.constr
| NotEnoughArgs of Environ.env * Constr.constr * Constr.constr
| NotConstructor of Environ.env * Names.Id.t * Constr.constr * Constr.constr * int * int
| NonPar of Environ.env * Constr.constr * int * Constr.constr * Constr.constr
| SameNamesTypes of Names.Id.t
| SameNamesConstructors of Names.Id.t
| SameNamesOverlap of Names.Id.t list
| NotAnArity of Environ.env * Constr.constr
| BadEntry
| LargeNonPropInductiveNotInType
| MissingConstraints of Sorts.t list * Sorts.t

The different kinds of errors that may result of a malformed inductive definition.

exception InductiveError of inductive_error

Raising functions

val error_unbound_rel : Environ.env -> int -> 'a
val error_unbound_var : Environ.env -> Names.variable -> 'a
val error_not_type : Environ.env -> Environ.unsafe_judgment -> 'a
val error_assumption : Environ.env -> Environ.unsafe_judgment -> 'a
val error_reference_variables : Environ.env -> Names.Id.t -> Names.GlobRef.t -> 'a
val error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a
val error_number_branches : Environ.env -> Environ.unsafe_judgment -> int -> 'a
val error_ill_formed_branch : Environ.env -> Constr.constr -> Constr.pconstructor -> Constr.constr -> Constr.constr -> 'a
val error_generalization : Environ.env -> (Names.Name.t * Constr.types) -> Environ.unsafe_judgment -> 'a
val error_actual_type : Environ.env -> Environ.unsafe_judgment -> Constr.types -> 'a
val error_cant_apply_not_functional : Environ.env -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_cant_apply_bad_type : Environ.env -> (int * Constr.constr * Constr.constr) -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_ill_formed_rec_body : Environ.env -> guard_error -> Names.Name.t Context.binder_annot array -> int -> Environ.env -> Environ.unsafe_judgment array -> 'a
val error_ill_typed_rec_body : Environ.env -> int -> Names.Name.t Context.binder_annot array -> Environ.unsafe_judgment array -> Constr.types array -> 'a
val error_unsatisfied_constraints : Environ.env -> Univ.Constraints.t -> 'a
val error_undeclared_universe : Environ.env -> Univ.Level.t -> 'a
val error_disallowed_sprop : Environ.env -> 'a
val error_bad_relevance : Environ.env -> 'a
val error_bad_invert : Environ.env -> 'a
val error_bad_variance : Environ.env -> lev:Univ.Level.t -> expected:Univ.Variance.t -> actual:Univ.Variance.t -> 'a
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error