idris-lang/Idris-dev — pull request #813 by david-christiansen (2014-01-29 17:16:18+00:00)
Title: Fix error in Java name mangling

The name mangler was creating invalid names, which were truncated,
leading to collisions for test038.

Additionally, more potential collisions are fixed by padding digit codes
to a common length, so that identifiers containing numbers don't clash
with different-length character codes.

This fixes #811. I'm submitting a separate PR in case error-reflection doesn't get merged later.