idris-lang/Idris-dev — pull request #1348 by david-christiansen (2014-06-30 16:50:15+00:00)
Title: Add goal types to quasiquotes.

A quasiquote expression can be given a goal type for the elaborator,
which helps with disambiguation. For instance, `(() : ()) quotes the
unit constructor, while `(() : Type) quotes the unit type. Both goal
types and quasiquote are typechecked in the global environment.