Add testcase for #461

This will not compile until @janno's stdpp fix is merged.

Old description

See explanation in #461 (comment 80771).

This allows the example to pass, but I don't know that this is the right change, and I don't understand the graph produced with this change.

Moreover, it might restore one annoyance that stdpp!368 (merged) complained about (not sure if this is still an annoyance):

In Iris, what this means is that bi_tforall/bi_texist have different universe levels than bi_forall/bi_exist.

I suspect this overall lets bi_tforall/bi_texist take a tele@{U} for some fixed U such that U < bi.Quant. That might be okay, since nobody nests telescopes (else we'd have to make them universe-polymorphic, triggering issues elsewhere).

mentioned in issue #461 (closed)

changed the description

That might be okay, since nobody nests telescopes (else we'd have to make them universe-polymorphic, triggering issues elsewhere).

This can't be right because stdpp telescopes are already universe polymorphic.

I wonder if this whole thing can be fixed by making telescopes cumulatively universe polymorphic. I'll make a new switch to test that.

Indeed, it seems cumulativity is all it takes. I can make the test case pass with just that. The problem seems (and I say "seems" because I have done zero investigation) to be from the fact that we are forcing telescopes in bi_tforall/bi_texist into the highest possible universe, Quant, and since not all binders used in telescopes enjoy cumulativity, this will eventually fail. I don't recommend universe polymorphic types without cumulativity, especially abstract types such as telescopes. There are however some performance downsides to cumulativity that have only been addressed recently (https://github.com/coq/coq/issues/11741). If we enable cumulativity we should probably run the full iris benchmark suite to make sure performance is not affected to a noticeable degree.

@robbertkrebbers was there a reason that telescopes are not already cumulatively universe polymorphic? I vaguely remember talking to some iris developer about this a long time ago but I cannot figure out who it was and if there was indeed a reason for it.

Regarding cumulativity, see stdpp!368 (comment 78939)

It is great that cumulativity solves this problem. Is it possible to come up with a self-contained test for std++?

Regarding cumulativity, see stdpp!368 (comment 78939)

I'd say the problem this MR tries to address is a good reason for cumulativity. I understand @jung's hesitation in using off-by-default flags but with cumulativity it is almost the prudent option to enable it in order to make the types more useful. (As I mentioned above, there can be performance issues but these should only show up in somewhat contrived examples in which Coq needs to unfold many many definitions to compute variance of universes.)

It is great that cumulativity solves this problem. Is it possible to come up with a self-contained test for std++?

I think the test case should be easy enough to minimize. I'll have a go at this.

It is great that cumulativity solves this problem. Is it possible to come up with a self-contained test for std++?

I think the test case should be easy enough to minimize. I'll have a go at this.

Actually, I am not sure that minimizing the example is worth anybody's time. It wouldn't test anything more than cumulativity and that on its own is much easier to test:

(* Assert that telescopes are cumulatively universe polymorphic. *)
Section Cumulativity.
  Monomorphic Universes Quant local.
  Monomorphic Constraint local < Quant.
  Example cumul (t : tele@{local}) : tele@{Quant} := t.
End Cumulativity.

It's hard to do pre-landing benchmarks for std++ changes, but if the chances of a regression are low then we can just do that post-landing.

No strong opinion on whether we should remove the Quant universe or unlock cumulative universes, but it seems our resident universe expert prefers the latter so that is fine with me.

added 2 commits

• 09b6a0c3 - Add testcase for #461 (closed)
• b7f57848 - Bad fix (to replace with Janno's)

Compare with previous version

Rebased. I'm going to remove this bad fix, but I kept the (reviewed) testcase.

marked this merge request as ready

changed title from Draft: Work around #461: Revert bi.telescope changes to Add testcase for #461

changed the description

Here's my stdpp mR: stdpp!380 (merged)

added 2 commits

• 5c6621c2 - Bump stdpp for universe fix
• 8aa6d9eb - Add testcase for #461 (closed)

Compare with previous version

added 5 commits

• 8aa6d9eb...1b5e1bc6 - 3 commits from branch iris:master
• e60de03f - Bump stdpp for universe fix
• 9851ef8d - Add testcase for #461 (closed)

Compare with previous version

changed the description

This is now optional, but might help benchmarking. You're welcome to take over :-).

resolved all threads

merged

mentioned in commit 9dd4d1ea