AddrSing for https://stackoverflow.com/questions/52750918/lifting-existentials-to-type-level

AddrSing.hs

{-# LANGUAGE TemplateHaskell, GADTs, ScopedTypeVariables, PolyKinds, DataKinds,
             TypeFamilies, TypeOperators, UndecidableInstances, InstanceSigs,
             TypeApplications, FlexibleInstances, StandaloneDeriving #-}

module AddrSing where

import GHC.TypeLits
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Sigma

singletons
  [d| data AddrType = Post | Email | Office
        deriving Show
  |]

data AddrFields :: AddrType -> Type where
  PostFields :: { city :: Symbol, street :: Symbol } -> AddrFields Post
  EmailFields :: { email :: Symbol } -> AddrFields Email
  OfficeFields :: { floor :: Nat, desk :: Nat } -> AddrFields Office

deriving instance Show (AddrFields addrType)

data SAddrFields :: forall addrType. AddrFields addrType -> Type where
  SPostFields :: Sing city -> Sing street -> SAddrFields (PostFields city street)
  SEmailFields :: Sing email -> SAddrFields (EmailFields email)
  SOfficeFields :: Sing floor -> Sing desk -> SAddrFields (OfficeFields floor desk)

deriving instance Show (SAddrFields addrFields)

type instance Sing = SAddrFields

instance (SingI city, SingI street) => SingI (PostFields city street) where
  sing = SPostFields sing sing

instance (SingI email) => SingI (EmailFields email) where
  sing = SEmailFields sing

instance (SingI floor, SingI desk) => SingI (OfficeFields floor desk) where
  sing = SOfficeFields sing sing

type Addr = Sigma AddrType (TyCon AddrFields)

singletons
  [d|
    someCoolPredicate :: [Addr] -> Bool
    someCoolPredicate (_ : _) = True
    someCoolPredicate [] = False
  |]

data AddrList :: [Addr] -> Type where
  MkAddrList :: (SomeCoolPredicate addrs ~ True) => Sing addrs -> AddrList addrs

deriving instance Show (AddrList addrs)

addrList = MkAddrList @'[SPost :&: PostFields "Foo" "Bar"] sing