{-# LANGUAGE DataKinds, GADTs #-}
{-# OPTIONS -Wall #-}
module M where

import GHC.TypeLits

data Idx n where
  ZI :: Idx 0
  (::@) :: Int -> Idx n -> Idx (n + 1)
infixr ::@

barIdx :: Idx 2 -> Int
barIdx (i ::@ j ::@ ZI) = i + j