Update Agda base to 2.7.0

[jespercockx]

Closes #349

[jespercockx]

There is a regression in issue #305: the instances from parametrized modules are no longer available in the instance table when we do the canonicity check. This seems to be caused by the new implementation of instance search in agda/agda#7109, specifically the optimization that deletes instances with explicit arguments from the signature before writing the interface file in https://github.com/agda/agda/blob/8b37dbf89978b46b360b2127d2d2aa9e60fe56ad/src/full/Agda/TypeChecking/InstanceArguments.hs#L1070-L1098
Indeed, the test case Issue305.agda is accepted by agda2hs when using --ignore-interfaces.

On the one hand, I understand that having instances that cannot possibly be used in other files is wasteful and thus it makes sense to remove them. On the other hand, I do not know of a good way for a backend like agda2hs to "go back" to the typechecking state with which a specific term was typechecked, which we do need here to properly check canonicity.

Perhaps the right solution would be to add some additional hooks to the backend machinery so that the backend can add additional checks during typechecking/elaboration itself. However, that's not something we cannot do without some major changes to Agda.

[jespercockx]

I've been trying to fix this by rolling a manual canonicity check for instances so we don't have to rely on Agda's instance search being able to re-infer the instances during compilation. In theory, this should not be hard: an instance is canonical if it is either a top-level definition/constructor marked as instance or a local variable introduced as an instance argument; and in either case all the instance arguments to the symbol should be canonical themselves.

However, agda/agda#7449 throws soot in the food (sorry for the Dutchism): the instance arguments that appear in the internal syntax are actually not the terms as constructed by instance search, but their whnf. For instances defined directly using copatterns, this does not matter. However, in the agda2hs standard library we define a lot of instances through helper functions such as:

• foldMap= and mkFoldable (for Foldable)
• fmap= and mkFunctor (for Functor)
• bind= (for Monad)
• mempty= and mkMonoid (for Monoid)
• ordFromCompare, ordFromLessThan, and ordFromLessEq (for Ord)
• unboundedEnumViaInteger, boundedBelowEnumViaInteger, boundedAboveEnumViaInteger, boundedEnumViaInteger (for Enum)
• possibly more that I haven't got to yet

For the first five items on this list, I could replace the current definitions in the agda2hs Prelude with alternatives that pass the simple canonicity check I outlined above, even when they are reduced. However, for the Enum helpers I failed so far to see a good way, due to the complexity of this class (with many private type definitions in the record itself). I'll continue to try, but if someone has another suggestion for an easier solution please let me know.

[jespercockx]

Weird, the Nix build seems to fail:

agda2hs> [ 8 of 23] Compiling Agda2Hs.Compile.Name ( src/Agda2Hs/Compile/Name.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Name.o )
agda2hs> src/Agda2Hs/Compile/Name.hs:101:41: error: [GHC-83865]
agda2hs>     • Couldn't match expected type ‘RecordData’ with actual type ‘Defn’
agda2hs>     • In the first argument of ‘_recNamedCon’, namely ‘def’
agda2hs>       In the first argument of ‘not’, namely ‘(_recNamedCon def)’
agda2hs>       In the expression: not (_recNamedCon def)
agda2hs>     |
agda2hs> 101 |       Just (r, def) | not (_recNamedCon def) -> r -- use record name for unnamed constructors
agda2hs>     |                                         ^^^

I don't have Nix so I cannot reproduce it locally. Could anyone who uses Nix take a look?

[jespercockx]

Thanks to some help from @liesnikov the Nix build has been fixed. We should investigate whether we can remove the jailbreak from nix.flake so this problem doesn't happen again in the future. Currently this is not possible due to the constraint >= 2.2 on the aeson package (cc @flupe who added that dependency). Either way, this is good to go now.

[flupe]

Yes tbf at the time I put >= 2.2 as the most conservative choice since it was the most recent version, we can probably relax the contraint (by a lot).