[Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]

[Nils Anders Danielsson]

On 2020-08-25 12:49, András Kovács wrote:
> However, this uniqueness is only about unification, but that's just
> one part of elaboration. There is also a degree of freedom in deciding
> where to insert implicit applications and lambdas, and Agda's choice
> of insertions is not really unique.

Example:

   id : {A : Set} → A → A
   id x = x

   f : ?
   f = id

What is the elaborated right-hand side of f? Is it "id" or
"id {A = <something>}"?

> In general, I think it's practically realistic to have unification
> which produces unique solutions, but not that realistic to have
> elaboration which produces unique output.

Can you elaborate on this?

-- 
/NAD