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.