[Agda] Compile-time parsing

[Conor McBride]

On 16 Dec 2011, at 12:14, Nils Anders Danielsson wrote:

> On 2011-12-16 12:39, Conor McBride wrote:
>> PS In the presence of equality on sets, where coercion between
>> provably equal sets is definable, it is possible to replace very
>> many type errors by irredeemable metavariables, turning brown to
>> yellow.
>
> What are you referring to here?

Anywhere you have an A where you want a B, you can insert
an explicit coercion by a metavariable proof that A equals B.
The Epigram elaborator (such as it is) uses this approach to
handle the "change of direction" rule in bidirectional
checking. In that setting, there are no errors, only proof
obligations which turn out to be a bit tricky.

Cheers

Conor