[Agda] type check performance

[Sergei Meshveliani]

On Tue, 2017-01-10 at 11:42 +0100, Nils Anders Danielsson wrote:
> 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.
> 


Nice example. Thank you.
I tried Agda-2.5.2 on 
 f :  {A : Set} → A → A
 f =  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘
      id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id

It type-checks it in a moment.

------
Sergei