<br><div class="gmail_quote">On Tue, Sep 28, 2010 at 6:05 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</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&#39;s behavior.<br>

<br>
As Nisse already pointed out, typed and untyped lambdas are treated differently.<br>
<br>
  \ x -&gt; 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 -&gt; t must be a function type).<br>

 This explains the failure of Alan&#39;s term x1.<br>
<br>
  \ (x : A) -&gt; t  synthesizes a function type (x : A) -&gt; ?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&#39;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 &quot;forcePi&quot; that tried to do this...<br></blockquote><div><br></div><div>I can&#39;t actually remember why they&#39;re treated differently. You could always change it and see if all the tests pass.</div>
<div><br></div><div>/ Ulf</div></div>