[Agda] Identifying inefficiency

[Martin Escardo]

It seems that indeed I am.

Instead of functors, like you, I am composing equivalences. And I have 
the composition of three equivalences, twice, with the two possible 
associations.

For the moment, I have solved this by making "abstract" the function 
that composes two equivalences. This brings down the time from 31s to 3s 
for the module under discussion.

But I will look at the link you gave, as it does seem to be the same 
kind of situation.

Thanks!

Martin

On 26/03/2019 16:42, kahl at cas.mcmaster.ca wrote:
> On Tue, Mar 26, 2019 at 03:33:11PM +0000, Martin Escardo wrote:
>> (I tried supplying all the implicit arguments to the RHS's, but the 30s
>> time remains the same.  At the holes, the types of the subterms of the
>> terms that I want to fill the holes with is known, so I am not sure what
>> is going on. But I guess this is a different question from the one in
>> this thread.)
> 
> Perhaps you are in the kind of situation that I frequently encounter,
> see https://github.com/agda/agda/issues/1625 .
> 
> I haven't tried Andrea's patch at
> 
>    https://github.com/agda/agda/issues/1625#issuecomment-132196576
> 
> in a while, but it worked wonders for some developments that would
> otherwise have been impossible to typecheck.
> 
> 
> Wolfram
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe