Consider this

ghci> import Data.Proxy
ghci> undefined :: '() -> Int

<interactive>:11:14: error:
    • Expected a type, but ‘ '()’ has kind ‘()’
    • In an expression type signature:  '() -> Int

What is that strange space doing before the '()?

Similarly

undefined :: Proxy '() Int

<interactive>:12:14: error:
    • Expected kind ‘* -> *’, but ‘Proxy  '()’ has kind ‘*’
    • In an expression type signature: Proxy  '() Int

Again, the strange space.

It comes from the HsType pretty printer, which is worried about printing the type

     '['K]

That is, a promoted list with one element K. The trouble is that looks like a character literal '['.

So we add an extra space, thus '[ 'K]. ''But we add it before every promoded data constructor!" Hence the spurious spaces.

In IfaceType exactly the same thing happens, but we are more clever, and only print the leading space if the promoted data con immediately follows '[ or '(. We should do the same thing for HsType.