search

agda / agda2hs

Compiling Agda code to readable Haskell
https://agda.github.io/agda2hs
MIT License
178 stars 37 forks source link

New (simpler but more robust) implementation of canonicity check #354

Closed jespercockx closed 2 months ago

jespercockx commented 3 months ago

This is an attempt to resolve the issue with the canonicity check that I encountered in https://github.com/agda/agda2hs/pull/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 https://github.com/agda/agda/issues/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.

jespercockx commented 3 months ago

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 commented 2 months ago

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