Derived Ord instances do a weird substitution

[Lysxia]

Input:

data F a = G a a deriving (Eq, Ord)

In the definition of (<) (Ord__F_op_zl__), the comparison for the first field should use GHC.Base.compare but instead it uses Ord__F_compare:

Local Definition Ord__F_compare {inst_a} `{GHC.Base.Ord inst_a}
   : F inst_a -> F inst_a -> comparison :=
  fun a b =>
    let 'G a1 a2 := a in
    let 'G b1 b2 := b in
    match (GHC.Base.compare a1 b1) with
    | Lt => Lt
    | Eq => (GHC.Base.compare a2 b2)
    | Gt => Gt
    end.

Local Definition Ord__F_op_zl__ {inst_a} `{GHC.Base.Ord inst_a}
   : F inst_a -> F inst_a -> bool :=
  fun a b =>
    let 'G a1 a2 := a in
    let 'G b1 b2 := b in
    match (Ord__F_compare a1 b1) with
    | Lt => true
    | Eq => (a2 GHC.Base.< b2)
    | Gt => false
    end.

[lastland]

It seems that this is what GHC derives. Using GHC 8.4.3 with -ddump-deriv gives me:

(GHC.Classes.<) a_a3rDu b_a3rDv
  = case a_a3rDu of {
      Ghci1.G a1_a3rDw a2_a3rDx
        -> case b_a3rDv of {
             Ghci1.G b1_a3rDy b2_a3rDz
               -> case (GHC.Classes.compare a1_a3rDw b1_a3rDy) of
                    GHC.Types.LT -> GHC.Types.True
                    GHC.Types.EQ -> (a2_a3rDx GHC.Classes.< b2_a3rDz)
                    GHC.Types.GT -> GHC.Types.False } }

[Lysxia]

The problem is that GHC.Classes.compare got replaced with Ord__F_compare, so the Coq code doesn't even typecheck.

[lastland]

I see. That's a weird problem indeed!

[lastland]

Maybe the problem comes from here:

hs-to-coq/src/lib/HsToCoq/ConvertHaskell/Declarations/Instances.hs

Lines 253 to 264 in b88b3d5

	-- In the translation of meth1, we want all _other_ methods to be renamed
	-- to the concrete methods of the current instance (because type class methods
	-- usually refer to each other).
	-- We don’t do this for the current method (because type class methods are usually
	-- not recursive.)
	-- This is a heuristic, and the user can override it using `rewrite` rules.
	let envFor :: Qualid -> r -> r
	envFor meth = appEndo $ foldMap Endo
	[ edits.renamings.at (NamespacedIdent ns m) ?~ localNameFor m
	| m <- classMethods
	, m /= meth
	, let ns = if m `elem` classTypes then TypeNS else ExprNS]

Right now, hs-to-coq doesn't have the necessary type instance resolution information to reliably detect whether the compare is a reference to its own class or to other classes, so a heuristic is used. This is one of the places the heuristic fails. A workaround is using the redefine edit or rewrite edit:

in Deriv.Ord__F_op_zl__ rewrite forall , Deriv.Ord__F_compare = GHC.Base.compare