Length of HList

Main.hs

{-# LANGUAGE DataKinds, TypeFamilies, ScopedTypeVariables, TypeOperators, GADTs, UndecidableInstances, FlexibleContexts #-}
module Main where

import GHC.TypeLits
import Data.Proxy

main :: IO ()
main = print $ hlength (HCons "Hello" (HCons (1 :: Int) HNil))

hlength :: forall xs. KnownNat (Length xs) => HList xs -> Integer
hlength _ = natVal (Proxy :: Proxy (Length xs))

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

type family Length (a :: [*]) :: Nat where
  Length '[]       = 0
  Length (x ': xs) = 1 + (Length xs)