Constraint on type pairs

Question

I'm trying to define a typeclass that each element of a type pair satisfies a constraint:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}

data a ::: b = a ::: b

class    (c1 x, c2 y) => CP c1 c2 (k :: x ::: y)
instance (c1 x, c2 y) => CP c1 c2 (k :: x ::: y)

However this is not exaclty what i need because CP is of the wrong kind

:kind CP
CP :: (* -> Constraint) -> (* -> Constraint) -> (x ::: y) -> Constraint

How can I make c1 and c2 arguments be of more general kind k -> Constraint?

Answer 1

You're applying the constraints to the types of the elements of the pair. In order to apply it to the elements, do this:

class (k ~ (Fst k '::: Snd k), c1 (Fst k), c2 (Snd k)) => CP c1 c2 (k :: x ::: y) where
    type Fst k :: x
    type Snd k :: y
instance (c1 a, c2 b) => CP c1 c2 ((a :: x) '::: (b :: y)) where
    type Fst (a '::: b) = a
    type Snd (a '::: b) = b

The class definition says that each k :: x ::: y has a Fst k :: x and a Snd k :: y (the elements), and in order for CP c1 c2 k to hold, the elements must satisfy their respective constraints and k must indeed be the pair of its elements. The instance declaration then restates that, and also defines Fst and Snd. Now

ghci> :k CP
CP :: forall x y.
      (x -> Constraint) -> (y -> Constraint) -> (x ::: y) -> Constraint

And e.g. this works:

type MyPair = String '::: Just False -- :: Type ::: Maybe Bool
class m ~ Just (FromJust m) => IsJust (m :: Maybe k) where type FromJust m :: k
instance IsJust (Just x) where type FromJust (Just x) = x

test :: ()
test = () :: CP Show IsJust MyPair => ()