Fix #5705 fix #5706: switch to Integer in Agda.Utils.Suffix

`Int` suffixes could be exploited by overflow to get Set:Set in Agda
2.6.2(.1).  This is fixed by switching to `Integer` suffixes.

src/full/Agda/Syntax/Scope/Monad.hs

@@ -399,8 +399,8 @@ tryResolveName kinds names x = do
   fromConcreteSuffix = \case
     Nothing              -> Nothing
     Just C.Prime{}       -> Nothing
-    Just (C.Index i)     -> Just $ A.Suffix $ toInteger i
-    Just (C.Subscript i) -> Just $ A.Suffix $ toInteger i
+    Just (C.Index i)     -> Just $ A.Suffix i
+    Just (C.Subscript i) -> Just $ A.Suffix i
 
 -- | Test if a given abstract name can appear with a suffix. Currently
 --   only true for the names of builtin sorts @Set@ and @Prop@.

src/full/Agda/Utils/Suffix.hs

@@ -2,6 +2,7 @@
 module Agda.Utils.Suffix where
 
 import Data.Char
+import qualified Data.List as List
 
 import Agda.Utils.Impossible
 
@@ -37,12 +38,11 @@ fromSubscriptDigit d
 -- | Classification of identifier variants.
 
 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).
+  = Prime     Integer  -- ^ Identifier ends in @Integer@ many primes.
+  | Index     Integer  -- ^ Identifier ends in number @Integer@ (ordinary digits).
+  | Subscript Integer  -- ^ Identifier ends in number @Integer@ (subscript digits).
 
--- | Increase the suffix by one.  If no suffix yet, put a subscript @1@
---   unless users do not want us to use any unicode.
+-- | Increase the suffix by one.
 
 nextSuffix :: Suffix -> Suffix
 nextSuffix (Prime i)     = Prime $ i + 1
@@ -53,17 +53,27 @@ nextSuffix (Subscript i) = Subscript $ i + 1
 
 suffixView :: String -> (String, Maybe Suffix)
 suffixView s
-    | (ps@(_:_), s') <- span (=='\'') rs         = (reverse s', Just $ Prime $ length ps)
+    | (ps@(_:_), s') <- span (=='\'') rs         = (reverse s', Just $ Prime $ List.genericLength ps)
     | (ns@(_:_), s') <- span isDigit rs          = (reverse s', Just $ Index $ read $ reverse ns)
     | (ns@(_:_), s') <- span isSubscriptDigit rs = (reverse s', Just $ Subscript $ read $
                                                       map fromSubscriptDigit $ reverse ns)
     | otherwise                                  = (s, Nothing)
     where rs = reverse s
 
+-- Note: suffixView could be implemented using spanEnd, but the implementation using reverse
+-- looks more efficient, since the reversal is only done once.
+--
+-- suffixView :: String -> (String, Maybe Suffix)
+-- suffixView s
+--     | (s', ps@(_:_)) <- spanEnd (=='\'') s         = (s', Just $ Prime $ length ps)
+--     | (s', ns@(_:_)) <- spanEnd isDigit s          = (s', Just $ Index $ read ns)
+--     | (s', ns@(_:_)) <- spanEnd isSubscriptDigit s = (s', Just $ Subscript $ read $ map fromSubscriptDigit ns)
+--     | otherwise                                    = (s, Nothing)
+
 -- | Print suffix.
 
 renderSuffix :: Suffix -> String
-renderSuffix (Prime n)     = replicate n '\''
+renderSuffix (Prime n)     = List.genericReplicate n '\''
 renderSuffix (Index i)     = show i
 renderSuffix (Subscript i) = map toSubscriptDigit (show i)
 

test/Fail/Issue5705.agda

@@ -0,0 +1,8 @@
+-- Andreas, 2021-12-22, issue #5705 reported by ksqsf
+
+open import Agda.Builtin.Equality
+
+crash : Set ≡ Set9223372036854775808
+crash = refl
+
+-- This should fail, but crashes in Agda 2.6.2 due to Int overflow.

test/Fail/Issue5705.err

@@ -0,0 +1,4 @@
+Issue5705.agda:5,15-37
+Set₉₂₂₃₃₇₂₀₃₆₈₅₄₇₇₅₈₀₉ != Set₁
+when checking that the expression Set₉₂₂₃₃₇₂₀₃₆₈₅₄₇₇₅₈₀₈ has type
+Set₁

test/Fail/Issue5706.agda

@@ -0,0 +1,64 @@
+-- Andreas, 2021-12-22, issue #5706 reported by Trebor-Huang
+-- In Agda <= 2.6.2.1, Int overflow can be exploited.
+
+-- Basically just a modified version of Russell's paradox found at
+-- http://liamoc.net/posts/2015-09-10-girards-paradox.html.
+
+-- -- This 64bit Int overflow got us Set:Set.
+-- WTF : Set₀
+-- WTF = Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅
+-- -- 18446744073709551615 = 2^64 - 1
+
+-- 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
+
+-- The rest follows the linked development of Russell's paradox.
+
+-- Naive sets (tree representation), accepted with --type-in-type.
+
+data SET : Set where
+  set : (X : Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅) → (X → SET) → SET
+
+-- Elementhood
+
+_∈_ : SET → SET → Set
+a ∈ set X f = ∃ λ x → a ≡ f x
+
+_∉_ : SET → SET → Set
+a ∉ b = (a ∈ b) → ⊥
+
+-- The set Δ of sets that do not contain themselves.
+
+Δ : SET
+Δ = set (∃ λ s → s ∉ s) proj₁
+
+-- Any member of Δ does not contain itself.
+
+x∈Δ→x∉x : ∀ {X} → X ∈ Δ → X ∉ X
+x∈Δ→x∉x ((Y , Y∉Y) , refl) = Y∉Y
+
+-- Δ does not contain itself.
+
+Δ∉Δ : Δ ∉ Δ
+Δ∉Δ Δ∈Δ = x∈Δ→x∉x Δ∈Δ Δ∈Δ
+
+-- Any set that does not contain itself lives in Δ.
+
+x∉x→x∈Δ : ∀ {X} →  X ∉ X → X ∈ Δ
+x∉x→x∈Δ {X} X∉X = (X , X∉X) , refl
+
+-- So Δ must live in Δ, which is absurd.
+
+falso : ⊥
+falso = Δ∉Δ (x∉x→x∈Δ Δ∉Δ)

test/Fail/Issue5706.err

@@ -0,0 +1,5 @@
+Issue5706.agda:31,3-6
+Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₆ is not less or equal than Set
+when checking that the type
+(X : Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅) → (X → SET) → SET of the constructor
+set fits in the sort Set of the datatype.