[Agda] Compile-time parsing

[Conor McBride]

On 16 Dec 2011, at 10:03, Nils Anders Danielsson wrote:

> On 2011-12-15 12:35, Andres Löh wrote:
>> I don't understand completely why you're opposed to your first
>> solution. Code being highlighted in yellow *is* a (particular kind  
>> of)
>> type error in Agda. In fact, it's a particularly well-behaved kind of
>> type error from which the type checker can recover and still check  
>> the
>> rest of the program. There's no implication that yellow means "almost
>> correct" ...
>
> At the last AIM Nicolas Pouillard suggested that unsolved meta- 
> variables
> should (by default) be treated as errors. I think his main motivation
> was that type-checking can be very slow if you have an unsolved
> meta-variable at the top of a long file. What do you think of this?
>
> (I'm not sure how easy this would be to implement, given that
> meta-variables related to goals should not be treated as errors.)

How about treating as an error an unsolved meta whose type, were it an
hypothesis, would be dismissed by an absurd pattern?

Conor