[Agda] stack overflow in Agda 2.3.2.1
James Cranch
jdc41 at cam.ac.uk
Thu Aug 15 15:33:20 CEST 2013
Hi all,
Typechecking the module below causes a stack overflow for me (running Agda
2.3.2.1). I have made the stack very large (64M) and it still happens,
which suggests it's a bug: I don't think the code is all that subtle.
I hope it's readable! It's online at
http://jdc41.user.srcf.net/Overflow.agda
if not.
I guess I'm interested in answers to the following questions:
1. Am I doing something wrong?
2. (If it's a bug), will it be fixed?
3. Is there a workaround for now?
Cheers,
James
\/\/\
module Overflow where
open import Level
open import Relation.Binary
mutual
-- Verified ordered lists: we can only form a cons if we can
-- demonstrate that the head is bigger than the first element of the
-- tail.
data OList {α ℓ : Level} {A : Set α} (_>_ : Rel A ℓ) : Set (α ⊔ ℓ)
where
nil : OList _>_
cons : {h : A} {t : OList _>_} → h ▷ t → OList _>_
data _▷_ {α ℓ : Level} {A : Set α} {_>_ : Rel A ℓ} : A → OList _>_ →
Set (α ⊔ ℓ) where
▷-nil : {a : A} → a ▷ nil
▷-cons : {a b : A} {l : OList _>_} → a > b → (b▷l : b ▷ l) → a ▷
cons b▷l
mutual
-- Cantor normal form, for ordinals less than epsilon_0. An ordinal
-- in CNF consists of a sum of omega^a, taken over some ordered list
-- of a's themselves in CNF.
Cantor : Set
Cantor = OList _≥_
data _>_ : (α β : Cantor) → Set where
>-zero : {h t : Cantor} (e : h ▷ t) → cons e > nil
>-now : {h₁ h₂ t₁ t₂ : Cantor} (e₁ : h₁ ▷ t₁) (e₂ : h₂ ▷ t₂) → h₁ >
h₂ → cons e₁ > cons e₂
>-later : {h t₁ t₂ : Cantor} (e₁ : h ▷ t₁) (e₂ : h ▷ t₂) → t₁ > t₂
→ cons e₁ > cons e₂
data _≥_ : (α β : Cantor) → Set where
≥-equal : (α : Cantor) → α ≥ α
≥-diff : {α β : Cantor} → α > β → α ≥ β
More information about the Agda
mailing list