Hello Cafe. I am trying to encode a version of sigma types using GADTs for the tag and a type family as the function between the GADT and the universe of types. My code looks like this (notice the use of StandaloneKindSignatures). --- | dependent.hs {-# language RankNTypes, PolyKinds, TypeFamilies, GADTs #-} {-# language StandaloneKindSignatures, DataKinds #-} module Main where import Data.Kind (Type) import Data.Functor.Identity main :: IO () main = return () type Tag :: Bool -> Type data Tag b where STrue :: Tag True SFalse :: Tag False type ApplyTag :: Bool -> Type type family ApplyTag t where ApplyTag 'True = Int ApplyTag 'False = Char type Sigma :: forall k. (k -> Type) -> (k -> Type) -> Type data Sigma t f where (:&:) :: forall t f a. t a -> f a -> Sigma t f ex :: Sigma Tag ApplyTag ex = STrue :&: 27 The error I get is dependent.hs:24:7: error: • The type family ‘ApplyTag’ should have 1 argument, but has been given none • In the type signature: ex :: Sigma Tag ApplyTag | 24 | ex :: Sigma Tag ApplyTag | ^^^^^^^^^^^^^^^^^^ which is true! How can I recover the intuition of type families being functions at the type level? -- Rubén. (pgp: 4EE9 28F7 932E F4AD)