[omelkonian]

The treeless pipeline happens to introduce some that are only sound under lazy semantics, e.g. ToTreeless.updateCatchall hoists the body of a catch-all/overlapping clause above the pattern match.

That's the reason Fannkuch benchmark failed on the Agda frontend: the recursive call was placed at the start before the pattern match and under strict evaluation loops forever.

A more proper solution would be to emit actual tLazy/tForce λ-box terms, but this seems to break things downstream in Peregrine and its backends, so leave a proper lazy-evaluation solution for the future, and now settle for this naive call-by-name fix.

• The LazyForce pass of Peregrine does exactly the same:

    | tLazy t => EAst.tLambda nAnon (lift 1 0 (implement_lazy_force t))
    | tForce t => EAst.tApp (implement_lazy_force t) tBox.

• Agda's built-in JS compiler does the same:

      -- `let x = t in e` is compiled to `(x => e[x()/x])(() => t)` so that `t`
      -- is only evaluated inside the body
      T.TLet t e -> do
        t' <- Lambda 0 <$> go t
        e' <- substShift 1 1 [Apply (Local (LocalId 0)) []] <$> go e
        return $ Apply (Lambda 1 e') [t']

• @mattam82 informed me that Peregrine's OCaml/Malfunction backend properly does it justice, and actually gives a memoised implementation of tLazy/tForce.