Universe overflow causes Russell's paradox

[Trebor-Huang]

Version used: Agda 2.6.2.1

{-# OPTIONS --safe #-}
module set-in-set where
-- Basically just a modified version of http://liamoc.net/posts/2015-09-10-girards-paradox.html
-- Some preliminaries, just to avoid any library imports
data _≡_ {ℓ : _} {A : Set ℓ} : A -> A -> Set where
    refl : ∀ {a} -> a ≡ a

record Σ (A : Set) (P : A -> Set) : Set where
    constructor _,_
    field
        proj₁ : A
        proj₂ : P proj₁
open Σ

data ⊥ : Set where

-- This shows the problem
WTF : Set₀
WTF = Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅
-- 18446744073709551615 = 2^64 - 1

-- The following is basically copying from the link
data SET : Set where
  set : (X : Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅) → (X → SET) → SET

_∈_ : SET → SET → Set
a ∈ set X f = Σ X (λ x → a ≡ f x)

_∉_ : SET → SET → Set
a ∉ b = (a ∈ b) → ⊥

Δ : SET
Δ = set (Σ SET (λ s → s ∉ s)) proj₁

x∈Δ→x∉x : ∀ {X} → X ∈ Δ → X ∉ X
x∈Δ→x∉x ((Y , Y∉Y) , refl) = Y∉Y

Δ∉Δ : Δ ∉ Δ
Δ∉Δ Δ∈Δ = x∈Δ→x∉x Δ∈Δ Δ∈Δ

x∉x→x∈Δ : ∀ {X} →  X ∉ X → X ∈ Δ
x∉x→x∈Δ {X} X∉X = (X , X∉X) , refl

falso : ⊥
falso = Δ∉Δ (x∉x→x∈Δ Δ∉Δ)

[Trebor-Huang]

Discovered by @ksqsf . See the adjacent issue about __IMPOSSIBLE__ errors on subscript formatting.

[Trebor-Huang]

Correction: The error occurs at 2^63.

• At l > 2^63-1, Set_l : Set0 (I'm using pseudo-notation) is accepted, no matter what l is.
• At l = 2^63-1, __IMPOSSIBLE__ occurs.
• At lower levels, Agda correctly rejects the declaration.

[andreasabel]

Curious what introduced this bug:

$ agda-bisect --must-fail --with-compiler ghc-8.8.4 --with-cabal cabal-3.2 --good v2.6.1 --bad v2.6.2 Issue5706.agda 

[Trebor-Huang]

@AliasQli identified that if you change these Ints into Integers then Agda correctly rejects the file.

agda/src/full/Agda/Utils/Suffix.hs

Lines 39 to 42 in 007a26f

	data Suffix
	= Prime Int -- ^ Identifier ends in @Int@ many primes.
	| Index Int -- ^ Identifier ends in number @Int@ (ordinary digits).
	| Subscript Int -- ^ Identifier ends in number @Int@ (subscript digits).

But those were written ages ago.

[andreasabel]

Yes, this is the easiest fix, I am working on a PR. However, I am still curious what causes the regression, and once I have seen the cause, I have more information to decide on a fix.

[andreasabel]

bisect says: 55013a9 is the first bad commit
Date: Mon Oct 19 17:35:36 2020 +0200

[ refactor ] smart constructor [s]sort should use smart univSort

Otherwise, non-normal sorts like (UnivSort (SSet l)) are created.

Unfortunately, that was me. 😊

But it is almost as if I fell into a trap that was laid out over time. So I suppose fixing Utils.Suffix to use Integer is the right way to go.

[gallais]

I suspect it may come from #4629. Prior to that we could directly parse the level n
in Setn. After that the decomposition into name + suffix can only be done after /
during scope checking and so we started repurposing Agda.Utils.Suffix only originally
used for name generation (when case splitting / shadowing).