Module Pretype_errors

The type of errors raised by the pretyper
type unification_error =
| OccurCheck of Evar.t * EConstr.constr
| NotClean of EConstr.existential * Environ.env * EConstr.constr
| NotSameArgSize
| NotSameHead
| NoCanonicalStructure
| ConversionFailed of Environ.env * EConstr.constr * EConstr.constr
| IncompatibleInstances of Environ.env * EConstr.existential * EConstr.constr * EConstr.constr
| MetaOccurInBody of Evar.t
| InstanceNotSameType of Evar.t * Environ.env * EConstr.types * EConstr.types
| UnifUnivInconsistency of Univ.univ_inconsistency
| CannotSolveConstraint of Evd.evar_constraint * unification_error
| ProblemBeyondCapabilities
type position = (Names.Id.t * Locus.hyp_location_flag) option
type position_reporting = (position * int) * EConstr.constr
type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
type type_error = (EConstr.constr, EConstr.types) Type_errors.ptype_error
type pretype_error =
| CantFindCaseType of EConstr.constr

Old Case

| ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error

Type inference unification

| UnifOccurCheck of Evar.t * EConstr.constr

Tactic Unification

| UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
| CannotUnify of EConstr.constr * EConstr.constr * unification_error option
| CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
| CannotUnifyBindingType of EConstr.constr * EConstr.constr
| CannotGeneralize of EConstr.constr
| NoOccurrenceFound of EConstr.constr * Names.Id.t option
| CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * pretype_error) option
| WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types
| AbstractionOverMeta of Names.Name.t * Names.Name.t
| NonLinearUnification of Names.Name.t * EConstr.constr

Pretyping

| VarNotFound of Names.Id.t
| EvarNotFound of Names.Id.t
| UnexpectedType of EConstr.constr * EConstr.constr
| NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
| UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option

unresolvable evar, connex component

| DisallowedSProp
exception PretypeError of Environ.env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
val error_actual_type : ?⁠loc:Loc.t -> ?⁠info:Exninfo.info -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b

Raising errors

val error_actual_type_core : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b
val error_cant_apply_not_functional : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
val error_cant_apply_bad_type : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> (int * EConstr.constr * EConstr.constr) -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
val error_case_not_inductive : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
val error_ill_formed_branch : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constr.pconstructor -> EConstr.constr -> EConstr.constr -> 'b
val error_number_branches : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> int -> 'b
val error_ill_typed_rec_body : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> int -> Names.Name.t Context.binder_annot array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
val error_elim_arity : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> Constr.pinductive -> EConstr.constr -> EConstr.unsafe_judgment -> (Sorts.family * Sorts.family * Sorts.family * Type_errors.arity_error) option -> 'b
val error_not_a_type : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
val error_assumption : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
val error_cannot_coerce : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr) -> 'b
Implicit arguments synthesis errors
val error_occur_check : Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> 'b
val error_unsolvable_implicit : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> Evar.t -> Evd.unsolvability_explanation option -> 'b
val error_cannot_unify : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> ?⁠reason:unification_error -> (EConstr.constr * EConstr.constr) -> 'b
val error_cannot_unify_local : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr * EConstr.constr) -> 'b
val error_cannot_find_well_typed_abstraction : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> (Environ.env * pretype_error) option -> 'b
val error_wrong_abstraction_type : Environ.env -> Evd.evar_map -> Names.Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b
val error_abstraction_over_meta : Environ.env -> Evd.evar_map -> Constr.metavariable -> Constr.metavariable -> 'b
val error_non_linear_unification : Environ.env -> Evd.evar_map -> Constr.metavariable -> EConstr.constr -> 'b
Ml Case errors
val error_cant_find_case_type : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'b
Pretyping errors
val error_unexpected_type : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b
val error_not_product : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'b
val error_var_not_found : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> 'b
val error_evar_not_found : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> 'b
val error_disallowed_sprop : Environ.env -> Evd.evar_map -> 'a
Typeclass errors
val unsatisfiable_constraints : Environ.env -> Evd.evar_map -> Evar.t option -> Evar.Set.t option -> 'a
val unsatisfiable_exception : exn -> bool