{-

A version of

https://github.com/agda/agda/issues/3026

-}

{-# OPTIONS
  --no-guardedness
  --no-subtyping
  --no-universe-polymorphism
  --safe
  --sized-types
  --without-K #-}

module size-bug where

open import Agda.Builtin.Size

----------------------------------------------------------------------
-- Empty type
----------------------------------------------------------------------
data ⊥ : Set where

----------------------------------------------------------------------
-- Well-founded relations
----------------------------------------------------------------------
data Acc
  {A : Set}
  (R : A → A → Set)
  (x : A)
  : -----------------
  Set
  where
  acc : (∀ y → R y x → Acc R y) → Acc R x

isWellFounded :
  {A : Set}
  (R : A → A → Set)
  → -----------------
  Set
isWellFounded R = ∀ x → Acc R x

----------------------------------------------------------------------
-- The < relation between sizes is well-founded
----------------------------------------------------------------------
data _<_ : Size → Size → Set where
  <proof : {i : Size}{j : Size< i} → j < i

<wf : isWellFounded _<_
<wf i = acc λ j → λ where <proof → <wf j

----------------------------------------------------------------------
-- But ∞ < ∞, so we get a contradiction :-(
----------------------------------------------------------------------
∞<∞ : ∞ < ∞
∞<∞ = <proof

∞notAcc : Acc _<_ ∞ → ⊥
∞notAcc (acc f) = ∞notAcc (f ∞ ∞<∞)

contradiction : ⊥
contradiction = ∞notAcc (<wf ∞)