safe_krivine.idr

module Expr
import Data.Vect
import Data.Fin

data Expr : Nat -> Type where
  Var : Fin n -> Expr n
  Lam : Expr (S n) -> Expr n
  App : Expr n -> Expr n -> Expr n

data Closure : Type where
  Close : Expr n -> Vect n Closure -> Closure

k : Expr 0 -> Closure
k e = k' (Close e Nil, []) where
  k' : (Closure, List Closure) -> Closure 
  k' (Close e env, s) = case e of
    Var i => k' (index i env, s)
    App m n => k' (Close m env, Close n env::s)
    Lam b  =>  case s of
      [] => Close e env
      (arg::s') => k' (Close b (arg::env), s')

Shouldn't the App case of k' push n('s closure) to the stack before recursing?

That's embarrassing! Thanks for catching that.