module T378a where

import Data.Kind
import Data.Singletons.TH hiding (Proxy(..))
import Prelude.Singletons hiding (Proxy(..))

$(singletons [d|
  constBA :: forall b a. a -> b -> a
  constBA x _ = x

  data Proxy :: forall k. k -> Type where
    Proxy1 :: Proxy a
    Proxy2 :: Proxy (a :: k)
    Proxy3 :: forall a. Proxy a
    Proxy4 :: forall k (a :: k). Proxy a
  |])

ex1 :: [Bool]
ex1 = [] @Bool

type PEx1 :: [Bool]
type PEx1 = '[] @Bool

sEx1 :: SList ('[] @Bool)
sEx1 = SNil @Bool

ex2 :: Bool
ex2 = constBA @Ordering @Bool True LT

type PEx2 :: Bool
type PEx2 = ConstBA @Ordering @Bool True LT

sEx2 :: Sing (ConstBA True LT)
sEx2 = sConstBA @Ordering @Bool STrue SLT

proxyEx1, proxyEx2, proxyEx3, proxyEx4 :: Proxy True
proxyEx1 = Proxy1 @True
proxyEx2 = Proxy2 @Bool @True
proxyEx3 = Proxy3 @True
proxyEx4 = Proxy4 @Bool @True

type ProxyEx1 :: Proxy True
type ProxyEx1 = Proxy1 @True

type ProxyEx2 :: Proxy True
type ProxyEx2 = Proxy2 @Bool @True

type ProxyEx3 :: Proxy True
type ProxyEx3 = Proxy3 @True

type ProxyEx4 :: Proxy True
type ProxyEx4 = Proxy4 @Bool @True

sProxyEx1 :: SProxy (Proxy1 @True)
sProxyEx1 = SProxy1 @True

sProxyEx2 :: SProxy (Proxy2 @Bool @True)
sProxyEx2 = SProxy2 @Bool @True

sProxyEx3 :: SProxy (Proxy3 @True)
sProxyEx3 = SProxy3 @True

sProxyEx4 :: SProxy (Proxy4 @Bool @True)
sProxyEx4 = SProxy4 @Bool @True