[Agda] help avoiding space leak using strict evaluation

[Martin Stone Davis]

I'm trying to use strict evaluation to avoid getting a space leak but my 
attempt fails: the below code blows-up the memory. (This question is a 
follow-up to a discussion in agda issue #2161 
<https://github.com/agda/agda/issues/2161>).

--

open import Agda.Builtin.Strict

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = primForce x f

open import Agda.Builtin.Nat
      using (zero; suc; Nat)
open import Agda.Builtin.Equality
      using (_≡_; refl)

id : {A : Set} → A → A
id x = x

data Nat' : Set where
   zero : Nat'
   suc : Nat' → Nat'

foo : Nat' → Nat'
foo zero = zero
foo (suc b) = suc (id b)

fooBy : Nat → Nat' → Nat'
fooBy zero x = x
fooBy (suc n) x = fooBy n $! foo x

test : fooBy 10000000 (suc zero) ≡ suc zero
test = refl

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160902/8efbaf18/attachment.html