Loss of subject reduction with Setω

[L-TChen]

Subject reduction is lost with Setω. Consider

bad : Setω
bad = λ (ℓ : ⊤ → Level) → ∀ t → Set (ℓ t)) (λ _ → lzero) 

whose type is Setω but after normalisation it becomes

bad = (t : ⊤) → Set

whose type is now Set₁. Indeed, if we fill the hole with the normalised expression by C-c C-m, Agda happily produces the second expression and complains about the term it just produced ... Any idea?

[nad]

The only theoretical work in this area (first-class level types and Setω) that I am aware of is @AndrasKovacs' Generalized Universe Hierarchies and First-Class Universe Levels. However, that paper does not seem to address subject reduction.

[andreasabel]

In type theories with subtyping, reduction may produce something of a more precise type. So, with --cumulativity, this would be perfectly fine.
Agda's double checker uses cumulativity always, independent of flag --cumulativity, so this subject reduction "problem" isn't found by the double checker:

{-# OPTIONS --no-cumulativity #-}
{-# OPTIONS --double-check #-}
{-# OPTIONS -v tc.check.internal:20 #-}

open import Agda.Primitive

record ⊤ : Set where

bad : Setω
bad = (λ (ℓ : ⊤ → Level) → ∀ t → Set (ℓ t)) (λ _ → lzero)

-- checking internal  (t : ⊤) → Set lzero : Setω

[jespercockx]

Perhaps it would make more sense to only assign type Setω to a pi type (x : A) → Set e if the variable x occurs strongly rigid in the expression e. This breaks backwards compatibility, but that's probably a price worth paying to preserve subject reduction.

[jespercockx]

Actually the occurrence of t in ℓ t is counted as strongly rigid, so the solution I suggested above does not work.

[jespercockx]

I have implemented an experimental fix for this issue, which you can find at https://github.com/jespercockx/agda/tree/Issue5810. However the builtin cubical modules fail to compile with it. Specifically, I get an error on the type of primComp:

  primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1

The problem here is in the type of u, which is ∀ i → Partial φ (A i). The type of of Partial φ (A i) is SSet (ℓ i), and since this depends on i, the type ∀ i → Partial φ (A i) gets assigned type SSetω. However this exhibits exactly the problem we are talking about in this issue: if ℓ is instantiated with a constant function, say λ _ → lzero, the type of Partial φ (A i) becomes SSet lzero, and hence the ∀ i → Partial φ (A i) now has type SSet lzero too. So already our builtin modules contain expressions that do not satisfy subject reduction in this manner!

I'm summoning the cubical overlords @Saizan @mortberg @plt-amy so hopefully they can give me an idea what the sort of ∀ i → Partial φ (A i) should be here.

[plt-amy]

Ah, we're being bitten in the behind by comp/transp taking a line of levels. Here's what @Saizan had to say on this when it last came up: #3722 (comment). I think the right move is:

Now, the sort of B should not actually depend on x when the sort of (x : A) -> B is not set-omega, however i did not feel it was safe to make use of this invariant at the time. Perhaps I should have. (Then one could strengthen the sort of B).

We can't transport/compose in Setω anyway, so it wouldn't be a big loss to change primComp/primTransp to take Level rather than I → Level.

[jespercockx]

So to experiment I disabled my check when --cubical is enabled and (while many tests then pass) there are a number of other test cases that then fail:

• Succeed/Issue930.agda contains the postulate P : (a : ⊤) → Set (q a) (though q is also a postulate so it cannot actually be instantiated).

  agda/test/Succeed/Issue930.agda

  Line 28 in d50b1e9

  P : (a : ⊤) → Set (q a)

• Succeed/Issue2408.agda contains the postulate F : .(a : A) → Set (l a) (though l is also a postulate so it cannot actually be instantiated)

  agda/test/Succeed/Issue2408.agda

  Line 15 in d50b1e9

  F : .(a : A) → Set (l a)

• Succeed/Issue2408Unused.agda contains the postulate F : (a : ⊥) → Set (l u a) (though l u a is blocked on the postulate u so it cannot actually be reduced).

  agda/test/Succeed/Issue2408Unused.agda

  Line 23 in d50b1e9

  F : (a : ⊥) → Set (l u a)

• Fail/Issue2408/LevelDependentOnIrrelevant contains the postulate .(a : A) → Set (l a)

  agda/test/Fail/Issue2408/LevelDependentOnIrrelevant.agda

  Line 14 in d50b1e9

  F : .(a : A) → Set (l a)

• Succeed/Cumulativity.agda has a bunch of unsolved constraints.

In addition, many error messages get more cluttered with extra "Has PTS rule: ..." constraints (Issue399.agda, Issue2344.agda, Issue2420.agda, Issue2834.agda, Issue2927.agda, Issue3044.agda, Issue4401.agda, ...) Personally I am more worried about these because they will make Agda's constraints (even) harder to read. Since these PTS constraints always arise from unsolved metavariables, perhaps we could hide them from the constraint output by default (and allow toggling them on with a flag perhaps).

I am also trying my fix on the std-lib, and I run into problems with the Nary constructions, specifically Sets in Function.Nary.Nondependent.Base:

Sets : ∀ n (ls : Levels n) → Set (Level.suc (⨆ n ls))

This shows a more serious limitation of my current attempt: the level Level.suc (⨆ n ls) is blocked on n first and not on ls, so (ls : Levels n) → Set (Level.suc (⨆ n ls)) is not accepted by my check.

It feels to me that this might require some more discussion and careful thought before we can have a fix that is both sufficient and does not break a bunch of sensible existing code that plays around with universe levels. Because of this and since this is not a regression, I am bumping this to 2.6.4.

[andreasabel]

Setomega is really a truncation of what would be naturally ordinal levels. Say we have construction for limit levels

sup : (A : Set) (f : A -> Level) -> Level

then (x : A) -> Set (f x) does not live a Setomega but simply in Set (sup A \ x -> lsuc (f x)). Once f x = lzero is known, this collapses to Set (sup A \ _ -> lsuc zero) = Set1.

We currently round up every limit on levels to omega and assign universe Setomega as safe choice. Of course, this loses information which might be regained by reduction.
So, the principled solution for the OP is to have cumulativity for Setomega. Then the gained information can be discarded, as wished, by the subsumption rule, and we have "subject reduction" back.

[nad]

If cumulativity is added for Setω, then I think Setω should be hidden behind a flag. (I think that Setω should be hidden behind a flag anyway, but I think the case for that is stronger with cumulativity.)

[L-TChen]

I’d second @andreasabel’s suggestion. The text of this issue might be misleading as I didn’t know what to expect at first, so I hinted that subject reduction should be restored.

[ On the other hand, not directly relevant to this issue, what is first-class universe level anyway? Can we learn something from @AndrasKovacs‘s work and lay the groundwork of what Agda is using precisely? ]

[andreasabel]

If cumulativity is added for Setω, then I think Setω should be hidden behind a flag. (I think that Setω should be hidden behind a flag anyway, but I think the case for that is stronger with cumulativity.)

Could you elaborate why?

[nad]

Lots of code breaks if --cumulativity is enabled, presumably because it is harder to infer levels.

Furthermore the current implementation of cumulativity is experimental, it is hidden behind a flag, and it is not compatible with --safe.

[andreasabel]

Yes, but we could make Setomega cumulative and leave the other universes alone. So, we do not need to enable --cumulativity in general.

[jespercockx]

Having subtyping Set i <: Setomega is an interesting idea, fixing the problem by making Agda more liberal rather than more restrictive. I can see both advantages and disadvantages of this approach:

• The advantage is that it is backwards compatible and arguably more intuitive than some kind of syntactic restriction
• The disadvantage is that it makes Agda's metatheory more complicated, and also (re)introduces subtyping to Agda which has been problematic wrt constraint solving.

[nad]

I don't want to have any subtyping enabled by default (unless perhaps if someone finds a good way to combine subtyping with Agda's treatment of meta-variables).