New (simpler but more robust) implementation of canonicity check

[jespercockx]

This is an attempt to resolve the issue with the canonicity check that I encountered in #350 by implementing it in a completely different way. Instead of re-inferring the instance and checking it for equality with the given one, we instead traverse the term and check that its head symbol is an instance (either a global instance Def or a local instance Var), and that all its recursive instance arguments are canonical too.

Due to the upstream issue agda/agda#7449, this has the annoying effect that instances need to be given in a form that does not reduce unless projected, or if they reduce then the reduct should be a valid instance itself. This should not be a problem for user-written instances, but for the instances in the Prelude it means we cannot make use of most of the tricks that were there to avoid boilerplate. Instead, I just bit the bullet and made the code in it quite a bit more verbose in order to make it pass the new canonicity check.

Happy to get feedback on the general idea as well as the implementation details.

[flupe]

With regards to instances being inlined, can this be prevented by annotating with {-# NO_INLINE #-}? Alternatively, since mkApplicative was marked as private, we could assume that all uses of mkApplicative in instance arguments must arise from instance search, so we could hardcode these helpers from the prelude to be fine (TM) though I get why this would be annoying.

This should not be a problem for user-written instances.

It would be if we wanted to use the same kind of tricks for a custom class, right?

Regardless, nice!

[jespercockx]

With regards to instances being inlined, can this be prevented by annotating with {-# NO_INLINE #-}?

That doesn't help as the terms are actually reduced to whnf, on which NO_INLINE has no effect.

since mkApplicative was marked as private, we could assume that all uses of mkApplicative in instance arguments must arise from instance search, so we could hardcode these helpers from the prelude to be fine (TM)

Yeah in hindsight perhaps this would've been easier. But now the work is done anyway.

It would be if we wanted to use the same kind of tricks for a custom class, right?

These tricks would not be accepted for instances that are actually compiled to Haskell. However, it could be a problem if a user wants to mirror instances that already exist in Haskell on the Agda side.

[jespercockx]

Since there are no objections I will merge this now, so we can continue to update the Agda base version to 2.7.0.