Jesper Cockx

Since there's an alternative solution I'm closing this issue. If there is still a need for a new primitive, feel free to reopen this or open a new issue/PR.

> However, if I understood the https://github.com/agda/agda/issues/5923#issuecomment-1140434684 of https://github.com/agda/agda/issues/5923 correctly, this is also the case for rewriting with eta-equality, because of singleton types. (Please correct me if that's wrong.) Indeed,...

In the past we have often made experimental flags not compatible with --safe, even though in principle they do not add any inconsistencies (see for example `--prop`). If this is...

This works fine for me. @andreasabel can you confirm this is still a problem?

Can't we just have a `Foldable` that is parametrized over the level of the return type? At least that's what @UlfNorell did in https://github.com/UlfNorell/agda-prelude/blob/master/src/Container/Foldable.agda.

@andreasabel what's the status on this? Since this would be a new feature, I think it would be a bad idea to add it this close to the release, so...

This seems to be caused by the promotion of metavariables in the occurs checker that I introduced in https://github.com/agda/agda/commit/d1a9d7d5f5422701037ae48d780feeafd30a82c0, so it might have the same root cause as https://github.com/agda/agda/issues/5845

Here is a minimized example: ```agda postulate ANY : ∀ {a} {A : Set a} → A variable A : Set _ F : ∀ {l} (A : Set l)...

The cause here seems indeed to be https://github.com/agda/agda/commit/982e18cdcbb2355d571bc05a8a98811fe6b48525, as applications of `F` used to be treated as neutrals in between its declaration and definition, but now they are treated as...

Pro of treating not-yet-defined functions as postulates: - Postulates are considered injective, so more metas can be solved. Con of treating not-yet-defined functions as postulates: - Postulates are rigid symbols,...