I'm not familiar with GHC internals but I have a couple questions about ConstraintKinds.
It says from GHC.Exts that
data Constraint :: BOX
which is misleading because Constraint is a kind of sort BOX. This brings us to the first question: we can import and export kinds? How does that work?
Please correct me on this next part if I'm totally off. From trying out different imports and glancing around at the source on hackage, my guess is that GHC.Exts imports Constraint from GHC.Base, who in turn, imports it from GHC.Prim. But I do not see where it is defined in GHC.Prim?
To my knowledge, there is no definition of Constraint in any Haskell source file. It's a built-in, wired-in name that is defined to belong within GHC.Prim in the GHC sources itself. So in particular Constraint is not a promoted datatype, there's no corresponding datatype of kind * that is called Constraint.
There are other kinds in GHC that are treated similarly, such as AnyK, OpenKind or even BOX itself.
GHC doesn't really make a big difference internally between datatypes and kinds and anything above. That's why they e.g. all show up as being defined using data albeit with different target kinds.
Note that as far as GHC is concerned, we also have
data BOX :: BOX
It's impossible for a user to directly define new "kinds" of super-kind BOX, though.
As far as I know, importing / exporting also makes no difference between the type and kind namespaces. So e.g.
import GHC.Exts (OpenKind, BOX, Constraint)
is legal. In fact, if you then say
x :: Constraint
x = undefined
you don't get a scope error, but a kind error, saying that a type of kind * is expected, but a type/kind of kind BOX is provided.
I should perhaps also say that the whole story about kinds is somewhat in flux, and there are proposals being discussed that change this a bit: see e.g. https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds for related discussion.