Index list in haskell

gistfile1.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Prim (Constraint)

data Nat = Succ Nat | Zero

data Vec n a where
    VNil :: Vec Zero a
    VCons :: a -> Vec n a -> Vec (Succ n) a

data Index n where
    IZero :: Index Zero
    ISucc :: Index n -> Index (Succ n)

type family LessThan (x :: Nat) (y :: Nat) :: Constraint where
    LessThan Zero (Succ x) = ()
    LessThan (Succ a) (Succ b) = LessThan a b
    LessThan (Succ a) x = ("Error" ~ "Inequality doesn't hold")

index :: (LessThan x n) => Vec n a -> Index x -> a
index (VCons x _) IZero = x
index (VCons _ xs) (ISucc n) = index xs n