{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}

module Test.Syd.HList where

import Data.Kind

data HList (r :: [Type]) where
  HNil :: HList '[]
  HCons :: e -> HList l -> HList (e ': l)

class HContains (l :: [Type]) a where
  getElem :: HList l -> a

instance HContains '[] () where
  getElem :: HList '[] -> ()
getElem HList '[]
HNil = ()

instance HContains l (HList l) where
  getElem :: HList l -> HList l
getElem = HList l -> HList l
forall a. a -> a
id

instance HContains '[a] a where
  getElem :: HList '[a] -> a
getElem (HCons e
a HList l
_) = a
e
a

instance HContains (a ': l) a where
  getElem :: HList (a : l) -> a
getElem (HCons e
a HList l
_) = a
e
a

instance HContains l a => HContains (b ': l) a where
  getElem :: HList (b : l) -> a
getElem (HCons e
_ HList l
hl) = HList l -> a
forall (l :: [*]) a. HContains l a => HList l -> a
getElem HList l
hl