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