Fix #11039: proof of False with template poly and nonlinear universes #11128
Conversation
SkySkimmer
added
part: universes
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
591a729 to
9f554a2
Compare
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
9f554a2 to
2bf6820
Compare
| @@ -257,7 +257,6 @@ Ltac blocked t := block_goal ; t ; unblock_goal. | |||
| be used by the [equations] resolver. It is especially useful to register the dependent elimination | |||
| principles for things in [Prop] which are not automatically generated. *) | |||
|
|
|||
| #[universes(template)] | |||
| Class DependentEliminationPackage (A : Type) := | |||
| { elim_type : Type ; elim : elim_type }. | |||
There was a problem hiding this comment.
This type and the one in ssrbool were not actually template.
kernel/indTyping.ml
Outdated
| (fun levels (d,c) -> | ||
| List.fold_left (fun levels d -> | ||
| Context.Rel.Declaration.fold_constr (fun c levels -> | ||
| Vars.with_universes_of_constr levels c) |
There was a problem hiding this comment.
Why not simply a union instead of exporting a new function? This is very unlikely to be performance-critical.
There was a problem hiding this comment.
because I got tired of typing these damn unions in the middle of writing the patch
There was a problem hiding this comment.
Come on, write a union and be done with it.
vernac/comInductive.mli
Outdated
| -> Entries.universes_entry | ||
| -> Constr.rel_context | ||
| -> Sorts.t option | ||
| -> bool | ||
| (** [template_polymorphism_candidate env uctx params conclsort] is |
There was a problem hiding this comment.
Would be good to update this comment as well.
There was a problem hiding this comment.
Appart from @ppedrot 's suggestion to use a union, which I second, the patch looks good to me.
If the universe is local, and does not appear in the constructors, then it can't be hidden under a definition. The only thing I can see that would allow to refer to the level is hence Ind I (A : Type@{i}) : Type@{j} := foo (B : Type@{k}) : I B -> I A but that would bound i from below, or nesting Ind I (A : Type@{i}) : Type@{i} := bar : list A -> I A and that is just transitively template poly.
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
2bf6820 to
d6e9338
Compare
SkySkimmer
added
the
needs: progress
|
This patch is still not enough, #[universes(template)]
Inductive foo@{i} (A:Type@{i}) (T:=Type@{i}:Type@{i+1}) : Type@{i+1}
:= bar (X:T) : foo A.goes through. Not sure how to fix this, maybe use a variant of |
|
What about using the same code as the one for irrelevant cumulative inductive types? |
|
I don't know what you mean by that. |
|
A variant of |
|
Type-check the inductive type as if it were a polymorphic cumulative one, check that all template indices are indeed irrelevant, and use the monomorphic constraints above for partial application. |
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
d6e9338 to
076984b
Compare
That sounds complicated, especially considering we run the check in the upper layers to decide if we're auto template. I added an optional rel_context argument to univs_of_constr instead. |
SkySkimmer
removed
the
needs: progress
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
a975dfc to
f6ba117
Compare
|
@SkySkimmer this still looks a bit ad-hoc and probably leaky. What about unconditionally adding the constraints appearing in let bodies? If the user starts using let binders in the context, they deserve it. |
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
f6ba117 to
f11f1cf
Compare
Sure, why not |
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
f11f1cf to
8e7de1e
Compare
|
Is this still waiting on something? |
dev/doc/critical-bugs
Outdated
| previous issue about template polymorphism exploiting other ways to | ||
| generate untracked constraints | ||
| introduced: morally at the introduction of template polymorphism, 23 | ||
| May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at |
There was a problem hiding this comment.
| May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at | |
| May 2006, 9c2d70b, r8845, Herbelin | |
| impacted released versions: at |
|
I can assign and merge if needed. |
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes coq#10504.
and do not run template_candidate in the upper layers when the template attribute is given. This means we can use an over-approximation in the upper layer implementation of template_candidate (returning false even in cases which the kernel may accept) if we ever want to.
SkySkimmer
force-pushed
the
fix-11039-template-poly-nonlinear-false
branch
from
8e7de1e to
1db8720
Compare
|
Pierre-Marie, please do so. And we will contemplate the release of 8.10.2. |
…ly and nonlinear universes
…ly and nonlinear universes
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.