Kind pattern matching for kinds from term level-CodePudding

Can one use pattern matching on lifted kinds from term level ?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

module CatLib.SO.SO_KProduct where

-- | Cartesian Product
data CartProd a b = MkCartProd a b

type family Proj1 (asd :: CartProd a b) where
  Proj1 ('MkCartProd a b) = a

type family Proj2 (asd :: CartProd a b) where
  Proj2 ('MkCartProd a b) = b

map :: forall k1 k2 (ax :: CartProd k1 k2) (m :: k1 -> k2 -> *). m (Proj1 ax) (Proj2 ax)
map = __

-- -- I would prefer...
mapPM :: forall k1 k2 ('MkCartProd a x :: CartProd k1 k2) (m :: k1 -> k2 -> *). m a x
mapPM = __

CodePudding user response：

One approach is to use a type equality constraint:

mapPM :: forall k1 k2 (p :: CartProd k1 k2) (m :: k1 -> k2 -> *) a x.
    (p ~ 'MkCartProd a x) => m a x