<br><div class="gmail_quote">On Wed, Jul 13, 2011 at 10:58 AM, Simon Foster <span dir="ltr">&lt;<a href="mailto:s.foster@dcs.shef.ac.uk">s.foster@dcs.shef.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

<div class="im">On Tue, 2011-07-05 at 15:52 +0200, Ulf Norell wrote:<br>
<br>
&gt; They&#39;re not actually present in the internal syntax. Implicit<br>
&gt; arguments to functions are stored in the internal syntax, but the<br>
&gt; datatype parameters are not stored as arguments to constructors. The<br>
&gt; reason for this is that they are uniquely determined by the type of<br>
&gt; the constructor application. Of course, we really ought to use that<br>
&gt; when going back to abstract syntax and put the correct term there.<br>
<br>
</div>Ok, so is it possible to infer the type of [] (the empty-list) from the<br>
type-checking context somehow? This (and other nullary constructors) is<br>
still proving problematic, as for others (e.g. _::_) I can usually<br>
figure out the type based on the parameters. I has a play around with<br>
InternalToAbstract, but couldn&#39;t figure out how to solve it in the<br>
former case as I&#39;m still getting meta-variables.<br></blockquote><div><br></div><div>You have to carry the type around to reconstruct the parameters.</div><div>InternalToAbstract doesn&#39;t do this at the moment.</div>

<div><br></div><div>/ Ulf</div></div>