decideKindGeneralisationPlan is too complicated

Consider this program, which originally comes from #14846 (closed). I have decorated it with kind signatures so you can see what is going on

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module T14846 where

import Data.Kind
import Data.Proxy

-- Cat :: * -> *
type Cat ob = ob -> ob -> Type

-- Struct :: forall k. (k -> Constraint) -> *
data Struct :: (k -> Constraint) -> Type where
  S :: Proxy (a::k) -> Struct (cls::k -> Constraint)

-- Structured :: forall k
--               forall (a:k) (cls:k->Constraint) -> Struct k cls
type Structured a cls = (S ('Proxy :: Proxy a) :: Struct cls)

-- AStruct :: forall k (cls : k->Constraint). Struct cls -> Type
data AStruct :: Struct cls -> Type where
  AStruct :: cls a => AStruct (Structured a cls)

-- StructI :: forall k1 k2 (cls :: k2 -> Constraint).
--            k1 -> Struct k2 cls -> Constraint
class StructI xx (structured::Struct (cls :: k -> Constraint)) where
  struct :: AStruct structured

--  Hom :: forall k1 k2 (cls :: k2 -> Constraint).
--         Cat k1 -> Cat (Struct {k2} cls)
data Hom :: Cat k -> Cat (Struct cls) where

-- Category :: forall ob. Cat ob -> Constraint
class Category (cat::Cat ob) where
  i :: StructI xx a => ríki a a

instance forall (riki :: Cat kx)
                (cls  :: kk -> Constraint).
         Category riki => Category (Hom riki :: Cat (Struct cls)) where
  i :: forall xx a. StructI xx a => Hom riki a a
  i = case struct :: AStruct (Structured a cls) of

Focus on the final instance declaration. Do kind inference on the type signature for i. I think we should get

  i :: forall {k1} {k2} {cls1 :: k2 -> Constraint}
       forall (xx :: k1) (a :: Struct {k2} cls1).
       StructI {k1} {k2} xx a => Hom {kx} {k2} riki a a

Nothing about i's type signature constraints the cls to be the same as the in-scope cls. Yes riki is in scope, but its kind is unrelated.

But at present GHC does not kind-generalise i's type (because of kindGeneralisationPlan), so random things in the body of i may influence how its kinds get fixed. And if we changed the signature a bit so that it didn't mention riki any more, suddenly it would be kind-generalised.

This seems incomprehensibly complicated to me.

Moreover, the type of i from the class decl:

class Category (cat::Cat ob) where
  i :: StructI xx a => ríki a a

comes out in its full glory as

  i :: forall k1 k2 (cls :: k2 -> Constraint)
              (xx :: k1) (a :: Struct {k2} cls)
              (riki :: Cat (Struct {k2} cls).
       StructI {k1} {k2} cls xx a => riki a a

So indeed i is expected to be as polymorphic as I expected, and the unexpected lack of generalisation gives rise (in HEAD) to a bogus error:

T14846.hs:51:8: error:
    • Couldn't match type ‘ríki’ with ‘Hom kx k1 cls0 riki’
      ‘ríki’ is a rigid type variable bound by
        the type signature for:
          i :: forall k (cls1 :: k -> Constraint) k3 (xx :: k3) (a :: Struct
                                                                        k cls1) (ríki :: Struct
                                                                                           k cls1
                                                                                         -> Struct
                                                                                              k cls1
                                                                                         -> *).
               StructI k3 k cls1 xx a =>
               ríki a a
        at T14846.hs:51:8-51
      Expected type: ríki a a
        Actual type: Hom kx k1 cls0 riki a0 a0
    • When checking that instance signature for ‘i’
        is more general than its signature in the class
        Instance sig: forall (xx :: k0) (a :: Struct k1 cls0).
                      StructI k0 k1 cls0 xx a =>
                      Hom kx k1 cls0 riki a a
           Class sig: forall k1 (cls :: k1
                                        -> Constraint) k2 (xx :: k2) (a :: Struct
                                                                             k1 cls) (ríki :: Struct
                                                                                                k1
                                                                                                cls
                                                                                              -> Struct
                                                                                                   k1
                                                                                                   cls
                                                                                              -> *).
                      StructI k2 k1 cls xx a =>
                      ríki a a
      In the instance declaration for
        ‘Category {Struct kk cls} (Hom kx kk cls riki)’