Put indexed data types in the right universes #2030
Conversation
To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default. There is an infective flag `--large-indices` to bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with `--no-large-indices` instead of adding the flag to the modules that used them.
andreasabel
changed the title
|
Added a CHANGELOG entry (and fixed whitespace violations there). |
|
I suppose the stdlib tsars are on vacation/busy atm. To clear the road for an Agda 2.6.4 RC, I am merging this now. These are anyhow mild changes... |
|
It would be nice indeed to not have a bottleneck of a single person who merges PRs. I've discussed a bit with @jamesmckinna who has also talked w/ @MatthewDaggitt about it, but I don't think it has gone beyond that. [I don't really want that power myself! I just would like the process to be a little faster without putting undue pressure onto a single person.] |
|
Well there is more than one person with the power to merge PRs here (as Andreas just demonstrated). It is just a power that's rarely exercised. |
|
AFAIK, I have the power too - but I'd like to know when I (and others) should use it. I think @andreasabel did the right thing, BTW. |
|
@JacquesCarette do you want to start a thread to discuss this on Zulip? |
|
I think I'm going to wait until the most active people seem to be back online - but yes, good idea. |
Base #2028 on
masterinstead of on outdatedexperimental.@plt-amy writes:
To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default.
There is an infective flag
--large-indicesto bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with--no-large-indicesinstead of adding the flag to the modules that used them.