Module `Type_errors`Source

Type errors. \label{typeerrors}

Sourcetype 'constr pfix_guard_error =

| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * Environ.env * 'constr * (int list * int list) Lazy.t
| NotEnoughArgumentsForFixCall of int
| FixpointOnIrrelevantInductive

Sourcetype '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

Sourcetype 'constr pguard_error =

| FixGuardError of 'constr pfix_guard_error
| CoFixGuardError of 'constr pcofix_guard_error

Sourcetype fix_guard_error = Constr.constr pfix_guard_error

Sourcetype cofix_guard_error = Constr.constr pcofix_guard_error

Sourcetype guard_error = Constr.constr pguard_error

Source

type ('constr, 'types) pcant_apply_bad_type =
  (int * 'constr * 'constr)
  * ('constr, 'types) Environ.punsafe_judgment
  * ('constr, 'types) Environ.punsafe_judgment array

Sourcetype ('constr, 'types, 'r) 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 * Sorts.t option
| CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
| CaseOnPrivateInd of Names.inductive
| WrongCaseInfo of Constr.pinductive * Constr.case_info
| NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
| IllFormedCaseParams
| 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 ('constr, 'types) pcant_apply_bad_type
| CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * (Names.Name.t, 'r) Context.pbinder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
| IllTypedRecBody of int * (Names.Name.t, 'r) Context.pbinder_annot array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
| UnsatisfiedQConstraints of Sorts.QConstraints.t
| UnsatisfiedConstraints of Univ.Constraints.t
| UndeclaredQualities of Sorts.QVar.Set.t
| UndeclaredUniverses of Univ.Level.Set.t
| DisallowedSProp
| BadBinderRelevance of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
| BadCaseRelevance of 'r * 'constr
| BadInvert
| BadVariance of {
1. lev : Univ.Level.t;
2. expected : UVars.Variance.t;
3. actual : UVars.Variance.t;
}
| UndeclaredUsedVariables of {
1. declared_vars : Names.Id.Set.t;
2. inferred_vars : Names.Id.Set.t;
}

Sourcetype type_error = (Constr.constr, Constr.types, Sorts.relevance) ptype_error

Sourceexception TypeError of Environ.env * type_error

Sourcetype inductive_error =

| NonPos of Constr.constr * Constr.constr
| NotEnoughArgs of Constr.constr * Constr.constr
| NotConstructor of Names.Id.t * Constr.constr * Constr.constr * int * int
| NonPar of 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 Constr.constr
| BadEntry
| LargeNonPropInductiveNotInType
| MissingConstraints of Sorts.t list * Sorts.t

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

Sourceexception InductiveError of Environ.env * inductive_error

Raising functions

Sourceval error_unbound_rel : Environ.env -> int -> 'a

Sourceval error_unbound_var : Environ.env -> Names.variable -> 'a

Sourceval error_not_type : Environ.env -> Environ.unsafe_judgment -> 'a

Sourceval error_assumption : Environ.env -> Environ.unsafe_judgment -> 'a

Source

val error_reference_variables : 
  Environ.env ->
  Names.Id.t ->
  Names.GlobRef.t ->
  'a

Source

val error_elim_arity : 
  Environ.env ->
  Constr.pinductive ->
  Constr.constr ->
  Sorts.t option ->
  'a

Sourceval error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a

Sourceval error_case_on_private_ind : Environ.env -> Names.inductive -> 'a

Sourceval error_number_branches : Environ.env -> Environ.unsafe_judgment -> int -> 'a

Source

val error_ill_formed_branch : 
  Environ.env ->
  Constr.constr ->
  Constr.pconstructor ->
  Constr.constr ->
  Constr.constr ->
  'a

Source

val error_generalization : 
  Environ.env ->
  (Names.Name.t * Constr.types) ->
  Environ.unsafe_judgment ->
  'a

Source

val error_actual_type : 
  Environ.env ->
  Environ.unsafe_judgment ->
  Constr.types ->
  'a

Source

val error_incorrect_primitive : 
  Environ.env ->
  (CPrimitives.op_or_type, Constr.types) Environ.punsafe_judgment ->
  Constr.types ->
  'a

Source

val error_cant_apply_not_functional : 
  Environ.env ->
  Environ.unsafe_judgment ->
  Environ.unsafe_judgment array ->
  'a

Source

val error_cant_apply_bad_type : 
  Environ.env ->
  (int * Constr.constr * Constr.constr) ->
  Environ.unsafe_judgment ->
  Environ.unsafe_judgment array ->
  'a

Source

val error_ill_formed_rec_body : 
  Environ.env ->
  guard_error ->
  Names.Name.t Constr.binder_annot array ->
  int ->
  Environ.env ->
  Environ.unsafe_judgment array ->
  'a

Source

val error_ill_typed_rec_body : 
  Environ.env ->
  int ->
  Names.Name.t Constr.binder_annot array ->
  Environ.unsafe_judgment array ->
  Constr.types array ->
  'a

Sourceval error_unsatisfied_qconstraints : Environ.env -> Sorts.QConstraints.t -> 'a

Sourceval error_unsatisfied_constraints : Environ.env -> Univ.Constraints.t -> 'a

Sourceval error_undeclared_qualities : Environ.env -> Sorts.QVar.Set.t -> 'a

Sourceval error_undeclared_universes : Environ.env -> Univ.Level.Set.t -> 'a

Sourceval error_disallowed_sprop : Environ.env -> 'a

Source

val error_bad_binder_relevance : 
  Environ.env ->
  Sorts.relevance ->
  Constr.rel_declaration ->
  'a

Source

val error_bad_case_relevance : 
  Environ.env ->
  Sorts.relevance ->
  Constr.case ->
  'a

Sourceval error_bad_invert : Environ.env -> 'a

Source

val error_bad_variance : 
  Environ.env ->
  lev:Univ.Level.t ->
  expected:UVars.Variance.t ->
  actual:UVars.Variance.t ->
  'a

Source

val error_undeclared_used_variables : 
  Environ.env ->
  declared_vars:Names.Id.Set.t ->
  inferred_vars:Names.Id.Set.t ->
  'a

Sourceval map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error

Source

val map_ptype_error : 
  ('r1 -> 'r2) ->
  ('c -> 'd) ->
  ('c, 'c, 'r1) ptype_error ->
  ('d, 'd, 'r2) ptype_error

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Type_errors/index.html

Module `Type_errors`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Type_errors/index.html

Module Type_errorsSource

Module `Type_errors`Source