is there a way around this? ~$ ghci GHCi, version 9.12.3: https://www.haskell.org/ghc/ :? for help ghci> :set -XGADTs ghci> :set -XDataKinds ghci> :m Data.Kind ghci> data T :: (Type, Type) -> Type where T :: a -> b -> T '(a, b) ghci> let lengthT :: [T '(a, b)] -> Int; lengthT = length ghci> let lengthT2 :: [T a_b] -> Int; lengthT2 = lengthT :14:44: error: [GHC-25897] • Couldn't match type ‘a_b’ with ‘'(a0, b0)’ Expected: [T a_b] -> Int Actual: [T '(a0, b0)] -> Int ‘a_b’ is a rigid type variable bound by the type signature for: lengthT2 :: forall (a_b :: (*, *)). [T a_b] -> Int at :14:5-30 • In the expression: lengthT In an equation for ‘lengthT2’: lengthT2 = lengthT • Relevant bindings include lengthT2 :: [T a_b] -> Int (bound at :14:33) (I need this to be able to use types like T in libraries that type-safely store and retrieve values of a parameterized type of any kind, including a tuple kind, which sometimes works, but often not for silly reasons like the above) I guess "type Fst '(a, b) = a" might be a workaround, but it doesn't typecheck, but maybe there is a type-function like that pre-defined somewhere?