Inconsistent treatment of implicitly bound kind variables as free-floating

(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)

This program is accepted:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

data Foo = MkFoo (forall a. Proxy a)

There's something interesting going on here, however. Because PolyKinds is enabled, the kind of a is generalized to k. But where does k get quantified? It turns out that it's implicitly quantified as an existential type variable to MkFoo:

λ> :i Foo
data Foo = forall k. MkFoo (forall (a :: k). Proxy a)

This was brought up some time ago in #7873 (closed), where the conclusion was to keep this behavior. But it's strange becuase the k is existential, so the definition is probably unusable.

But to make things stranger, it you write out the kind of a explicitly:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

data Foo2 = MkFoo2 (forall (a :: k). Proxy a)

Then GHC will reject it:

Bug.hs:7:1: error:
    Kind variable ‘k’ is implicitly bound in data type
    ‘Foo2’, but does not appear as the kind of any
    of its type variables. Perhaps you meant
    to bind it (with TypeInType) explicitly somewhere?
  |
7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

So GHC's treatment is inconsistent. What should GHC do? We could:

1. Have both be an error.

2. Have both be accepted, and implicitly quantify k as an existential type variable

3. Have both be accepted, and implicitly quantify k in the forall itself. That is:

   MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo

4. Something else. When you try a similar trick with type synonyms:

   {-# LANGUAGE ExistentialQuantification #-}
   {-# LANGUAGE PolyKinds #-}
   {-# LANGUAGE RankNTypes #-}
   
   import Data.Proxy
   
   type Foo3 = forall a. Proxy a

   Instead of generalizing the kind of a, its kind will default to Any:

   λ> :i Foo3
   type Foo3 = forall (a :: GHC.Types.Any). Proxy a

   Would that be an appropriate trick for data types as well?