Type level programming analogue to "flip" function for MPTC?

Learn
#1

For there following program, type class C is a MPTC, and AnyC is some sort of “Any Type” where mkAny is the desired effect. For C the second type parameter is meant to be shared by its “family” of instances, while the first one is the actual type. But I couldn’t figure out how to “flip” the type parameters when creating the IsAnyTypeOf instance for AnyC implementation.

{-# LANGUAGE DeriveAnyClass         #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies           #-}

import           Data.Kind

-- ~a~ is an ~AnyType~ of ~c~
class IsAnyTypeOf (a :: Type) (c :: Type -> Constraint) | a -> c where
  mkAny :: c e => e -> a

--

class C a b

data X1 t = X1 t
instance C (X1 t) t

data X2 t = X2 (t, t)
instance C (X2 t) t

data AnyC t = forall a. C a t => MkAnyC a
deriving instance C (AnyC t) t

x1 :: X1 Int
x1 = X1 2

x2 :: X2 Int
x2 = X2 (4, 2)

cs :: [AnyC Int]
cs = [MkAnyC x1, MkAnyC x2]

-- QUESTION: how to flip C ?  t?
-- instance AnyC t `IsAnyTypeOf` C ? t where
--  mkAny = MkAnyC

-- QUESTION:  How to create `cs'` using `mkAny`?
-- cs' :: [AnyC Int]
-- cs' = [mkAny x1, mkAny x2]

Edit, just to show an example use of IsAnyTypeOf for a type class without MPTC:

-- Non MPTC

class C₀ a

data X₀1 = X₀1 Int
instance C₀ X₀1
data X₀2 = X₀2 (Int, Int)
instance C₀ X₀2

data AnyC₀ = forall a. C₀ a => MkAnyC₀ a
deriving instance C₀ AnyC₀

instance AnyC₀ `IsAnyTypeOf` C₀ where
  mkAny = MkAnyC₀

cs₀ :: [AnyC₀]
cs₀ = [mkAny (X₀1 2), mkAny (X₀2 (4, 2))]
#2

I got it resolved… by using an intermediary type class do the flipping :confused:

class c b a => MPTCFlip c a b
deriving instance C b a => MPTCFlip C a b

Full program:

{-# LANGUAGE DeriveAnyClass          #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import           Data.Kind


class c a => IsAnyTypeOf (a :: Type) (c :: Type -> Constraint) | a -> c where
  mkAny :: c e => e -> a

class Show a => C a b

data X1 t = X1 t deriving Show
instance Show t => C (X1 t) t

data X2 t = X2 (t, t) deriving Show
instance Show t => C (X2 t) t

data AnyC t = forall a. C a t => MkAnyC a
deriving instance C (AnyC t) t
instance Show (AnyC t) where show (MkAnyC a) = show a

class c b a => MPTCFlip c a b
deriving instance C b a => MPTCFlip C a b

instance AnyC t `IsAnyTypeOf` (MPTCFlip C t) where
  mkAny = MkAnyC

main = do
  print $ show ([mkAny (X1 (2 :: Int)), mkAny (X2 ((4::Int), (2::Int)))] :: [AnyC Int])
  print "end"