aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml59
-rw-r--r--pretyping/evarsolve.ml5
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/unification.mli2
4 files changed, 55 insertions, 26 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/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..c58ebe1bbd 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -810,7 +810,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
@@ -1575,7 +1576,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/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-05 10:51:37 +0000