[Agda] type check performance

[Nils Anders Danielsson]

On 2017-01-11 19:46, Sergei Meshveliani wrote:
> Here the size of the type expression grows 2 times with each adding of
> `id'.
>
> Probably this expense in unavoidable.

No, it can be avoided. See the first page of the paper from which I took
the example: "Implementing Typed Intermediate Languages" by Shao, League
and Monnier (https://doi.org/10.1145/289423.289460). The basic idea is
to store the terms more compactly.

-- 
/NAD