Higher-kinded type variables?

I find myself wanting to be able to Typeable quantify over higher-kinded variables, like * -> * or Constraint. This problem comes in two parts: one of them I've thought a lot about and I'm pretty sure I've cracked, and one of them I haven't been able to swing at successfully.

{-# LANGUAGE PolyKinds, DataKinds, EmptyDataDecls, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperclasses #-}
import GHC.TypeLits (Nat)
import qualified GHC.Exts as E (Any)

There's two different approaches, which depend on what version of GHC you have. The first is the simpler, if you have a newer version.

data family Any :: Nat -> k -- Not exported
type family ANY :: Nat -> k where -- Exported
  ANY = Any

Unlike the type family Any from GHC.Exts, the data family here is Typeable.

The other works if you have an older version which can't declare data families ending in anything other than *.

data AnyT0 (n :: Nat) -- None of these datatypes are exported.
data AnyT1 (n :: Nat) (a :: k)
data AnyT2 (n :: Nat) (a :: ka) (b :: kb)
-- And so on.
class E.Any => AnyC0 (n :: Nat) -- And neither are these.
class E.Any => AnyC1 (n :: Nat) (a :: k)
class E.Any => AnyC2 (n :: Nat) (a :: ka) (b :: kb)
type family ANY :: Nat -> k where -- This is, though.
  ANY = AnyT0
  ANY = AnyT1
  ANY = AnyT2
  ANY = AnyC0
  ANY = AnyC1
  ANY = AnyC2
  -- And so on.

This is also more convenient because you use GHC-provided Nats rather than bespoke Peano nats.

The problem I'm having, and the reason this is an issue rather than a pull request, is I don't know how to do inference and unification on these types. I suspect you'd need something similar to GHC's code for it.

The issue names no repository files or tests. Start by studying the proposed Haskell Any/ANY encodings and the GHC inference and unification code it references. Done would require a concrete design and implementation for higher-kinded Typeable variables, with tests demonstrating correct inference and unification.