Bad axiom produced for polykinded data family

When I say

data family DF a (b :: k)
data instance DF (Proxy c) :: Proxy j -> Type

with -ddump-tc, I get

  axiom Scratch.D:R:DFProxyProxy0 ::
    forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
      DF (Proxy c) a = Scratch.R:DFProxyProxy k1 k2 c j

This is bogus, because a should be on the RHS, too. It's not clear to me whether this is a pretty-printing bug or a real one.

Trac metadata

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