TFD.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType             #-}

data These a b = Neither
               | This a
               | That b
               | These a b
                
type family ToThese (a :: Maybe k) (b :: Maybe j) = (c :: These k j) where
    ToThese 'Nothing  'Nothing  = 'Neither
    ToThese ('Just a) 'Nothing  = 'This a
    ToThese 'Nothing  ('Just b) = 'That b
    ToThese ('Just a) ('Just b) = 'These a b

type family ToThese' (ab :: (Maybe k, Maybe j)) = (c :: These k j) | c -> ab where
    ToThese' '( 'Nothing, 'Nothing) = 'Neither
    ToThese' '( 'Just a , 'Nothing) = 'This a
    ToThese' '( 'Nothing, 'Just b ) = 'That b
    ToThese' '( 'Just a , 'Just b ) = 'These a b