HList

{-# LANGUAGE ConstraintKinds, GADTs, TypeApplications, ScopedTypeVariables, TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

import Data.Typeable
import Data.Kind (Constraint, Type)

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:#) :: t -> HList xs -> HList (t ': xs)
    
infixr 5 :#

hlength :: HList ts -> Int
hlength HNil = 0
hlength (_ :# xs) = 1 + hlength xs

hhead :: HList (x ': xs) -> x
hhead (x :# _) = x

showMiddle :: Show a => HList '[_1, a, _2] -> String
showMiddle (_ :# a :# _ :# HNil) = show a

main =  putStrLn $ showMiddle $ True :# 42 :# [1,2,3] :# HNil


five :: (a ~ Int) => a
five = 5