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
| InstanceNotFunctionalType of Evar.t * Environ.env * EConstr.constr * EConstr.types
| UnifUnivInconsistency of UGraph.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
val of_type_error : Type_errors.type_error -> type_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 * unification_error
| NotProduct of EConstr.constr
| TypingError of type_error
| CantApplyBadTypeExplained of (EConstr.constr, EConstr.types) Type_errors.pcant_apply_bad_type * unification_error
| CannotUnifyOccurrences of subterm_unification_error
| UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t(*

unresolvable evar, connex component

*)
| DisallowedSProp
exception PretypeError of Environ.env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
val raise_type_error : ?loc:Loc.t -> (Environ.env * Evd.evar_map * type_error) -> 'a

Raising errors

val error_actual_type : ?loc:Loc.t -> ?info:Exninfo.info -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b
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 -> ?error:unification_error -> (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 EConstr.binder_annot array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
val error_elim_arity : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.inductive EConstr.puniverses -> EConstr.constr -> EConstr.ESorts.t 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 -> unification_error -> '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 -> 'a
val unsatisfiable_exception : exn -> bool