This is a reduction of a problem that occurs in real code.

{-# LANGUAGE PolyKinds #-}
class D a => C (f :: k) a
class C () a => D a

Typechecking complains:

    The first argument of ‘C’ should have kind ‘k’,
      but ‘()’ has kind ‘*’
    In the class declaration for ‘D’

This program should be accepted, but we're not generalizing enough.

A slightly less reduced version of the problem arises in practice in:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}

import Control.Category

class (Category c, Category d, Category e) => Profunctor
  (p :: x -> y -> z)
  (c :: x -> x -> *)
  (d :: y -> y -> *)
  (e :: z -> z -> *)
  | p -> c d e

-- lens-style isomorphism families in an arbitrary category
type Iso (c :: i -> i -> *) (s :: i) (a :: i) = forall (p :: i -> i -> *). 
  Profunctor p c c (->) => p a a -> p s s

class Category e => Cartesian (e :: z -> z -> *) where
  type P e :: z -> z -> z
  associate :: Iso e (P e (P e a b) c) (P e a (P e b c))

This typechecks, but if I replace the line

class (Category c, Category d, Category e) => Profunctor

with

class (Category c, Category d, Cartesian e) => Profunctor

to say that you can only enrich a category over a monoidal category (using Cartesian in the approximation here), then it fails because a more baroque version of the same kind of cycle as the minimal example above as Profunctor references Cartesian which references an Iso which mentions a Profunctor.

I'm supplying explicit kind variables in the signature of the class, so we should be able to use those like we do with function signatures a universe down. =/