search

agda / agda2hs

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

Definition of `Functor` is inconsistent with `base-4.18.1.0` etc. #318

Open bwbush opened 2 months ago

bwbush commented 2 months ago

The agda2hs prelude puts void as a member of the typeclass, but the latest GHC base libraries do not.

Compare void in

https://github.com/agda/agda2hs/blob/7b3e48a35448acff9bb5823ca22623eafb000d15/lib/Haskell/Prim/Functor.agda#L15-L24

and to it's top-level placement in

https://github.com/ghc/ghc/blob/f3225ed4b3f3c4309f9342c5e40643eeb0cc45da/libraries/base/Data/Functor.hs#L210-L211

The same problem occurs for several other members of Functor and for several other typeclasses.

jespercockx commented 1 month ago

Currently we are not very explicit about which version of GHC or the Haskell Prelude we support. But in this case I believe it makes sense to remove void as a field so we are compatible with the latest release at least.