<br><div class="gmail_quote">On Wed, Jul 13, 2011 at 10:58 AM, Simon Foster <span dir="ltr"><<a href="mailto:s.foster@dcs.shef.ac.uk">s.foster@dcs.shef.ac.uk</a>></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>
> They're not actually present in the internal syntax. Implicit<br>
> arguments to functions are stored in the internal syntax, but the<br>
> datatype parameters are not stored as arguments to constructors. The<br>
> reason for this is that they are uniquely determined by the type of<br>
> the constructor application. Of course, we really ought to use that<br>
> 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't figure out how to solve it in the<br>
former case as I'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't do this at the moment.</div>
<div><br></div><div>/ Ulf</div></div>