Try:

```agda
f : {ℕ} → ℕ
f {n} = n
```

In general, writing lambdas directly can be brittle, because Agda can be (over-)eager to introduce implicits, so this is one to watch out for. Writing definitions in 'pattern-matching' style offers slightly more fine-grained control.