[Agda] type check performance

[Nils Anders Danielsson]

On 2017-01-08 20:20, Sergei Meshveliani wrote:
> He said that the only source of an unnatural type check cost with Coq
> can be not of the language/compiler/interpreter itself, but due to
> unlucky usage of proof _tactics_ in the user program.

Consider the following Coq code (which is based on an example in
"Implementing Typed Intermediate Languages" by Shao, League and
Monnier):

   Definition id {A : Set} (x : A) : A := x.

   Definition slow {A : Set} : A -> A :=
     id id id id id id id id id id id id id id id id id id.

The time required to check this code using Coq 8.4pl4 seems to be
roughly exponential in the number of occurrences of "id" on the last
line [*], and as far as I can tell the code does not use a single
tactic.

[*] With enough occurrences of "id" Coq complains about stack overflows,
so I guess that the code isn't actually checked.

-- 
/NAD