gistfile1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

type family   TakeN (n :: Nat) (m :: Nat) (b :: Bool) (xs :: [k]) :: [k]
type instance TakeN n m 'True  xs        = '[]
type instance TakeN n m 'False (x ': xs) = x ': TakeN (n+1) m (m <=? (n+1)) xs

type Take (n :: Nat) (xs :: [k]) = TakeN 0 n 'False xs