aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml59
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/evarsolve.ml23
-rw-r--r--pretyping/evarsolve.mli12
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/unification.mli2
6 files changed, 74 insertions, 44 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5de0745d17..a793e217d4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1784,25 +1784,24 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
!evdref, ans
let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
- let sigma, t, tt = match t with
+ let s = mkSort s in
+ match t with
| None ->
(* This is the situation we are building a return predicate and
we are in an impossible branch *)
let n = Context.Rel.length (rel_context !!env) in
let n' = Context.Rel.length (rel_context !!tycon_env) in
- let sigma, (impossible_case_type, u) =
- Evarutil.new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)
- sigma univ_flexible_alg
- in
- (sigma, lift (n'-n) impossible_case_type, mkSort u)
+ let src = Loc.tag ?loc Evar_kinds.ImpossibleCase in
+ let sigma, impossible_case_type =
+ Evarutil.new_evar (reset_context !!env) sigma ~src ~typeclass_candidate:false s in
+ (sigma, { uj_val = lift (n'-n) impossible_case_type; uj_type = s })
| Some t ->
let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in
let sigma, tt = Typing.type_of !!extenv sigma t in
- (sigma, t, tt) in
- match unify_leq_delay !!env sigma tt (mkSort s) with
- | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
- | sigma ->
- sigma, { uj_val = t; uj_type = tt }
+ match unify_leq_delay !!env sigma tt s with
+ | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
+ | sigma -> (sigma, { uj_val = t; uj_type = tt })
+
(* For a multiple pattern-matching problem Xi on t1..tn with return
* type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
@@ -1915,9 +1914,24 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
- let s' = Retyping.get_sort_of !!env sigma t in
- let sigma, s = Evd.new_sort_variable univ_flexible sigma in
- let sigma = Evd.set_leq_sort !!env sigma s' s in
+ let s = Retyping.get_sort_of !!env sigma t in
+ let sigma, s = Sorts.(match s with
+ | SProp | Prop | Set ->
+ (* To anticipate a possible restriction on an elimination from
+ SProp, Prop or (impredicative) Set we preserve the sort of the
+ main branch, knowing that the default impossible case shall
+ always be coercible to one of those *)
+ sigma, s
+ | Type _ ->
+ (* If the sort has algebraic universes, we cannot use this sort a
+ type constraint for the impossible case; especially if the
+ default case is not the canonical one provided in Prop by Coq
+ but one given by the user, which may be in either sort (an
+ example is in Vector.caseS', even if this one can probably be
+ put in Prop too with some care) *)
+ let sigma, s' = Evd.new_sort_variable univ_flexible sigma in
+ let sigma = Evd.set_leq_sort !!env sigma s s' in
+ sigma, s') in
let pb =
{ env = pb_env;
pred = (*ty *) mkSort s;
@@ -2066,6 +2080,15 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars
Some (sigma', p, arsign)
with e when precatchable_exception e -> None
+let expected_elimination_sort env tomatchl =
+ List.fold_right (fun (_,tm) s ->
+ match tm with
+ | IsInd (_,IndType(indf,_),_) ->
+ (* Not a degenerated line, see coerce_to_indtype *)
+ let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in
+ if Sorts.family_leq s s' then s else s'
+ | NotInd _ -> s) tomatchl Sorts.InType
+
(* Builds the predicate. If the predicate is dependent, its context is
* made of 1+nrealargs assumptions for each matched term in an inductive
* type and 1 assumption for each term not _syntactically_ in an
@@ -2116,8 +2139,12 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty
| Some rtntyp ->
(* We extract the signature of the arity *)
let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
- let sigma, newt = new_sort_variable univ_flexible sigma in
- let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
+ (* We put a type constraint on the predicate so that one
+ branch type-checked first does not lead to a lower type than
+ another branch; we take into account the possible elimination
+ constraints on the predicate *)
+ let sigma, rtnsort = fresh_sort_in_family sigma (expected_elimination_sort !!env tomatchs) in
+ let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in
let predccl = nf_evar sigma predcclj.uj_val in
[sigma, predccl, building_arsign]
in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cbf539c1e9..00d4c7b3d8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1620,12 +1620,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
in
Success (solve_refl ~can_drop:true f flags env evd
(position_problem true pbty) evk1 args1 args2)
- | Evar ev1, Evar ev2 when app_empty ->
+ | Evar (evk1,_ as ev1), Evar ev2 when app_empty ->
(* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
- Success (solve_evar_evar ~force:true
+ (try
+ Success (solve_evar_evar ~force:true
(evar_define evar_unify flags ~choose:true)
evar_unify flags env evd
(position_problem true pbty) ev1 ev2)
+ with IllTypedInstance (env,t,u) ->
+ UnifFailure (evd,InstanceNotSameType (evk1,env,t,u)))
| Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
(* and otherwise second-order matching *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..44414aa6a0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -227,8 +227,7 @@ let recheck_applications unify flags env evdref t =
(match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
| Success evd -> evdref := evd;
aux (succ i) (subst1 args.(i) codom)
- | UnifFailure (evd, reason) ->
- Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+ | UnifFailure (evd, reason) -> raise (IllTypedInstance (env, ty, argsty.(i))))
| _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
else ()
in aux 0 fty
@@ -810,7 +809,8 @@ let check_evar_instance unify flags env evd evk1 body =
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
let ty =
try Retyping.get_type_of ~lax:true evenv evd body
- with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
+ with Retyping.RetypeError _ ->
+ let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance"))
in
match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
| Success evd -> evd
@@ -935,13 +935,6 @@ let project_with_effects aliases sigma t subst =
in
filter_solution (Int.Map.fold is_projectable subst [])
-open Context.Named.Declaration
-let rec find_solution_type evarenv = function
- | (id,ProjectVar)::l -> get_type (lookup_named id evarenv)
- | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv)
- | (id,ProjectEvar _)::l -> find_solution_type evarenv l
- | [] -> assert false
-
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -1552,10 +1545,10 @@ let rec invert_definition unify flags choose imitate_defs
raise (NotEnoughInformationToProgress sols);
(* No unique projection but still restrict to where it is possible *)
(* materializing is necessary, but is restricting useful? *)
- let ty = find_solution_type (evar_filtered_env env evi) sols in
- let ty' = instantiate_evar_array evi ty argsv in
+ let t' = of_alias t in
+ let ty = Retyping.get_type_of env !evdref t' in
let (evd,evar,(evk',argsv' as ev')) =
- materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
+ materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty in
let ts = expansions_of_var evd aliases t in
let test c = isEvar evd c || List.exists (is_alias evd c) ts in
let filter = restrict_upon_filter evd evk test argsv' in
@@ -1564,7 +1557,7 @@ let rec invert_definition unify flags choose imitate_defs
let evd = match candidates with
| NoUpdate ->
let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
- add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd
+ add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t') evd
| UpdateWith _ ->
restrict_evar evd evk' filter candidates
in
@@ -1575,7 +1568,7 @@ let rec invert_definition unify flags choose imitate_defs
match EConstr.kind !evdref t with
| Rel i when i>k ->
let open Context.Rel.Declaration in
- (match Environ.lookup_rel (i-k) env' with
+ (match Environ.lookup_rel i env' with
| LocalAssum _ -> project_variable (RelAlias (i-k))
| LocalDef (_,b,_) ->
try project_variable (RelAlias (i-k))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 8ff2d7fc63..094dae4828 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind ->
Preconditions:
- [ev] does not occur in [c].
- [c] does not contain any Meta(_)
- *)
+
+ If [ev] and [c] have non inferably convertible types, an exception
+ [IllTypedInstance] is raised *)
val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
Evar.t -> constr -> evar_map
@@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
some problems that cannot be solved in a unique way (except if choose is
- true); fails if the instance is not valid for the given [ev] *)
+ true); fails if the instance is not valid for the given [ev];
+ If [ev] and [c] have non inferably convertible types, an exception
+ [IllTypedInstance] is raised *)
val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool ->
env -> evar_map -> bool option -> existential -> constr -> evar_map
@@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool ->
(env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
unifier -> unify_flags ->
env -> evar_map -> bool option -> existential -> existential -> evar_map
+ (** The two evars are expected to be in inferably convertible types;
+ if not, an exception IllTypedInstance is raised *)
val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map ->
bool option * existential * constr -> unification_result
@@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
exception IllTypedInstance of env * types * types
-(* May raise IllTypedInstance if types are not convertible *)
val check_evar_instance : unifier -> unify_flags ->
env -> evar_map -> Evar.t -> constr -> evar_map
+ (** May raise IllTypedInstance if types are not convertible *)
val remove_instance_local_defs :
evar_map -> Evar.t -> 'a list -> 'a list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 982814fdfc..c352a6ac1f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -38,7 +38,7 @@ type metabinding = (metavariable * EConstr.constr * (instance_constraint * insta
type subst0 =
(evar_map *
metabinding list *
- (Environ.env * EConstr.existential * EConstr.t) list)
+ ((Environ.env * int) * EConstr.existential * EConstr.t) list)
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -227,7 +227,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0)
| Evar ev ->
let env' = pop_rel_context nb env in
let sigma,c = pose_all_metas_as_evars env' sigma c in
- sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst
+ sigma,metasubst,((env,nb),ev,solve_pattern_eqn env sigma l c)::evarsubst
| _ -> assert false
let push d (env,n) = (push_rel_assum d env,n+1)
@@ -769,21 +769,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Some sigma ->
sigma, metasubst, evarsubst
| None ->
- sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cN)::evarsubst)
end
| Evar (evk,_ as ev), _
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cN) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cnvars cmvars then
- sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cN)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Evar (evk,_ as ev)
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cM) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cmvars cnvars then
- sigma,metasubst,((curenv,ev,cM)::evarsubst)
+ sigma,metasubst,((curenvnb,ev,cM)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| Sort s1, Sort s2 ->
(try
@@ -1357,7 +1357,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
(* Process evars *)
match evars with
- | (curenv,(evk,_ as ev),rhs)::evars' ->
+ | ((curenv,nb),(evk,_ as ev),rhs)::evars' ->
if Evd.is_defined evd evk then
let v = mkEvar ev in
let (evd,metas',evars'') =
@@ -1376,7 +1376,8 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
w_merge_rec evd' metas evars eqns
else
let evd' =
- let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
+ let env' = pop_rel_context nb curenv in
+ let evd', rhs'' = pose_all_metas_as_evars env' evd rhs' in
try solve_simple_evar_eqn eflags curenv evd' ev rhs''
with Retyping.RetypeError _ ->
error_cannot_unify curenv evd' (mkEvar ev,rhs'')
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 5462e09359..077597c278 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -105,7 +105,7 @@ type metabinding = (metavariable * constr * (instance_constraint * instance_typi
type subst0 =
(evar_map *
metabinding list *
- (Environ.env * existential * t) list)
+ ((Environ.env * int) * existential * t) list)
val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:04:15 +0000