yay, it works and in both directions: [...] ghci> :set -XTypeFamilies ghci> type family Fst (a_b :: (Type, Type)) :: Type where Fst '(a, b) = a ghci> type family Snd (a_b :: (Type, Type)) :: Type where Snd '(a, b) = b ghci> let lengthT2 :: a_b ~ '(Fst a_b, Snd a_b) => [T (a_b :: (Type, Type))] -> Int; lengthT2 = lengthT ghci> let lengthT3 :: [T '(a, b)] -> Int; lengthT3 = lengthT2