[Agda] stack overflow in Agda 2.3.2.1

[James Cranch]

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} → α > β → α ≥ β