Given the following:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

type Const (a :: Type) (b :: Type) = a

GHC happily accepts these definitions:

type family F :: Const Type a where
  F = Int
type TS = (Int :: Const Type a)

However, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:

data T :: Const Type a where
  MkT :: T

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )

Bug.hs:14:3: error:
    • Quantified type's kind mentions quantified type variable
      (skolem escape)
           type: forall a1. T
        of kind: Const * a
    • In the definition of data constructor ‘MkT’
      In the data type declaration for ‘T’
   |
14 |   MkT :: T
   |   ^^^^^^^^

I'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of T:

data T2 :: Const Type a -> Type where
  MkT2 :: T2 b

Quite mysterious.

I briefly looked into where this error message is being thrown from. It turns out if you make this one-line change to GHC:

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 218f539c68..c7925767f9 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
         ; check_type (ve{ve_tidy_env = env'}) tau
                 -- Allow foralls to right of arrow

-        ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
+        ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))
                    (forAllEscapeErr env' ty tau_kind)
         }
   where

Then GHC will accept T. Whether this change is the right choice to make, I don't think I'm qualified to say.