Higher order type families in haskell

Question

If we manipulate indexed constraints for a structure, say a category, as soon as we want to write operator mapping a structure to another one, say a functor, we have to transform their indexed contraints, leading to higher kind type families.

It seems that this is not supported in haskell, but I imagine it can be defunctionalized.

Is there any other alternative to defunctionalization ?

Can/should the haskell module system (backpack) be used instead for such design ?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
import Data.Constraint
----------------------------------------------------------------------------
-- definitions
class Category (cat :: i -> i -> *) where
  type Obj cat :: i -> Constraint

class (Category dom, Category cod) => Functor f dom cod
----------------------------------------------------------------------------
newtype Id0 a = Id0 {unId0 :: a}

type family Get0 (p :: Id0 a) :: a where
  Get0 ('Id0 a) = a

-- A new category from the previous one
type Id0Cat :: forall {k}. (k -> k -> *) -> Id0 k -> Id0 k -> *
newtype Id0Cat p a b = Id12 {unId12 :: p (Get0 a) (Get0 b)}
----------------------------------------------------------------------------
-- we can write a Functor instance under the assumptions
instance
  ( Category cat,
    Category (Id0Cat cat)
  ) =>
  Functor 'Id0 cat (Id0Cat cat)
----------------------------------------------------------------------------
-- Let's prove to haskell 

instance Category cat => Category (Id0Cat cat) where
  type Obj (Id0Cat cat) = Id0Ct (Obj cat)

-- Error : Unexpected type ‘i -> Constraint’
type family Id0Ct (i -> Constraint) (Id0 i) :: Constraint where
  Id0Ct con (Id0 a) = con a