{-# LANGUAGE FunctionalDependencies, 
             MultiParamTypeClasses, 
             FlexibleInstances,
             FlexibleContexts,
             UndecidableInstances,
             ScopedTypeVariables,
             OverlappingInstances,
             GADTs #-}

import Prelude hiding (succ)

data Null
data Succ a

type One = Succ Null
type Two = Succ One
type Three = Succ Two

newtype SafeList l a = SafeList [a]

nil :: SafeList Null a
nil = SafeList []
cons :: a -> SafeList n a -> SafeList (Succ n) a
cons a (SafeList x) = SafeList $ a:x

at :: (Less i n) => SafeList n a -> LessThanT i Int -> a
at (SafeList a) = (a!!) . unpack

-- a < b
class Less a b where
instance Less Null (Succ a)
instance (Less a b) => Less (Succ a) (Succ b)

newtype LessThanT a b = LessThan b deriving (Show)
instance Less (LessThanT a b) a
unpack (LessThan x) = x

class Plus a b c | a b -> c where
instance (Num a) => Plus Null a a
instance Plus a Null a
instance (Plus a b c) => Plus (Succ a) (Succ b) c

class ToLess a b where
  less :: a -> Maybe (LessThanT b a)

-- Shifting values to the type level isn't fast yet possible
instance (Num a, Eq a) => ToLess a One where
  less 0 = Just (LessThan 0)
  less _ = Nothing

instance (Num a, Eq a, ToLess a b) => ToLess a (Succ b) where
  less n = case (less $ n - 1) :: Maybe (LessThanT b a) of
             Nothing -> Nothing
             Just _  -> Just (LessThan n)
 
succ :: (Num x) => LessThanT a x -> LessThanT (Succ a) x
succ (LessThan n) = LessThan $ n + 1

getAt' :: (i' ~ Succ i, Less i' n) => SafeList n a -> LessThanT i Int -> a
getAt' a i = at a $ succ i

main = do
  m <- readLn :: IO Int
  n <- readLn :: IO Int
  print $ foldl cons nil [1..n]