hs-to-coq translates GeneralizedNewtypeDeriving instances incorrectly

[nosewings]

As of GHC 8.10.7, the base library contains type class instances generated via GeneralizedNewtypeDeriving. Given newtype X a = X a, a type class C e with a method f :: t gets translated like

instance C a => C (X a) where
  f = GHC.Prim.coerce (f) :: t'

where t' is obtained by substituting X a for e in t.

For example, the following code:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype Ap f a = Ap { getAp :: f a }
  deriving (Functor)

generates the following instance:

instance GHC.Base.Functor f => GHC.Base.Functor (Main.Ap f) where
  GHC.Base.fmap
    = GHC.Prim.coerce
        @((a_agZ -> b_ah0) -> f_agj a_agZ -> f_agj b_ah0)
        @((a_agZ -> b_ah0) -> Main.Ap f_agj a_agZ -> Main.Ap f_agj b_ah0)
        (GHC.Base.fmap @f_agj) ::
        forall (a_agZ :: TYPE GHC.Types.LiftedRep)
               (b_ah0 :: TYPE GHC.Types.LiftedRep).
        (a_agZ -> b_ah0) -> Main.Ap f_agj a_agZ -> Main.Ap f_agj b_ah0
  (GHC.Base.<$)
    = GHC.Prim.coerce
        @(a_ah2 -> f_agj b_ah3 -> f_agj a_ah2)
        @(a_ah2 -> Main.Ap f_agj b_ah3 -> Main.Ap f_agj a_ah2)
        ((GHC.Base.<$) @f_agj) ::
        forall (a_ah2 :: TYPE GHC.Types.LiftedRep)
               (b_ah3 :: TYPE GHC.Types.LiftedRep).
        a_ah2 -> Main.Ap f_agj b_ah3 -> Main.Ap f_agj a_ah2

The code that hs-to-coq generates for fmap looks like:

#[local] Definition Functor__Ap_fmap {inst_f : Type -> Type} `{GHC.Base.Functor
  inst_f}
   : forall {a : Type},
     forall {b : Type}, (a -> b) -> Ap inst_f a -> Ap inst_f b :=
  fun {a : Type} {b : Type} =>
    GHC.Prim.coerce (GHC.Base.fmap) : (forall {a
      : GHC.Prim.TYPE GHC.Types.LiftedRep}
     {b : GHC.Prim.TYPE GHC.Types.LiftedRep},
     (a -> b) -> Ap inst_f a -> Ap inst_f b).

But this doesn't typecheck (or, more precisely, Coq will fail to find a Coercible instance): the coerce is ascribed a fully-polymorphic type, but the type arguments have already been "eaten" by the fun construct.

The code for generating these instances is in HsToCoq.ConvertHaskell.Declarations.Instances. The fundamental problem is that this code assumes that the RHS of a typeclass instance method is never polymorphic, which is not true in this case.

In c86c82d, I implemented the "bad" solution, which is to heuristically detect methods that look like they were generated by GeneralizedNewtypeDeriving and throw away the ascription. As I see it, the "correct" solution would be to infer the type of the RHS and unify it against the method's expected type.