diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-16 15:44:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:29:06 +0100 |
| commit | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (patch) | |
| tree | 605a2dae6692cec6503ab5fcdce7c90421db26f0 /pretyping/unification.ml | |
| parent | 3d86afb36517c9ba4200289e169239f7fa54fca1 (diff) | |
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.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) -> |