GND is subtly broken w.r.t. higher-rank kinds

The following program ought to compile:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Coerce
import Data.Kind
import Data.Type.Equality

class HTestEquality (f :: forall k. k -> Type) where
  hTestEquality :: forall k1 k2 (a :: k1) (b :: k2).
                   f a -> f b -> Maybe (a :~~: b)
newtype T :: (forall k. k -> Type) -> (forall k. k -> Type) where
  MkT :: forall (f :: forall k. k -> Type) k (a :: k). f a -> T f a

deriving instance forall (f :: forall k. k -> Type).
                  HTestEquality f => HTestEquality (T f)

Unfortunately, it doesn't. Here is what happens if you try to compile this with GHC HEAD:

$ ~/Software/ghc5/inplace/bin/ghc-stage2 -ddump-deriv Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

==================== Derived instances ====================
Derived class instances:
  instance forall (f :: forall k. k -> *).
           Bug.HTestEquality f =>
           Bug.HTestEquality (Bug.T f) where
    Bug.hTestEquality
      = GHC.Prim.coerce
          @(f_a12D k1_a11H a_a11J
            -> f_a12D k2_a11I b_a11K
               -> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K))
          @(Bug.T f_a12D k1_a11H a_a11J
            -> Bug.T f_a12D k2_a11I b_a11K
               -> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K))
          (Bug.hTestEquality @f_a12D) ::
          forall (k1_a11H :: TYPE GHC.Types.LiftedRep)
                 (k2_a11I :: TYPE GHC.Types.LiftedRep)
                 (a_a11J :: k1_a11H)
                 (b_a11K :: k2_a11I).
          Bug.T f_a12D k1_a11H a_a11J
          -> Bug.T f_a12D k2_a11I b_a11K
             -> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K)
  

Derived type family instances:



Bug.hs:22:1: error:
    • Expected kind ‘k4 -> *’, but ‘T f k1’ has kind ‘*’
    • In an expression type signature:
        forall (k1 :: TYPE GHC.Types.LiftedRep)
               (k2 :: TYPE GHC.Types.LiftedRep)
               (a :: k1)
               (b :: k2).
        T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
      In the expression:
          coerce
            @(f k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
            @(T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
            (hTestEquality @f) ::
            forall (k1 :: TYPE GHC.Types.LiftedRep)
                   (k2 :: TYPE GHC.Types.LiftedRep)
                   (a :: k1)
                   (b :: k2).
            T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
      In an equation for ‘hTestEquality’:
          hTestEquality
            = coerce
                @(f k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
                @(T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
                (hTestEquality @f) ::
                forall (k1 :: TYPE GHC.Types.LiftedRep)
                       (k2 :: TYPE GHC.Types.LiftedRep)
                       (a :: k1)
                       (b :: k2).
                T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
      When typechecking the code for ‘hTestEquality’
        in a derived instance for ‘HTestEquality (T f)’:
        To see the code I am typechecking, use -ddump-deriv
   |
22 | deriving instance forall (f :: forall k. k -> Type).
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Yikes! There are actually two different (but related) things going wrong here:

1. The first visible type argument to coerce is f k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b), but this really ought to be f @k1 a -> f @k2 b -> Maybe ((:~~:) @k1 @k2 a b) instead. The reason this happens is because HsUtils.typeToLHsType (which powers GeneralizedNewtypeDeriving's code generation) doesn't take visibility into account properly when dealing with AppTys like AppTy (AppTy f k1) a.
2. The second visible type argument to coerce is T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b), but this really ought to be T f @k1 a -> T f @k2 b -> Maybe ((:~~:) @k1 @k2 a b) instead. This one is a bit more perplexing, but some digging has revealed that Type.fun_kind_arg_flags is the culprit. Namely, fun_kind_arg_flags simply isn't equipped to deal with kind that have nested foralls like (forall k. k -> Type) -> (forall k. k -> Type), and if it does encounter such a kind, it bails out and incorrectly claims that all arguments are required.

Both of these buglets are quite straightforward to fix. Patch incoming.