TList.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
module TList where

import Data.Proxy

data TList (ixs :: [*]) (f :: * -> *) where
  TNil  :: TList '[] f
  (:-:) :: f ix -> TList ixs f -> TList (ix ': ixs) f

infixr 5 :-:


class TListGen ixs (g :: * -> *) where
  genTList :: Proxy ixs -> g ix -> TList ixs g

instance TListGen '[] g where
  genTList _ _ = TNil

instance {-# OVERLAPS #-} TListGen ixs g => TListGen (ix ': ixs) g where
  genTList pixs g = g :-: genTList (proxyTail pixs) g
  
proxyTail :: Proxy (z ': zs) -> Proxy zs
proxyTail _ = Proxy