Origin of type errors

[abooij]

The error message for type checking errors, while correct, is rather unhelpful in bigger proofs. It would be nice if it could at least state a line number where things go haywire.

It looks like this data is not exposed by bnfc, so we'd have to prepend position to every token. Or is there a less invasive solution?

[mortberg]

Yes, I think our error messages are pretty bad overall. Also, the REPL just crashes sometimes when you input something which it cannot parse. However our main priority at the moment is to document and check the correctness of the system, so we don't really have time to improve the interface at the moment... However, it would be very welcome if someone made a pull request improving these kind of things. :)