Open bwbush opened 5 months ago
So the problem here seems to be that Agda itself eta-contracts MakeHask (hashBytes x)
to x
, even when the parameters of the constructor and the projection are different, possibly caused by https://github.com/agda/agda/issues/2732. I'm not sure if there is much we can do to fix this on the agda2hs side. As a workaround, you could add a no-eta-equality
clause to the record definition, which should be enough to stop Agda from eta-contracting.
Perhaps we should just enforce that records that are compiled to Haskell data types always have eta-equality disabled.
Agda
becomes Haskell
even though
MakeHash . hashBytes != id
since in this case we hadMakeHash :: ByteString -> Maybe a
buthashBytes :: () -> ByteString
etc.