{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TemplateHaskell #-}
module Type.List where
import Data.Proxy
import Data.Kind
import Data.Singletons
import GHC.TypeLits
class KnownNats (ns :: [Nat]) where
natsVal :: [Int]
instance KnownNats '[] where
natsVal = []
{-# INLINE natsVal #-}
instance (KnownNat n, KnownNats ns) => KnownNats (n ': ns) where
natsVal = fromInteger (natVal (Proxy @n)) : natsVal @ns
{-# INLINE natsVal #-}
type family MkCtx (kx :: Type) (kctx :: Type) (ctx :: kctx) (x :: kx) :: Constraint where
MkCtx kx (kx ~> Constraint) ctx x = Apply ctx x
MkCtx kx (kx -> Constraint) ctx x = ctx x
MkCtx _ Constraint () _ = ()
MkCtx _ Type () _ = ()
class DemoteWith (kx :: Type) (kctx :: Type) (ctx :: kctx) (xs :: [kx]) where
demoteWith :: (forall (x :: kx). (MkCtx kx kctx ctx x) => Proxy x -> a) -> [a]
instance DemoteWith kx kctx ctxs '[] where
demoteWith _ = []
{-# INLINE demoteWith #-}
instance (DemoteWith kx kctx ctx xs, MkCtx kx kctx ctx x) => DemoteWith kx kctx ctx (x ': xs) where
demoteWith f = f (Proxy @x) : demoteWith @kx @kctx @ctx @xs f
{-# INLINE demoteWith #-}