HPC tick floating seems wrong

Consider this:

import GHC.Exts

bar :: () -> Proxy# Int
bar _ = proxy# @Int

foo xs f = map f xs

And compile with -O0 -fhpc. We get this

foo :: forall a b. [a] -> (a -> b) -> [b]
foo
  = \ (@a_aC5) (@b_aC6) ->
      letrec {
        foo_aC9 :: [a_aC5] -> (a_aC5 -> b_aC6) -> [b_aC6]
        [LclId]
        foo_aC9
          = \ (xs_avz :: [a_aC5]) (f_avA :: a_aC5 -> b_aC6) ->
              hpc<Foo,3>
              hpc<Foo,2>
              map @a_aC5 @b_aC6 (hpc<Foo,0> f_avA) (hpc<Foo,1> xs_avz); } in
      foo_aC9

bar :: () -> Proxy# Int
bar = \ (ds_dCz :: ()) -> hpc<Foo,5> hpc<Foo,4> proxy# @(*) @Int


==================== Desugar (after optimization) ====================
bar :: () -> Proxy# Int
bar = \ _ [Occ=Dead] ->
         (hpc<Foo,5> hpc<Foo,4> proxy#) @(*) @Int

foo :: forall a b. [a] -> (a -> b) -> [b]
foo
  = \ (@a_aC5) (@b_aC6) (xs_avz :: [a_aC5]) (f_avA :: a_aC5 -> b_aC6) ->
      hpc<Foo,3> hpc<Foo,2> map @a_aC5 @b_aC6
                                (hpc<Foo,0> f_avA)
                                (hpc<Foo,1> xs_avz)

Notice that for bar the HPC ticks wrap the entire expression. But for foo, the HPC ticks are pushed inwards so we get

         (hpc<Foo,5> hpc<Foo,4> proxy#)
            @(*)
            @Int

The treatment of HPC ticks seeme weirdly inconsistent: they stay outside value application but get pushed into the head of a type application. Why?

This inconsistent treatment is maintained by the simplifier, so we end up with the rather silly code for bar after CorePrep

bar = \_ -> case (hpc<Foo,5> hpc<Foo,4> proxy#) of
               f -> f @(*) @Int

This mysterious behaviour happens because of the elaborate and poorly-documented function CoreUtils.mkTick, which does this "push ticks inside type application stuff":

    App f arg
      -- Always float through type applications.
      | not (isRuntimeArg arg)
      -> mkTick' (top . flip App arg) rest f

Maybe none of this is a bug, and it probably doesn't affect many programs, but looks wrong to me. And I wish mkTick was properly documented.

All this arose from looking at this commennt in !1869 (closed)