{-# 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

-- Copyright   :  (C) 2017 Alexey Vagarenko

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Alexey Vagarenko (vagarenko@gmail.com)

-- Stability   :  experimental

-- Portability :  non-portable

--

----------------------------------------------------------------------------



module Type.List where



import Data.Proxy

import Data.Kind

import Data.Singletons

import GHC.TypeLits



-- | Demote type-level list of 'Nat'.

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 #-}



---------------------------------------------------------------------------------------------------

-- | Make a constraint for type @x :: kx@ from 'TyFun', or partially applied constraint, or make an empty constraint.

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               ()   _ = ()



-- | Demote a type-level list to value-level list with a type-indexed function.

--   The function takes list element as type parameter @x@ and applies constraints @ctx@ for that element.

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 #-}