Linear and non-linear data constructor types are printed identically

Summary

There seems to be no way to distinguish between linear and non-linear data constructors from the way GHCi prints them

Steps to reproduce

ghci> :set -XLinearTypes
ghci> import GHC.Types

ghci> data T1 a where MkT1 :: a %Many -> T1 a
ghci> :t MkT1
MkT1 :: a -> T1 a
ghci> dup :: T1 a %1 -> (a, a); dup (MkT1 x) = (x, x) -- to show it's really non-linear

<no error>

ghci> data T1 a where MkT1 :: a %1 -> T1 a
ghci> :t MkT1
MkT1 :: a -> T1 a
ghci> dup :: T1 a %1 -> (a, a); dup (MkT1 x) = (x, x) -- to show it's really linear

<interactive>:19:53: error:
    * Couldn't match type 'Many with 'One
        arising from multiplicity of `x'
    * In the pattern: MkT1 x
      In an equation for `dup': dup (MkT1 x) = (x, x)

As you can see, in both cases, the result of :t MkT1 is the same.

Expected behavior

Print one of them differently: Either explicitly show the multiplicity for the first one, or explicitly show it for the second one. (Probably explicitly show it for the linear version, since that is how :i does it.)

Environment

• GHC version used: 9.3.20220319

Optional:

• Operating System: Arch
• System Architecture: x86_64