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