А можно как-то констрейнты затащить на каинд левел? infixr 5 :&&: data

Question

А можно как-то констрейнты затащить на каинд левел? infixr 5 :&&: data

LoT k where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)

type TypeNatExpr :: forall k. k -> k -> Type
type TypeNatExpr k1 k2 = Proxy k1 -> Proxy k2 -> Type

type k1 ~> k2 = TypeNatExpr k1 k2

infixr 4 ~>

type HeadLoT :: forall k k'. LoT (k -> k') -> k -> Constraint
class HeadLoT l h | l -> h

instance HeadLoT (a :&&: as) a

type TailLoT :: forall k k'. LoT (k -> k') -> LoT k' -> Constraint
class TailLoT l t | l -> t

instance TailLoT (a :&&: as) as

type Apply :: forall k. k -> LoT k -> Type -> Constraint
class Apply x l t | l x -> t

instance Apply f LoT0 f
instance (HeadLoT as h, TailLoT as t, Apply (f h) t r) => Apply f as r

type Apply1 :: forall k. k -> LoT k -> Type
type Apply1 f as = forall r. Apply f as r => r

type TEvalN :: forall f g as. (f ~> g) -> Apply1 f as -> Apply1 g as -> Constraint
class TEvalN nat f g | nat f -> g