Pretype_errors (rocq-runtime.Pretype

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 option * 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

type type_error =
  (EConstr.constr, EConstr.types, EConstr.ERelevance.t) Type_errors.ptype_error

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
*)
| NotAllowedSProp
| NotAllowedElimination of bool * EConstr.ESorts.t * Names.inductive EConstr.puniverses
| NotAllowedDependentElimination of bool * Names.inductive

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 : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  (EConstr.constr * EConstr.constr) ->
  'b

Implicit arguments synthesis errors

val error_occur_check : 
  ?loc:Loc.t ->
  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 : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  (EConstr.constr * EConstr.constr * EConstr.constr) ->
  'b

val error_cannot_find_well_typed_abstraction : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr list ->
  (Environ.env * pretype_error) option ->
  'b

val error_wrong_abstraction_type : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  EConstr.constr ->
  EConstr.types ->
  EConstr.types ->
  'b

val error_abstraction_over_meta : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  Names.Name.t ->
  'b

val error_non_linear_unification : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  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_not_allowed_sprop : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> 'a

val error_not_allowed_elimination : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  bool ->
  EConstr.ESorts.t ->
  Names.inductive EConstr.puniverses ->
  'a

val error_not_allowed_dependent_elimination : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  bool ->
  Names.inductive ->
  'a

Typeclass errors

val unsatisfiable_constraints : 
  Environ.env ->
  Evd.evar_map ->
  Evar.t option ->
  Evar.Set.t ->
  'a

val unsatisfiable_exception : exn -> bool