[Agda] stack overflow in Agda 2.3.2.1

[Fredrik Nordvall Forsberg]

Hi James,

> 1. Am I doing something wrong?

You are defining

  Cantor : Set
  Cantor = OList {A = Cantor} _≥_

(I have made the implicit argument A = Cantor explicit) which the
termination checker rightfully complains about (using the development
version of Agda). My guess is that 2.3.2.1 for some reason is trying
to unfold the expression

  Cantor = OList {A = Cantor} _≥_ = OList {A = OList {A = Cantor} _≥_} _≥_ = ...

until it runs out of stack.

If you instead make Cantor isomorphic to OList {A = Cantor} _≥_, i.e.
define

  data Cantor : Set where
    cnf : OList {A = Cantor} _≥_ → Cantor

and insert the iso and its inverse

  uncnf : Cantor → OList _≥_
  uncnf (cnf x) = x

in appropriate places, the file is type and termination
checked for me using the development version of Agda.
I have included the modified file below.

Hope that helps,
Fredrik

--------------------------------------------------


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.
  data Cantor : Set where
    cnf : OList {A = Cantor} _≥_ -> Cantor

  data _>_ : (α β : Cantor) → Set where
    >-zero : {h t : Cantor} (e : h ▷ uncnf t) → cnf (cons e) > cnf nil
    >-now : {h₁ h₂ t₁ t₂ : Cantor} (e₁ : h₁ ▷ uncnf t₁) (e₂ : h₂ ▷ uncnf t₂) → h₁ > h₂ → cnf (cons e₁) > cnf (cons e₂)
    >-later : {h t₁ t₂ : Cantor} (e₁ : h ▷ uncnf t₁) (e₂ : h ▷ uncnf t₂) → t₁ > t₂ → cnf (cons e₁) > cnf (cons e₂)

  data _≥_ : (α β : Cantor) → Set where
    ≥-equal : (α : Cantor) → α ≥ α
    ≥-diff : {α β : Cantor} → α > β → α ≥ β

  uncnf : Cantor -> OList _≥_
  uncnf (cnf x) = x


--------------------------------------------------


On 15/08/13 14:33, James Cranch wrote:
> 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} → α > β → α ≥ β