You cannot without a hacks until https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0242-un... is implemented. One hack is to use defunctionalisation, as in singletons library. Check their definition for Sigma https://hackage.haskell.org/package/singletons-3.0/docs/Data-Singletons-Sigm... where (@@) is a synonym for Apply type family, and your Tag is essentially Sing for Bool. - Oleg On 9.9.2021 18.35, Ruben Astudillo wrote:
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?