Core Lint error (ghc 9.1.0.20201202)

This piece of code (see #19092 (closed)) triggers a core lint error, I don't know why!

{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}

{-# Options_GHC -dcore-lint #-}

import Data.Type.Equality
import Data.Kind

type PolyKinded :: Type -> Type
type PolyKinded res = (forall (k :: Type). k -> res)

infix 4
 ===
type
 (===) :: PolyKinded (PolyKinded Bool)
type family
 a === b where
 a === a = True
 _ === _ = False

type  TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
class (a === b) ~ cond
   => TryUnify cond a b

$ ghc --interactive -ignore-dot-ghci ~/hs/4007_bug.hs
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/baldur/hs/4007_bug.hs, interpreted )
*** Core Lint errors : in result of TcGblEnv axioms ***
/home/baldur/hs/4007_bug.hs:22:1: warning:
    Kind application error in type `TryUnify cond_aBb a_aBc b_aBd'
      Function kind = Bool -> forall k. k -> forall k. k -> Constraint
      Arg types = [cond_aBb, k2_X0, a_aBc, k2_X0, b_aBd]
    Fun: k2_X0 -> forall k. k -> Constraint
         a_aBc :: k1_aBi
    In the coercion axiom N:TryUnify :: [(cond_aBb :: Bool), k1_aBi,
                                         (a_aBc :: k1_aBi), k2_aBi, (b_aBd :: k2_aBi)].
                                        TryUnify cond_aBb a_aBc b_aBd
                                        ~_R
                                        (a_aBc === b_aBd) ~ cond_aBb
    Substitution: [TCvSubst
                     In scope: InScope {k2_X0 cond_aBb a_aBc b_aBd k1_aBi}
                     Type env: [aBb :-> cond_aBb, aBc :-> a_aBc, aBd :-> b_aBd,
                                aBi :-> k2_X0]
                     Co env: []]
/home/baldur/hs/4007_bug.hs:22:1: warning:
    Kind application error in type `a_aBc === b_aBd'
      Function kind = forall k. k -> forall k. k -> Bool
      Arg types = [k2_X0, a_aBc, k2_X0, b_aBd]
    Fun: k2_X0 -> forall k. k -> Bool
         a_aBc :: k1_aBi
    In the coercion axiom N:TryUnify :: [(cond_aBb :: Bool), k1_aBi,
                                         (a_aBc :: k1_aBi), k2_aBi, (b_aBd :: k2_aBi)].
                                        TryUnify cond_aBb a_aBc b_aBd
                                        ~_R
                                        (a_aBc === b_aBd) ~ cond_aBb
    Substitution: [TCvSubst
                     In scope: InScope {k2_X0 cond_aBb a_aBc b_aBd k1_aBi}
                     Type env: [aBb :-> cond_aBb, aBc :-> a_aBc, aBd :-> b_aBd,
                                aBi :-> k2_X0]
                     Co env: []]
*** Offending Program ***
axiom D:R:=== ::
  forall {k} {a :: k}.
    a === a = 'True -- Defined at /home/baldur/hs/4007_bug.hs:18:2
  _ === _ = 'False -- Defined at /home/baldur/hs/4007_bug.hs:19:2
axiom N:TryUnify ::
  forall {cond :: Bool} {k1} {a :: k1} {k2} {b :: k2}.
    TryUnify cond a b = (a_aBc === b_aBd) ~ cond_aBb
      -- Defined at /home/baldur/hs/4007_bug.hs:22:1
*** End of Offense ***


<no location info>: error:
Compilation had errors


*** Exception: ExitFailure 1
ghci>

If you unfold

type  TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)

PolyKinded the program compiles

type  TryUnify :: Bool -> forall k. k -> PolyKinded Constraint

type  TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint