Poor pretty-printing of GADT constructors in GHCi

I recently loaded this file into GHCi:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Proxy

data Foo1 (a :: k) where
  MkFoo1a :: Proxy a -> Int -> Foo1 a
  MkFoo1b :: { a :: Proxy a, b :: Int } -> Foo1 a

data family Foo2 (a :: k)
data instance Foo2 (a :: k) where
  MkFoo2a :: Proxy a -> Int -> Foo2 a
  MkFoo2b :: { c :: Proxy a, d :: Int} -> Foo2 a

And when I queried these datatypes with :info, I saw this:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint-explicit-kinds
GHCi, version 8.7.20181129: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :i Foo1 Foo2
type role Foo1 nominal phantom
data Foo1 @k (a :: k) where
  MkFoo1a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo1 k a
  MkFoo1b :: forall k (a :: k).
             {a :: Proxy @{k} a, b :: Int} -> Foo1 k a
        -- Defined at Bug.hs:8:1
data family Foo2 @k (a :: k)    -- Defined at Bug.hs:12:1
data instance forall k (a :: k). Foo2 @k a where
  MkFoo2a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo2 @k a
  MkFoo2b :: forall k (a :: k).
             {c :: Proxy @{k} a, d :: Int} -> Foo2 @k a
        -- Defined at Bug.hs:13:15

Yuck. A couple of icky things to note here:

• For some reason, the Proxy @{k} a field is needlessly parenthesized in MkFoo1a and MkFoo2a. This does //not// happen when record syntax is used, as demonstrated with MkFoo1b and MkFoo2b.
• Even more strangely, despite the fact that k is a specified argument, we're pretty-printing the return type of MkFoo1{a,b} as Foo k a, not Foo @k a. This problem doesn't appear to happen for data family instances, since MkFoo2{a,b} don't have this issue.

Patch incoming.

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