Typed holes show applications to inferred arguments

Typed hole suggestions print type arguments using @T, even if the argument is inferred. For example,

λ> :set -XPolyKinds -XTypeApplications
λ> data T a = MkT
λ> foo :: T Int; foo = _

<interactive>:3:21: error:
    • Found hole: _ :: T Int
    • In the expression: _
      In an equation for ‘foo’: foo = _
    • Relevant bindings include
        foo :: T Int (bound at <interactive>:3:15)
      Valid hole fits include
        foo :: T Int (bound at <interactive>:3:15)
        MkT :: forall k (a :: k). T a
          with MkT @* @Int
          (defined at <interactive>:2:12)

The penultimate line should be MkT @Int (or, if we allowed to specify inferred arguments, something like MkT @{*} @Int).

The motivation comes from the linear types branch; in linear types, constructors have additional inferred multiplicity arguments, which significantly clutters the output.