idris-lang/Idris-dev — pull request #1803 by david-christiansen (2014-12-22 20:47:59+00:00)
Title: Error reflection for Fin

Add reflection-based error message improvements for Fin literals. Now, instead of a collection of internal implementation details, a friendly and descriptive message is returned.

Demo:
```idris
module error005

-- Test the Prelude's error rewrites for Fin

one : Fin 2
one = 1

two : Fin 2
two = 2

hahaha : (n : Nat) -> Fin n
hahaha n = 0

ok : (n : Nat) -> Fin (plus 2 n)
ok n = 1

notOk : (n : Nat) -> Fin (plus 2 n)
notOk n = 2
```
gives
```
error005.idr:11:1:When elaborating right hand side of two:
When elaborating argument prf to function Prelude.Fin.fromInteger:
When using 2 as a literal for a Fin 2
Could not show that 2 is less than 2
error005.idr:14:1:When elaborating right hand side of hahaha:
When elaborating argument prf to function Prelude.Fin.fromInteger:
When using 0 as a literal for a Fin n
Could not show that 0 is less than n
error005.idr:19:1:When elaborating right hand side of notOk:
When elaborating argument prf to function Prelude.Fin.fromInteger:
When using 2 as a literal for a Fin (S (S n))
Could not show that 2 is less than S (S n)
```

This did require moving the basic parts of `Language.Reflection` into `prelude`, but I think this is a good idea anyway, because it stops the quasiquote syntax from throwing bizzare unknown variable errors when the user hasn't imported them.

I don't want to merge it myself because I want @edwinb's OK to add the reflection datatype to the prelude.

Later I'll find more error messages to pretty up. This is pre-hospital work - don't worry, I'm relaxing and healing :)