[Agda] Implicit variables on data constructors

[Simon Foster]

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.

Thanks,

-Si.