[Agda] Implicit variables on data constructors

[Ulf Norell]

On Wed, Jul 13, 2011 at 10:58 AM, Simon Foster <s.foster at dcs.shef.ac.uk>wrote:

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

You have to carry the type around to reconstruct the parameters.
InternalToAbstract doesn't do this at the moment.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110713/22772838/attachment.html