Couldn't match kind ‘k1’ with ‘k1’

The following program gives a hopelessly confusing error message on GHC 8.6.3 and HEAD:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

import Data.Kind

type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class SameKind a b => C (k :: Const Type a) (b :: k)

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:18: error:
    • Couldn't match kind ‘k1’ with ‘k1’
    • In the second argument of ‘SameKind’, namely ‘b’
      In the class declaration for ‘C’
   |
11 | class SameKind a b => C (k :: Const Type a) (b :: k)
   |                  ^

I imagine that the real issue is that SameKind a b would force a :: k, which would be ill-scoped. But figuring that out from this strange error message requires a lot of thought.

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture