Internal error when trying to overflow levels

[ksqsf]

The following code will cause an internal error:

module Test where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

_ : Set1 ≡ Set18446744073709551615
_ = refl

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Utils/Suffix.hs:23:17 in Agd-2.6.2-d23be80f:Agda.Utils.Suffix

Information:

• Agda version 2.6.2
• MacOS 12.1

[andreasabel]

This is Int overflow,

ghci> 18446744073709551615 :: Int

<interactive>:1:1: warning: [-Woverflowed-literals]
    Literal 18446744073709551615 is out of the Int range -9223372036854775808..9223372036854775807
-1

because suffixes are Int:

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

Lines 39 to 42 in 015759c

	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).

Actually, we already get the crash at (maxBound :: Int) + 1:

crash' : Set ≡ Set9223372036854775808
crash' = refl

There are two avenues to fix this:

1. Relax suffixes to Integer. Then you can have as many concrete universes as number of atoms in the physical universe, and more.
2. Give a proper error stating that Agda does not support so many concrete universes.

Alt 1 will possibly come with performance penalties, but these might be small.

Alt 2 might be doable in the parser. Note that in the Set l form, we might never reach Int overflow. At least I think I will probably die before this computation finishes:

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Primitive

natToLevel : Nat → Level
natToLevel zero = lzero
natToLevel (suc n) = lsuc (natToLevel n)

endOfUniverse : Set1 ≡ Set (natToLevel 18446744073709551615)
endOfUniverse = refl

The question is whether we can get from the Set l form to the Set_l internally. Yes, we do:

foo : Set (natToLevel 1) ≡ Set (natToLevel 2)
foo = refl

Set₃ != Set₂

CONCLUSION: The easiest and most robust fix is Alt 1 (Integer).