idris-lang/Idris-dev — pull request #1360 by ziman (2014-07-06 00:57:29+00:00)
Title: Make case elaboration respect dots

The problem shown [here](https://gist.github.com/ziman/10458331) stems from the fact that dotted fields of constructors were not respected by case elaboration. This patch fixes this and now case elaboration tries to avoid dotted fields.

The patch includes:
* instead of `State CS`, case tree building now happens in the `CaseBuilder` monad (which adds a `ReaderT` layer with information about accessibility)
* `toPat` no longer replaces repeated pattern variables with `PAny`, which also allowed us to get rid of the state monad there
* `argsToAlt` returns not only the list of new variables but also distinguishes between accessible and inaccessible patvars

All tests pass on both machines of mine and my test programs now exhibit correct dot avoidance.