From 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 16 Feb 2018 15:44:44 +0100 Subject: Allow using cumulativity without forcing strict constraints. Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. --- pretyping/unification.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f4269a2c5..1cd8d3940 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -568,10 +568,10 @@ let force_eqs c = Universes.Constraints.add c' acc) c Universes.Constraints.empty -let constr_cmp pb sigma flags t u = +let constr_cmp pb env sigma flags t u = let cstrs = - if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u - else EConstr.leq_constr_universes sigma t u + if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u + else EConstr.leq_constr_universes env sigma t u in match cstrs with | Some cstrs -> @@ -736,7 +736,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb sigma flags cM cN in + let sigma',b = constr_cmp cv_pb env sigma flags cM cN in if b then sigma',metasubst,evarsubst else @@ -918,7 +918,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb sigma flags cM cN in + let sigma', b = constr_cmp cv_pb env sigma flags cM cN in if b then (sigma', metas, evars) else try reduce curenvnb pb opt substn cM cN @@ -1087,7 +1087,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n - | _ -> constr_cmp cv_pb sigma flags m n in + | _ -> constr_cmp cv_pb env sigma flags m n in if b then Some sigma else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> -- cgit v1.2.3