[Agda] type check performance

[Stefan Monnier]

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

I think Agda's inference algorithm is sufficiently close to
Hindley-Milner that it suffers from the same DEXPTIME complexity, so
while the above example can be implemented more efficiently, there re
other cases where you can't avoid it.

But these HM pathological cases involve no reductions and are extremely
rare in real-life: you can show that the complexity of HM is not
DEXPTIME but O(N) if the size of types manipulated is bounded
by a constant; IOW you need exponential-sized types to get an
exponential slowdown.

I suspect the slow type-checking in cases such as Sergei's is due to
something else, linked to all the evaluation that happens at the type-level.


        Stefan