idris-lang/Idris-dev — pull request #1763 by ziman (2014-12-04 16:55:31+00:00)
Title: Define `Show` instance for `Vect` via `toList`

Nicola Botta has got a program whose runtime went from 11 to 42 seconds when we merged erasure. This is mostly caused by a single one wrong case tree generated from the `Show` instance for vectors, which inspect the length index, which in turn cannot be erased in the whole program.

Since it seems that the proper fix is non-trivial, let us use a workaround for now.