[Haskell-cafe] New type of ($) operator in GHC 8.0 is problematic

[Tom Ellis]

On Sat, Feb 06, 2016 at 12:12:47PM -0500, Edward Kmett wrote:
> The primitives that GHC uses to implement arrays, references and the like
> live in #. We then wrap them in something in * before exposing them to the
> user, but you can shave a level of indirection by knowing what lives in #
> and what doesn't.
> 
> But even if you never care about #, Int, Double, etc. are of kind *,
> Functors are of kind * -> *, etc. so to talk about the type of types at all
> you need to be able to talk about these concepts at all with any rigor, and
> to understand why Maybe Maybe isn't a thing.

(This question is for my own edification and is not meant to be a point in
the current debate)

If we were inventing a language from the beginning, would it be strictly
necessary to have two kinds?  Could we have just an unboxed kind #, and have
a box be an explicit type constructor?  If the type constructor were called
'P' (standing for pointer) then we could have

    id :: P a -> P a

    data [a] = (P a) : [a] | []

etc.

Does this thing seem remotely plausible to people who know clever type
theory?

Tom