Default associated type instances are too general

I compile the following with -ddump-tc and -fprint-explicit-kinds:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators,
             UndecidableInstances #-}

module Bug where

import Data.Type.Equality
import Data.Proxy

class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where
  type (:==) (x :: a) (y :: a) :: Bool
  type x :== y = x == y

and I see

TYPE SIGNATURES
TYPE CONSTRUCTORS
  PEq :: forall (a :: BOX). KProxy a -> Constraint
  class (~) (KProxy a) kproxy (KProxy a) => PEq (a::BOX)
                                                (kproxy::KProxy a)
    Roles: [nominal, nominal]
    RecFlag NonRecursive
    type family (:==) (a::BOX) (x::a) (y::a) :: Bool (open)
      Defaults: [(k, BOX), (x, k), (y, k)] k x y = (==) k x y
COERCION AXIOMS
  axiom Bug.NTCo:PEq ::
      PEq a kproxy = (~) (KProxy a) kproxy ('KProxy a)

The problem is the Defaults: line. That k should be an a. This is not a printing/tidying problem -- the default does not work when it should. For example, if I add the following

instance PEq ('KProxy :: KProxy Bool)

foo :: Proxy (True :== True) -> Proxy (True == True)
foo = id

I get

    Couldn't match type ‘(:==) Bool 'True 'True’ with ‘'True’
    Expected type: Proxy Bool ((:==) Bool 'True 'True)
                   -> Proxy Bool ((==) Bool 'True 'True)
      Actual type: Proxy Bool 'True -> Proxy Bool 'True
    In the expression: id
    In an equation for ‘foo’: foo = id

Adding kind signatures (that is :: a) to the arguments of the type family default fixes the problem.

Trac metadata

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