{-# LANGUAGE DataKinds, TypeOperators, GADTs, MultiParamTypeClasses, PolyKinds, ScopedTypeVariables #-}

module Data.HList where

import Data.Nat
import Data.Proxy

data HList as where
  HNil  :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

infixr 6 `HCons`

class HNth as n where
  hnth :: HList as -> Proxy n -> as :!: n
  
instance HNth as n => HNth (b ': as) ('NS n) where
  hnth (HCons _ as) _ = hnth as (Proxy :: Proxy n)

instance HNth (a ': as) 'NZ where
  hnth (HCons a _) _ = a