idris-lang/Idris-dev — pull request #1258 by bmsherman (2014-05-26 22:02:47+00:00)
Title: Fix possible bug in alpha conversion

The function `uniqueBinders` in `Idris.Core.TT` is behaving differently than I expected. I expected that if `term :: TT Name` has uniquely named binders, then for any list of names to avoid, `names :: [Name]`, we should have that `uniqueBinders names term :: TT Name` should still have uniquely named binders.

However, if we have a term `(a1 : Type) -> (a2 : Type) -> Type`, and we avoid the names `[a1,a2]`, then uniqueBinders ends up giving `(a3 : Type) -> (a3 : Type) -> Type`. With my pull request, the result will instead be `(a3 : Type) -> (a4 : Type) -> Type`.

I can't say with certainty that my change is correct (partially because there is no documentation saying what `uniqueBinders` *should* do), but I thought I'd bring this up.

I haven't even compiled this change yet! I will do so and run the tests soon.