`-fprint-typechecker-elaboration` prints type applications twice

We have

{-# LANGUAGE TypeApplications #-}

module Bug where

x = id @Int

and say

ghc -c Bug.hs -ddump-tc -fprint-typechecker-elaboration

to witness

[1 of 1] Compiling Bug              ( Bug2.hs, Bug2.o )
TYPE SIGNATURES
  x :: Int -> Int
Dependent modules: []
Dependent packages: [base-4.14.0.0, ghc-prim-0.6.1,
                     integer-gmp-1.0.2.0]

==================== Typechecker ====================
Bug.$trModule
  = GHC.Types.Module
      (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Bug"#)
AbsBinds [] []
  {Exports: [x <= x_atL
               wrap: <>]
   Exported types: x :: Int -> Int
                   [LclId]
   Binds: x = id @Int @Int
   Evidence: [EvBinds{}]}

In the Binds: field immediately above, we see x = id @Int @Int. That double type application is very strange, and surely looks wrong. Yet this module is compiled without a problem, and its desugared syntax is just fine. What on earth is going on?

The problem is that -fprint-typechecker-elaboration prints out HsWrappers. When type-checking a polymorphic call (like id), we instantiate any quantified variables by using wrappers. In this case, we follow the user's direction and instantiate id with Int. All good. This is the first @Int we see. But, the HsSyn retains the visible type application, and we print that @Int as well. Thus getting two @Ints. HsSyn visible type applications are dropped during desugaring (as they should be -- the wrappers have already incorporated what the user is trying to do with them), so all is well after desugaring. This is all jolly confusing.

What should we do? I propose not printing type applications when printing HsExpr GhcTc when -fprint-typechecker-elaboration is on. That's not ideal, though, because normally -fprint-typechecker-elaboration should give us strictly more information. So perhaps a middle road is to still print the user-written type applications with -fprint-typechecker-elaboration -dppr-debug, but clearly signpost which applications are from wrappers (and should be desugared) and which are just in HsSyn (and will be ignored).