I will be on vacation for 2 weeks after today
I may still do some things but don't wait for me
I leave you with a new inconsistency ;)
I claim prior art on this one.
it was breaking a test in https://github.com/coq/coq/pull/15908 but I didn't dig deeper
(I thought let bindings were always expanded or something)
they're not expanded in your fast path
not in the version pushed, but with an intermediate one
it was precisely breaking a (A : Type := Type) in the test-suite
but well it doesn't really matter
we know have an inconsistency to fix, yay
I see
@ppedrot ppedrot force-pushed the template-invariant-cumul branch from 281ca0d to 9889dd5 2 days ago
281ca0d has no test suite failures
9889dd5 has the broken fast path
Pierre-Marie Pédrot said:
but well it doesn't really matter
it matters if we have multiple related but not quite the same bugs
then if we fix one the other might survive
we seem to have more tests for template poly than for cumulative
we've been burned more with the former...
so if we fix it and the PR using inferCumul for template is still broken we'll know
I removed your fast path in the merge commit I pushed btw (it conflicted)
there are two ways to fix the bug, either we make the section universe invariant or we recheck the variance when closing a section
what's the more reasonable design?
(given that you can't specify cumulativity per universe / inductive pair)
Pierre-Marie Pédrot said:
(given that you can't specify cumulativity per universe / inductive pair)
we do though
mind_sec_variance in the mutual_inductive_body
section universes are likely to be irrelevant as typically they're the universe of a parameter
so for a quick fix we may be better of rechecking
but we have no syntax for this, I mean
in general you can't even do that because cumulativity only makes sense for arities
reinferring at section closing goes against the no-inference-rule in the kernel
Last updated: Oct 13 2024 at 01:02 UTC