In order to be able to ask types to make sure something about values (their equality), you might want to create a type, which contains a value in its type-parameter, and then ask that types are equal if you want some equality property in datatype. Here's an example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module Main where

import GHC.TypeLits

newtype TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    print (MyP (one, two) (two, one))
    -- | this will error:
    -- print (MyP (one, two) (one, one))
    print (MyPGen (one, two) (two, one))
    -- | this will error:
    -- print (MyPGen (one, two) (one, one))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)