[Agda] type check performance

[Martin Escardo]

On 08/06/18 11:04, nad at cse.gu.se wrote:
> On 2018-06-08 10:21, Martin Escardo wrote:
>> In my case, Agda 2.5.3 is faster than 2.5.4.
>>
>> Typechecking [1] takes respectively 43 and 48 seconds (12% more) in 
>> the same laptop.
>>
>> (NB. I tried 2.5.3 with --no-sharing, and then I get a unification 
>> failure in [2].)
> 
> I could typecheck your code [1] using Agda 2.5.3 without enabling
> sharing.

Right. I meant that with --sharing I get an error - sorry. Namely
"
/home/mhe/TypeTopology/source/UF-Equiv.lagda:325,57-61
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
   x₁ ≟ x , _2385 f (f x) x x' refl p'
   x₁ ≟ x' , p'
Possible reason why unification failed:
   Cannot solve variable p' of type f x ≡ f x with solution
   _2385 f (f x) x x refl p' because the variable occurs in the
   solution, or in the type of one of the variables in the solution.
when checking that the pattern refl has type
x , _2385 f (f x) x x' refl p' ≡ x' , p'
"

> The outcome of a single test was that 2.5.4 was ∼3% slower.

Repeating the test a number of times, I get between a minimum of 7% and 
a maximum of 12% slower.

Martin