Implicit lambda insertion with deBruijn

[atennapel]

Checking an explicit lambda against an implicit pi means we can insert an implicit lambda:

\y. e : t2  ~>  tm
-------
\y. e : {x : t1} -> t2  ~>  \{x : t1}. tm

But given the following example: \x y. x : {a : *} -> a -> {b : *} -> b -> a, this may not work out correctly when working with deBruijn indeces. It seems like you have to shift up the \y. e before checking against t2 or else the indeces do not point to the right type in the environment. Is there any way around this shifting?

[atennapel]

Looking at https://github.com/AndrasKovacs/smalltt/blob/master/src/Elaboration.hs I see that NOInserted will cause the variable lookup to skip inserted entries.

[AndrasKovacs]

Yes, that's how it works, but note that raw syntax never contains indices, because users write names in programs. Shifting raw syntax is not a defined operation, nor renaming/substitution on raw syntax.

[atennapel]

Interesting. I was converting from the surface level syntax with names to deBruijn syntax before elaboration, but I see you perform elaboration on the syntax with names, using a NameTable to map names to indeces. I will have to try that approach as well.