<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>