[Haskell-cafe] Using a non fully saturated type family

[Ruben Astudillo]

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)