[Agda] How does unification work?

[Nils Anders Danielsson]

On 01/09/2019 16.44, Erik Palmgren wrote:
> My new colleague Anders Mörtberg mentioned that in cubicaltt there is
> a check for identical terms that can speed up unifications.
> 
> Could it possible to implement his trick in standard Agda?

This trick is implemented in Agda (you can turn it off using
--no-syntactic-equality). In this case I suppose that the problem is
that one or more implicit arguments are not syntactically equal.

-- 
/NAD