## 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)’
```