From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 22 Oct 2016 11:03:13 +0200 Subject: Renamings to avoid confusion deprecating old names reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics --- pretyping/evarsolve.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'pretyping/evarsolve.ml') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f1526facc..f0aa9b564 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1603,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) -let reconsider_conv_pbs conv_algo evd = +let reconsider_unif_constraints conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left (fun p (pbty,env,t1,t2 as x) -> @@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd = (Success evd) pbs +let reconsider_conv_pbs = reconsider_unif_constraints + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_conv_pbs conv_algo evd + reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) -- cgit v1.2.3 From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:25:05 +0100 Subject: Fix UGraph.check_eq! Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code --- engine/evd.ml | 7 ++ engine/evd.mli | 3 +- kernel/uGraph.ml | 21 ++-- pretyping/cases.ml | 11 +- pretyping/cases.mli | 5 +- pretyping/evarsolve.ml | 41 ++++---- test-suite/bugs/closed/5208.v | 222 +++++++++++++++++++++++++++++++++++++++++ test-suite/success/Inductive.v | 21 ++++ toplevel/command.ml | 8 +- 9 files changed, 294 insertions(+), 45 deletions(-) create mode 100644 test-suite/bugs/closed/5208.v (limited to 'pretyping/evarsolve.ml') diff --git a/engine/evd.ml b/engine/evd.ml index aa91fc522..a6b6f742b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -854,6 +854,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in diff --git a/engine/evd.mli b/engine/evd.mli index b47b389d1..89dcd92ce 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -514,7 +514,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map - + +val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e2712615b..4884d0deb 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -638,19 +638,6 @@ let check_smaller g strict u v = type 'a check_function = universes -> 'a -> 'a -> bool -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in - Universe.for_all (fun x1 -> exists x1 l2) l1 - && Universe.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -669,7 +656,13 @@ let real_check_leq g u v = let check_leq g u v = Universe.equal u v || is_type0m_univ u || - check_eq_univs g u v || real_check_leq g u v + real_check_leq g u v + +let check_eq_univs g l1 l2 = + real_check_leq g l1 l2 && real_check_leq g l2 l1 + +let check_eq g u v = + Universe.equal u v || check_eq_univs g u v (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa24733d9..27c1dd031 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1934,14 +1934,19 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = *) let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = + let refresh_tycon sigma t = + refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) + env sigma t + in let preds = match pred, tycon with (* No return clause *) | None, Some t when not (noccur_with_meta 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) - (* First strategy: we abstract the tycon wrt to the dependencies *) - let p1 = + (* First strategy: we abstract the tycon wrt to the dependencies *) + let sigma, t = refresh_tycon sigma t in + let p1 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in @@ -1952,7 +1957,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) let sigma,t = match tycon with - | Some t -> sigma,t + | Some t -> refresh_tycon sigma t | None -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((t, _), sigma, _) = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ba566f374..ee4148de6 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> Context.Rel.t list -> Constr.constr option -> - 'a option -> (Evd.evar_map * Names.name list * Term.constr) list + glob_constr option -> + (Evd.evar_map * Names.name list * Term.constr) list diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f0aa9b564..02e10d7fc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,33 +42,34 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_level evd s = - match Evd.is_sort_variable evd s with - | None -> true - | Some l -> not (Evd.is_flexible_level evd l) - let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let rec refresh status dir t = - match kind_of_term t with - | Sort (Type u as s) when - (match Univ.universe_level u with - | None -> true - | Some l -> not onlyalg && refresh_level evd s) -> + let refresh_sort status dir s = let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' + modified := true; evdref := evd; mkSort s' + in + let rec refresh onlyalg status dir t = + match kind_of_term t with + | Sort (Type u as s) -> + (match Univ.universe_level u with + | None -> refresh_sort status dir s + | Some l -> + (match Evd.universe_rigidity evd l with + | UnivRigid -> if not onlyalg then refresh_sort status dir s else t + | UnivFlexible alg -> + if onlyalg && alg then + (evdref := Evd.make_flexible_variable !evdref false l; t) + else t)) | Sort (Prop Pos as s) when refreshset && not dir -> - let s' = evd_comb0 (new_sort_variable status) evdref in - let evd = set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' + refresh_sort status dir s | Prod (na,u,v) -> - mkProd (na,u,refresh status dir v) + mkProd (na, u, refresh onlyalg status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = @@ -81,7 +82,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh univ_flexible true evi.evar_concl in + let ty' = refresh onlyalg univ_flexible true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -101,9 +102,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) in let t' = if isArity t then - (match pbty with - | None -> t - | Some dir -> refresh status dir t) + match pbty with + | None -> refresh true univ_flexible false t + | Some dir -> refresh onlyalg status dir t else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v new file mode 100644 index 000000000..b7a684a27 --- /dev/null +++ b/test-suite/bugs/closed/5208.v @@ -0,0 +1,222 @@ +Require Import Program. + +Require Import Coq.Strings.String. +Require Import Coq.Strings.Ascii. +Require Import Coq.Numbers.BinNums. + +Set Implicit Arguments. +Set Strict Implicit. +Set Universe Polymorphism. +Set Printing Universes. + +Local Open Scope positive. + +Definition field : Type := positive. + +Section poly. + Universe U. + + Inductive fields : Type := + | pm_Leaf : fields + | pm_Branch : fields -> option Type@{U} -> fields -> fields. + + Definition fields_left (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch l _ _ => l + end. + + Definition fields_right (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ r => r + end. + + Definition fields_here (f : fields) : option Type@{U} := + match f with + | pm_Leaf => None + | pm_Branch _ s _ => s + end. + + Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} := + match p with + | xH => match m with + | pm_Leaf => None + | pm_Branch _ x _ => x + end + | xO p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch L _ _ => L + end + | xI p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ R => R + end + end. + + Definition fields_leaf : fields := pm_Leaf. + + Inductive member (val : Type@{U}) : fields -> Type := + | pmm_H : forall L R, member val (pm_Branch L (Some val) R) + | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R) + | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R). + Arguments pmm_H {_ _ _}. + Arguments pmm_L {_ _ _ _} _. + Arguments pmm_R {_ _ _ _} _. + + Fixpoint get_member (val : Type@{U}) p {struct p} + : forall m, fields_get p m = @Some Type@{U} val -> member val m := + match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with + | xH => fun m => + match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val => + match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with + | eq_refl => pmm_H + end + end + | xO p' => fun m => + match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val => + @pmm_L _ _ _ _ (@get_member _ p' l pf) + end + | xI p' => fun m => + match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val => + @pmm_R _ _ _ _ (@get_member _ p' r pf) + end + end. + + Inductive record : fields -> Type := + | pr_Leaf : record pm_Leaf + | pr_Branch : forall L R (V : option Type@{U}), + record L -> + match V return Type@{U} with + | None => unit + | Some t => t + end -> + record R -> + record (pm_Branch L V R). + + + Definition record_left {L} {V : option Type@{U}} {R} + (r : record (pm_Branch L V R)) : record L := + match r in record z + return match z with + | pm_Branch L _ _ => record L + | _ => unit + end + with + | pr_Branch _ l _ _ => l + | pr_Leaf => tt + end. +Set Printing All. + Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R)) + : match V return Type@{U} with + | None => unit + | Some t => t + end := + match r in record z + return match z (* return ?X *) with + | pm_Branch _ V _ => match V return Type@{U} with + | None => unit + | Some t => t + end + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_here {L : fields} (v : Type@{U}) {R : fields} + (r : record (pm_Branch L (@Some Type@{U} v) R)) : v := + match r in record z + return match z return Type@{U} with + | pm_Branch _ (Some v) _ => v + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R := + match r in record z return match z with + | pm_Branch _ _ R => record R + | _ => unit + end + with + | pr_Branch _ _ _ r => r + | pr_Leaf => tt + end. + + Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val := + match m in member _ pm return record pm -> val with + | pmm_H => fun r => record_here r + | pmm_L m' => fun r => record_get m' (record_left r) + | pmm_R m' => fun r => record_get m' (record_right r) + end. + + Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m} + : record pm -> record pm := + match m in member _ pm return record pm -> record pm with + | pmm_H => fun r => + pr_Branch (Some _) + (record_left r) + x + (record_right r) + | pmm_L m' => fun r => + pr_Branch _ + (record_set m' x (record_left r)) + (record_at r) + (record_right r) + | pmm_R m' => fun r => + pr_Branch _ (record_left r) + (record_at r) + (record_set m' x (record_right r)) + end. +End poly. +Axiom cheat : forall {A}, A. +Lemma record_get_record_set_different: + forall (T: Type) (vars: fields) + (pmr pmw: member T vars) + (diff: pmr <> pmw) + (r: record vars) (val: T), + record_get pmr (record_set pmw val r) = record_get pmr r. +Proof. + intros. + revert pmr diff r val. + induction pmw; simpl; intros. + - dependent destruction pmr. + + congruence. + + auto. + + auto. + - dependent destruction pmr. + + auto. + + simpl. apply IHpmw. congruence. + + auto. + - dependent destruction pmr. + + auto. + + auto. + + simpl. apply IHpmw. congruence. +Qed. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 9661b3bfa..f746def5c 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. hit the Inductiveops.get_arity bug mentioned above (see #3491) *) Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. + + +Module TemplateProp. + + (** Check lowering of a template universe polymorphic inductive to Prop *) + + Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Check Foo True : Prop. + +End TemplateProp. + +Module PolyNoLowerProp. + + (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *) + + Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Fail Check Foo True : Prop. + +End PolyNoLowerProp. diff --git a/toplevel/command.ml b/toplevel/command.ml index 7ffe680e5..ed3eac51b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -537,11 +537,9 @@ let inductive_levels env evdref poly arities inds = in let duu = Sorts.univ_of_sort du in let evd = - if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then - if is_flexible_sort evd duu then - if Evd.check_leq evd Univ.type0_univ duu then - evd - else Evd.set_eq_sort env evd (Prop Null) du + if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then + Evd.set_eq_sort env evd (Prop Null) du else evd else Evd.set_eq_sort env evd (Type cu) du in -- cgit v1.2.3 From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 18:00:18 +0100 Subject: Document changes --- engine/evd.mli | 12 ++++++++++- kernel/univ.ml | 54 +++++++++++++++++++++++++++++++------------------- pretyping/cases.ml | 3 +++ pretyping/evarsolve.ml | 29 +++++++++++++++++---------- 4 files changed, 66 insertions(+), 32 deletions(-) (limited to 'pretyping/evarsolve.ml') diff --git a/engine/evd.mli b/engine/evd.mli index 89dcd92ce..86887f3dc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (********************************************************* Sort/universe variables *) -(** Rigid or flexible universe variables *) +(** Rigid or flexible universe variables. + + [UnivRigid] variables are user-provided or come from an explicit + [Type] in the source, we do not minimize them or unify them eagerly. + + [UnivFlexible alg] variables are fresh universe variables of + polymorphic constants or generated during refinement, sometimes in + algebraic position (i.e. not appearing in the term at the moment of + creation). They are the candidates for minimization (if alg, to an + algebraic universe) and unified eagerly in the first-order + unification heurstic. *) type rigid = UState.rigid = | UnivRigid diff --git a/kernel/univ.ml b/kernel/univ.ml index c863fac0e..09f884ecd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -468,20 +468,32 @@ struct else if Level.is_prop u then hcons (Level.set,n+k) else hcons (u,n+k) - + + type super_result = + SuperSame of bool + (* The level expressions are in cumulativity relation. boolean + indicates if left is smaller than right? *) + | SuperDiff of int + (* The level expressions are unrelated, the comparison result + is canonical *) + + (** [super u v] compares two level expressions, + returning [SuperSame] if they refer to the same level at potentially different + increments or [SuperDiff] if they are different. The booleans indicate if the + left expression is "smaller" than the right one in both cases. *) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in - if Int.equal cmp 0 then Inl (n < n') + if Int.equal cmp 0 then SuperSame (n < n') else match x, y with | (l,0), (l',0) -> let open RawLevel in (match Level.data l, Level.data l' with - | Prop, Prop -> Inl false - | Prop, _ -> Inl true - | _, Prop -> Inl false - | _, _ -> Inr cmp) - | _, _ -> Inr cmp + | Prop, Prop -> SuperSame false + | Prop, _ -> SuperSame true + | _, Prop -> SuperSame false + | _, _ -> SuperDiff cmp) + | _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -603,24 +615,26 @@ struct | Nil, _ -> l2 | _, Nil -> l1 | Cons (h1, _, t1), Cons (h2, _, t2) -> - (match Expr.super h1 h2 with - | Inl true (* h1 < h2 *) -> merge_univs t1 l2 - | Inl false -> merge_univs l1 t2 - | Inr c -> - if c <= 0 (* h1 < h2 is name order *) - then cons h1 (merge_univs t1 l2) - else cons h2 (merge_univs l1 t2)) + let open Expr in + (match super h1 h2 with + | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 + | SuperSame false -> merge_univs l1 t2 + | SuperDiff c -> + if c <= 0 (* h1 < h2 is name order *) + then cons h1 (merge_univs t1 l2) + else cons h2 (merge_univs l1 t2)) let sort u = let rec aux a l = match l with | Cons (b, _, l') -> - (match Expr.super a b with - | Inl false -> aux a l' - | Inl true -> l - | Inr c -> - if c <= 0 then cons a l - else cons b (aux a l')) + let open Expr in + (match super a b with + | SuperSame false -> aux a l' + | SuperSame true -> l + | SuperDiff c -> + if c <= 0 then cons a l + else cons b (aux a l')) | Nil -> cons a l in fold (fun a acc -> aux a acc) u nil diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 27c1dd031..6e4d72705 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1935,6 +1935,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = + (** If we put the typing constraint in the term, it has to be + refreshed to preserve the invariant that no algebraic universe + can appear in the term. *) refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) env sigma t in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 02e10d7fc..4fd030845 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -46,30 +46,35 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let refresh_sort status dir s = + (* direction: true for fresh universes lower than the existing ones *) + let refresh_sort status ~direction s = let s' = evd_comb0 (new_sort_variable status) evdref in let evd = - if dir then set_leq_sort env !evdref s' s + if direction then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' in - let rec refresh onlyalg status dir t = + let rec refresh ~onlyalg status ~direction t = match kind_of_term t with | Sort (Type u as s) -> (match Univ.universe_level u with - | None -> refresh_sort status dir s + | None -> refresh_sort status ~direction s | Some l -> (match Evd.universe_rigidity evd l with - | UnivRigid -> if not onlyalg then refresh_sort status dir s else t + | UnivRigid -> + if not onlyalg then refresh_sort status ~direction s + else t | UnivFlexible alg -> if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref false l; t) else t)) - | Sort (Prop Pos as s) when refreshset && not dir -> - refresh_sort status dir s + | Sort (Prop Pos as s) when refreshset && not direction -> + (* Cannot make a universe "lower" than "Set", + only refreshing when we want higher universes. *) + refresh_sort status ~direction s | Prod (na,u,v) -> - mkProd (na, u, refresh onlyalg status dir v) + mkProd (na, u, refresh ~onlyalg status ~direction v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = @@ -82,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh onlyalg univ_flexible true evi.evar_concl in + let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -103,8 +108,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let t' = if isArity t then match pbty with - | None -> refresh true univ_flexible false t - | Some dir -> refresh onlyalg status dir t + | None -> + (* No cumulativity needed, but we still need to refresh the algebraics *) + refresh ~onlyalg:true univ_flexible ~direction:false t + | Some direction -> refresh ~onlyalg status ~direction t else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t -- cgit v1.2.3