agda2hs cannot compile Traversable instances defined with `traverse=_`

[ggrandi]

I was trying to use mapM from agda2hs and when I compiled it I am getting the output:

agda2hs failed:
<...>: error: [CustomBackendError]
agda2hs:
  illegal instance:  Haskell.Prim.Traversable.traverse=
                     Haskell.Prim.Traversable.traverseList

The code I got it to fail on was as follows:

usingMapM : Maybe (List Nat)
usingMapM = mapM pure []

{-# COMPILE AGDA2HS usingMapM #-}

The other thing that confused me is that when I inlined the definition of traverse=_ into iTraversableList in lib/base/Haskell/Prim/Traversable.agda to

   iTraversableList : Traversable List
-  iTraversableList = traverse= traverseList
+  iTraversableList = record {DefaultTraversable (record {traverse = traverseList})}

without making any other changes it seemed to work.

I am not quite sure what is going on so I wanted to make an issue since I think this might happen again in other places where there is a record created from a default record with a helper (I don't think there are any other instances of it within base).

[jespercockx]

Ah, I think this is a consequence of the "new" way we check for validity of instances (see #354). It seems these instances have not seen a lot of testing, unfortunately.

With the new (simpler but more robust check) it's no longer possible to use helper functions in this way to construct instances, they should instead be defined using copatterns or using a default instance. You'll note that in that PR I already got rid of a lot of these helper functions, but it seems that I've missed the traverse= function. So your fix inlining the definition of traverse= looks correct to me.