Andreas Abel

This is more an issue for the standard library. It works if you assume `S : Setoid a (a ⊔ ℓ)` instead. Apparently the second level has to be at...

> To help this, I tried > > lift : Setoid a ℓ → Setoid a (a ⊔ ℓ) > lift S = S > But it is rejected. Is...

Using `Setoid a (a ⊔ ℓ)` instead of `Setoid a ℓ` restricts uses to situation where the type of the equality relation is at least as big as the type...

I'd rather not have a non-conservative fix just before the release. The issue #6697 is not pressing. However, disabling previously legal rewrite relation leaves the user without workarounds.

Oh we missed the chance to merge this just after the 2.7 release. Now we are in the same situation again...

@jespercockx : Maybe a good time now to revive this PR.

> This shows that `--level-universe` should not only be considered coinfective (as it already is) but also _infective_. Ouch!

Frankly, I don't understand why `Level : Set` should be problematic, and why there should be a `LevelUniv`. In particular with the few levels we have in `Level` (`omega` many...

On a less fundamental note, this seems to be just another instance of - #5810 It seems to be due to a lack of subtyping `Set1

This error stems from an uncaught `patternViolation` here: https://github.com/agda/agda/blob/2ee8d18194b6f6db1f144c12cb177dbc17089d5e/src/full/Agda/Interaction/BasicOps.hs#L205-L207 (Maybe we should ~~equip `patternViolation`~~ use `patternViolation'` with some explanation ~~or call stack for the sake of debugging~~ more often and...