'Kind pattern matching for kinds from term level

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 = __
haskell


Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source

Related Questions