idris-lang/Idris-dev — pull request #1252 by ziman (2014-05-22 12:15:26+00:00)
Title: Fix "unknown reference: k" in erasure analysis

This patch makes the usage analysis remember names of de Bruijn variables to also cover the cases where a let-bound or a lambda-bound variable is referred to as `P _ n _`, not `V i`.

This should fix #1250. Since I can't reproduce it, it's hard to test. However, all the tests do pass.