{-# Language TypeOperators, GADTs , KindSignatures , DataKinds , ConstraintKinds , TypeApplications , RankNTypes , ScopedTypeVariables , TypeFamilies#-}

-- a snoc list
data Snoc a = Empty | Snoc (Snoc a) a

egSnoc :: Snoc Bool
egSnoc = Empty `Snoc` True

type EgSnoc = 'Snoc 'Empty 'True

-- a singletons bool
data SBool (b :: Bool) where
 STrue  :: SBool 'True
 SFalse :: SBool 'False

-- a snoc list which just containes SBools
data SnocSBools where
 EmptySBools :: SnocSBools 
 SnocSBools  :: SnocSBools -> SBool b -> SnocSBools 

egSnocSBools :: SnocSBools 
egSnocSBools = SnocSBools EmptySBools STrue

type EgSnocSBools = 'SnocSBools 'EmptySBools 'STrue

-- a snoc list which contains altenating SBools
data SnocAlternating (first :: Bool) (carry :: Bool) where
 EmptyAlternating :: SnocAlternating first first
 SnocAlternating  :: Not b ~ carry => SnocAlternating first carry -> SBool b -> SnocAlternating first b

type family Not (b :: Bool) :: Bool where
 Not True  = False
 Not False = True

egAlternating :: SnocAlternating 'False 'True
egAlternating = SnocAlternating EmptyAlternating STrue 

type EgAlternating = ( 'SnocAlternating 'EmptyAlternating 'STrue) :: SnocAlternating 'False 'True

{-
    * Couldn't match type 'True with 'False
        arising from a use of `SnocAlternating'
    * In the expression: SnocAlternating EmptyAlternating SFalse

egAlternatingError :: SnocAlternating 'False 'True
egAlternatingError = SnocAlternating EmptyAlternating SFalse 
-}

{-
type EgAlternatingError = ( 'SnocAlternating 'EmptyAlternating 'SFalse) :: SnocAlternating 'False 'True

    * Expected kind `SnocAlternating 'False 'True',
        but 'SnocAlternating 'EmptyAlternating 'SFalse has kind `SnocAlternating
                                                                   'False 'False'
-}