Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications

Originally reported here. When applying types via -XTypeApplications, the type/kind that gets instantiated seems to be different depending on whether you're using functions, datatypes, or typeclasses.

Here's an example contrasting functions and datatypes:

$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160106: http://www.haskell.org/ghc/  :? for help
λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType 
λ> data Prox a = Prox
λ> prox :: Prox a; prox = Prox
λ> :t prox
prox :: forall k (a :: k). Prox k a
λ> :t prox @Int
prox @Int :: Prox * Int
λ> :t Prox
Prox :: forall k (a :: k). Prox k a
λ> :t Prox @Int
Prox @Int :: Prox Int a

This is the core of the problem: with a function, Int seems to be applied to type variable a, whereas with data types, Int appears to be applied to the kind variable k. This confuses me, since k wasn't specified anywhere in the definition of Prox.

Andres Löh also observed a similar discrepancy between functions and typeclasses:

λ> :set -XScopedTypeVariables 
λ> class C a where c :: ()
λ> d :: forall a. C a => (); d = c @_ @a
λ> :t d
d :: forall k (a :: k). C k a => ()
λ> :t d @Int
d @Int :: C * Int => ()
λ> :t c
c :: forall k (a :: k). C k a => ()
λ> :t c @Int
c @Int :: C Int a => ()
λ> :t c @_ @Int
c @_ @Int :: C * Int => ()

EDIT: See also documentation infelicity in ticket:11376#comment:113518.

EDIT: Most of this is fix, as of March 25. But the data family stuff in ticket:11376#comment:114637 is still outstanding, and we need a test case.