Confused about specified type variables using -XTypeApplications

[Ryan Scott]

I read in the Visible Type Applications paper [1] that you can only
apply types to "specified" type variables. However, after trying out
-XTypeApplications, I'm confused as to what exactly that means:

    $ /opt/ghc/head/bin/ghci
    GHCi, version 8.1.20160106: http://www.haskell.org/ghc/  :? for help
    λ> :set -XTypeInType -XTypeApplications
    λ> data Prox a = Prox
    λ> let prox :: Prox a; prox = Prox
    λ> :t prox @Int
    prox @Int :: Prox Int
    λ> :t Prox @Int
    Prox @Int :: Prox a

Huh? For some reason, I'm getting different types for prox @Int and
Prox @Int! I think what's happening here is that in Prox @Int, the Int
is being applied to a kind variable. That is, it's being applied to
the k variable in:

    Prox :: forall k (t :: k). Prox t

But why is this? After all, I don't think I "specified" k anywhere in
the definition of Prox, and to make things more confusing, Int gets
applied differently in prox @Int (and the definition of prox also
doesn't mention k). Is this a bug, or am I misunderstanding something
about -XTypeApplications?

Ryan S.
-----
[1] http://www.cis.upenn.edu/~eir/papers/2016/type-app/visible-type-app.pdf