_/=_ generates incorrect `iEq…`

[naucke]

not0 : Int → Bool
not0 n = n /= 0
{-# COMPILE AGDA2HS not0 #-}

generates

import qualified Prelude ((/=))

not0 :: Int -> Bool
not0 n = (Prelude./=) iEqInt n 0

where iEqInt is an instance from our Haskell.Prim.Eq, not a Haskell function, and, importing Prelude qualifiedly breaks all mentions to it (such as Int and Bool from that generated snippet)

[jespercockx]

The problem here is that the definition of the Eq record in the Haskell.Prelude is wrong: the _/=_ should be defined either as a field or as a standalone function, but here it is defined as a function nested in a record type.

Normally we have a check that forbids such functions, but here we use an existing-class pragma which circumvents that check. Ideally we should also throw an error when compiling a record to a (new or existing) class and that record type has functions in its body, but for now we can just fix the immediate error in the Haskell.Prelude.