[Agda] Implicit variables on data constructors

[Ulf Norell]

On Tue, Jul 5, 2011 at 3:08 PM, Simon Foster <s.foster at dcs.shef.ac.uk>wrote:

> Hi,
>
> A slightly technical question about the Agda core - why do (some?) implicit
> variables which are applied to a data constructor get converted into
> anonymous meta-variables when converting from the internal syntax to the
> abstract syntax? e.g. If I have a function
>
> ++-rzero : ∀ {A : Set} → (xs : List A) → xs ++ [] ≡ xs
>
> and ask for the type of ++-rzero {A} I get shown
>
> (x : A) (xs : List A) → _≡_ {List A} (_∷_ {_} x xs) (_∷_ {_} x xs)
>
> I assume this is down to the "whocares" assignment in
> InternalToAbstract.hs, because AFAICS the variables are represented
> explicitly in the internal syntax (i.e. when I do inferExpr on the name of
> ++-rzero).
>

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.

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