<br><div class="gmail_quote">On Tue, Sep 28, 2010 at 6:05 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
I looked at the Agda type checker and want to add some clarifications here:<br>
<br>
- Bidirectional type checking: Agda does not do bidirectional checking (= type checking and type inference), it only does type checking, where checking against a metavar has similar results to type inference. Still, bidirectional type checking is a metaphor that explains some of Agda's behavior.<br>
<br>
As Nisse already pointed out, typed and untyped lambdas are treated differently.<br>
<br>
\ x -> t expects to be checked against a function type. If it does not get a function type (e.g., it is checked against a meta variable, the type checking problem is postponed, but no constraint is propagated that the type of \ x -> t must be a function type).<br>
This explains the failure of Alan's term x1.<br>
<br>
\ (x : A) -> t synthesizes a function type (x : A) -> ?B where the new meta-var is the type of t<br>
@Thorsten: Thus, not all metavars come from holes in the input!<br>
<br>
Thus, \ (x : _) and \ x behaved differently, which is unexpected and confusing to the outsider. As we have seen by Alan's examples, there are cases where \ (x : _) works and \ x not. Can it also be the other way round?<br>
<br>
@Ulf: Could \x be treated as \(x : _) ? There seems to be some abandoned code "forcePi" that tried to do this...<br></blockquote><div><br></div><div>I can't actually remember why they're treated differently. You could always change it and see if all the tests pass.</div>
<div><br></div><div>/ Ulf</div></div>