Overlapping instances and poly-kinded types

Summary

The overlapping instances message usually looks like this:

• Overlapping instances for Cls Bool arising from a use of ‘foo’
Matching instances:
  instance Cls a
    -- Defined at /home/zliu41/ana/overlapping/A.hs:10:10
  instance Cls Bool
    -- Defined at /home/zliu41/ana/overlapping/A.hs:12:10

which makes perfect sense. But it becomes less sensible when a in one of the instances is poly-kinded, even if Cls a has an explicit kind signature on a.

Steps to reproduce

Example 1:

class Cls (a :: (Type -> Constraint) -> Type)
instance Cls a
instance Cls Proxy
foo :: Cls Proxy => Int
foo = 42
bar :: Int
bar = foo

Here the message is

• Overlapping instances for Cls Proxy arising from a use of ‘foo’
  Matching instances:
    instance Cls a -- Defined at /home/zliu41/ana/overlapping/A.hs:9:10
  There exists a (perhaps superclass) match:
  (The choice depends on the instantiation of ‘’
    To pick the first instance above, use IncoherentInstances
    when compiling the other instance declarations)

This message has several problems:

• It shows only one instance, while there are two
• It says "There exists a (perhaps superclass) match:", but doesn't show it
• "The choice depends on the instantiation of ‘’"
• It shouldn't suggest "IncoherentInstances", because the error can be fixed by adding {-# OVERLAPPABLE #-} to instance Cls a.

Example 2:

Exactly the same as Example 1, except

class Cls (a :: (Type -> Type) -> Type)

Now the message is

• Overlapping instances for Cls Proxy arising from a use of ‘foo’
  Matching instances:
    instance Cls a -- Defined at /home/zliu41/ana/overlapping/A.hs:9:10
    ...plus one instance involving out-of-scope types
      instance Cls Proxy
        -- Defined at /home/zliu41/ana/overlapping/A.hs:10:10

which is better than the message in Example 1, however, it is not clear why instance Cls Proxy is out-of-scope. Which part is out-of-scope exactly? My guess is that it's referring to the kind k in Proxy :: k -> Type, but either way it's confusing.

Expected behavior

In both Examples, the error message should be like the one in Summary.

Environment

• GHC version used: 9.3.20211002