idris-lang/Idris-dev — pull request #1753 by david-christiansen (2014-11-28 05:40:05+00:00)
Title: A new primitive tactic for getting source locations

The tactic sourceLocation fills the hole with the current location in
the file. If such information is unavailable, it fails.

This is to be used by DSL implementers to provide useful error
messages that can't be caught at type-check time. Additionally, it may
prove useful for debugging and assertion libraries, so they can report
errors.

Because the tactic merely fills out an implicit argument in a particular
way, it doesn't break referential transparency, at least not of the core
language. This is similar to the technique used in Scala Virtualized.