<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>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 <a
href="https://github.com/agda/agda/issues/2161">agda issue #2161</a>).</p>
<p>--<br>
</p>
<p>open import Agda.Builtin.Strict<br>
<br>
infixr 0 _$!_<br>
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B
x<br>
f $! x = primForce x f<br>
<br>
open import Agda.Builtin.Nat<br>
using (zero; suc; Nat)<br>
open import Agda.Builtin.Equality<br>
using (_≡_; refl)<br>
<br>
id : {A : Set} → A → A<br>
id x = x<br>
<br>
data Nat' : Set where<br>
zero : Nat'<br>
suc : Nat' → Nat'<br>
<br>
foo : Nat' → Nat'<br>
foo zero = zero<br>
foo (suc b) = suc (id b)<br>
<br>
fooBy : Nat → Nat' → Nat'<br>
fooBy zero x = x<br>
fooBy (suc n) x = fooBy n $! foo x<br>
<br>
test : fooBy 10000000 (suc zero) ≡ suc zero<br>
test = refl<br>
<br>
</p>
</body>
</html>