Faulty rigid type variable with standalone deriving-via and PolyKind

Summary

In Ghci (and Ghci only!), a query such as

deriving via
  Generically1 (Product f g)
  instance
    (Applicative f, Applicative g) => Applicative (Product f g)

Can fail to typecheck with the following error (in GHC 9.2 it even produces a NoSkolem anomaly, I assume the anomaly has been fixed as part of !7105 (closed)):

src/Data/Functor/Linear/Internal/Applicative.hs:29:18: error:
    • Couldn't match kind ‘k’ with ‘*’
      Expected kind ‘* -> *’, but ‘f’ has kind ‘k -> *’
      ‘k’ is a rigid type variable bound by
        the deriving clause for ‘Generically1 (Product f g)’
        at src/Data/Functor/Linear/Internal/Applicative.hs:27:3-28
    • In the first argument of ‘Applicative’, namely ‘f’
      In the stand-alone deriving instance for
        ‘(Applicative f, Applicative g) => Applicative (Product f g)’
   |
29 |     (Applicative f, Applicative g) => Applicative (Product f g)
   |                  ^

A key ingredient, here, is that f is supposed to have Type -> Type, for a type class with variables of kind Type, the problem doesn't appear to show up.

It is a regression compared to GHC 9.0 [@monoidal points out that this is do to GHC 9.2 having PolyKinds enabled by default].

Steps to reproduce

Load a file with the following content in Ghci:

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Data.Functor.Linear.Internal.Applicative
  ( Applicative (..),
  )
where

import GHC.Types

-- type Product :: (Type -> Type) -> (Type -> Type) -> Type -> Type
data Product f g a = Pair (f a) (g a)

-- type Generically1 :: (Type -> Type) -> Type -> Type
newtype Generically1 f a = Generically1 (f a)

type Functor :: (Type -> Type) -> Constraint
class Functor f where
class Functor f => Applicative f where

deriving instance (Functor f, Functor g) => Functor (Product f g)

deriving via
  Generically1 (Product f g)
  -- Geneically1 (Product (f :: Type -> Type) g)
  instance
    (Applicative f, Applicative g) => Applicative (Product f g)

The bug disappears when either signature is uncommented. Or when the Generically1 (Product …) lines is replaced by the commented out one.

It also disappears when built with ghc rather than loaded in ghci. Which makes me think that this bug is a companion to #20169. [actually the behaviour of ghc and ghci is identical the difference that I observed was probably due to the fact that stack ghci doesn't respect the language stanza from the cabal file]

Expected behavior

Evidently, the inferred type for Product is forall k. (k -> Type) -> (k -> Type) -> k -> Type. But why this k would be made rigid in the case at hand, I have no idea. I don't think that it should be.

I expect k to be a unification variable, and the whole standalone deriving clause to type check without my help.

Environment

• GHC version used: 9.3.20220406