How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]

[Nils Anders Danielsson]

On 2010-09-29 11:03, Conor McBride wrote:
> In Epigram 2, the plan (only partially realised so far) is
> to support implicit syntax as an elaboration convention
> outside the evidence language, rather than as a funny Pi-type
> in the language at any layer.

If you write out all the implicit arguments explicitly before running
the core type-checker, how do you handle the potential problems of code
explosion and unnecessary equality checking? Careful use of lets?

--
/NAD