Typeclass fails to compile with StandaloneKindSignatures; only compiles with conventional kind annotations

Summary

A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.

Steps to reproduce

Try to compile this module:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Main where

import Data.Kind
import Data.Proxy
import GHC.TypeLits

data Color
  = R
  | B
  deriving (Show, Eq)

data Map symbol q
  = E
  | N Color (Map symbol q) symbol q (Map symbol q)
  deriving (Show, Eq)

type Record :: (q -> Type) -> Map Symbol q -> Type
data Record f t where
  Empty :: Record f E
  Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right)

type CanMakeBlack :: Map Symbol q -> Constraint
class CanMakeBlack t where
  type MakeBlack t :: Map Symbol q
  makeBlackR :: Record f t -> Record f (MakeBlack t)

instance CanMakeBlack (N color left k v right) where
  type MakeBlack (N color left k v right) = N B left k v right
  makeBlackR (Node left fv right) = Node left fv right

instance CanMakeBlack E where
  type MakeBlack E = E
  makeBlackR Empty = Empty

type Delable :: Symbol -> q -> Map Symbol q -> Constraint
class Delable k v t where
-- Using conventional kind annotations, it compiles correctly
--class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
  type Del k v t :: Map Symbol q
  del :: Record f t -> Record f (Del k v t)

type Deletable :: Symbol -> q -> Map Symbol q -> Constraint
class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
  type Delete k v t :: Map Symbol q
  _delete :: Record f t -> Record f (Delete k v t)

instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
  type Delete k v t = MakeBlack (Del k v t)
  _delete r = makeBlackR (del @_ @k @v r)

main :: IO ()
main = pure ()

The compilation will fail with the error:

Main.hs:70:15: error:
    * Could not deduce: MakeBlack (Del k v t) ~ MakeBlack (Del k v t)
      from the context: (Delable k v t, Del k v t ~ deleted,
                         CanMakeBlack deleted)
        bound by the instance declaration at Main.hs:68:10-86
      Expected: Record f (Delete k v t)
        Actual: Record f (MakeBlack (Del k v t))
      NB: `MakeBlack' is a non-injective type family

However, if instead of the line

class Delable k v t where

We use the line

class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where

The code compiles correctly, even if the standalone kind signature remains.

Expected behavior

The code should compile correctly with the standalone kind signature, without need of explicit kind annotations on the variables.

Environment

• GHC version used: 9.0.1

Optional:

• Operating System: Windows 10