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

[Conor McBride]

Hi Nisse

On 30 Sep 2010, at 16:36, Nils Anders Danielsson wrote:

> 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?

In a sense, yes. But that's really not the picture.

It's not a question of writing out and then checking the candidates
for the implicit arguments in full. It is perfectly possible to equip
the evidence (I no longer find any meaning in the word "core") language
with metavariables, and thus to typecheck the inference *problem*,
then incrementally check the definitions resulting from solving
constraints. It is not merely unnecessary but backward to wait until a
fully elaborated and substituted-out term has materialised before
invoking the typechecker. For one thing, it is helpful to solve
constraints in the presence of accurate type information.

You can call that "careful use of lets" if you like, but it's far more
systematic than that phrasing suggests. Extensional equality also
allows us to capture type equality constraints as unsolved goals, just
like anything else. Right enough, it helps to solve those goals sooner
rather than later.

But the point is this: we solve constraints after typechecking, not
before.

All the best

Conor