@[specialize]
def foo {α} : Nat → (α → α) → α → α 
  | 0, f, a => f a 
  | n+1, f, a => foo n f a

-- The following example demonstrates that `f` is properly specialized:
set_option trace.Compiler.saveBase true in
/--
trace: [Compiler.saveBase] size: 6
    def foo._at_._example.spec_0 x.1 x.2 : Nat :=
      cases x.1 : Nat
      | Nat.zero =>
        let _x.3 := 1;
        let _x.4 := Nat.add x.2 _x.3;
        return _x.4
      | Nat.succ n.5 =>
        let _x.6 := foo._at_._example.spec_0 n.5 x.2;
        return _x.6
[Compiler.saveBase] size: 2
    def _example n : Nat :=
      let _x.1 := 5;
      let _x.2 := foo._at_._example.spec_0 n _x.1;
      return _x.2
-/
#guard_msgs in
example {n} := foo n (· + 1) 5

-- The following example demonstrates that while `f` is properly specialized, `a` is not:
set_option trace.Compiler.saveBase true in
/--
trace: [Compiler.saveBase] size: 6
    def foo._at_._example.spec_0 x.1 x.2 _y.3 : Nat :=
      cases x.1 : Nat
      | Nat.zero =>
        let _x.4 := x.2 _y.3;
        let _x.5 := x.2 _x.4;
        return _x.5
      | Nat.succ n.6 =>
        let _x.7 := foo._at_._example.spec_0 n.6 x.2 _y.3;
        return _x.7
[Compiler.saveBase] size: 4
    def _example n : Nat :=
      fun _f.1 x.2 : Nat :=
        let _x.3 := 1;
        let _x.4 := Nat.add x.2 _x.3;
        return _x.4;
      let _x.5 := 5;
      let _x.6 := foo._at_._example.spec_0 n _f.1 _x.5;
      return _x.6
-/
#guard_msgs in
example {n} := foo n (fun f a => f (f a)) (· + 1) 5