ランタイムに失敗しないインデックス演算子

前回の発展のようなかんじで，GADT を用いて型レベル自然数同士の大小関係を表現する項を作れるようにし，「n が m より小さい」ことを示す項と Vec m a を受け取って n 番目の要素を返す関数を定義してみた．
例によって一度ランタイムに compare して LT, GT, EQ のいずれかの Ordering を得て，LT のときのみ (!!) 関数に渡せるようになっている．
しかしなんか全体的に冗長な実装になっているような気がする… LtZ と LtS の2つに対して同じようなものを書いていたりとか．

https://ideone.com/Bi7vR

{-# LANGUAGE GADTs, Rank2Types #-}
import Prelude hiding (Ordering, Eq, compare, length, (!!))

data Z = Z
data S n = S n

data LT = LT
data GT = GT
data EQ = EQ

data Ordering n m o where
  EqZ :: Ordering Z Z EQ
  EqS :: (Nat n, Nat m) => Ordering n m EQ -> Ordering (S n) (S m) EQ
  LtZ :: Nat m => S m -> Ordering Z (S m) LT
  LtS :: (Nat n, Nat m) => Ordering n m LT -> Ordering (S n) (S m) LT
  GtZ :: Nat n => S n -> Ordering (S n) Z GT
  GtS :: (Nat n, Nat m) => Ordering n m GT -> Ordering (S n) (S m) GT
data SomeOrdering n m = forall o. SomeOrdering (Ordering n m o)

data IsZero n where
  IsZero :: IsZero Z
  NotZero :: Nat n => S n -> IsZero (S n)

class Nat n where
  toInt :: n -> Int
  isZero :: n -> IsZero n
  compare :: Nat m => n -> m -> SomeOrdering n m

instance Nat Z where
  toInt _ = 0
  isZero _ = IsZero
  compare _ m =
    case isZero m of
      IsZero -> SomeOrdering EqZ
      NotZero _ -> SomeOrdering $ LtZ m
instance Nat n => Nat (S n) where
  toInt ~(S n) = 1 + toInt n
  isZero n = NotZero n
  compare ~(S n) m =
    case isZero m of
      IsZero -> SomeOrdering $ GtZ (S n)
      NotZero ~(S m') ->
        case compare n m' of
          SomeOrdering o@(LtZ _) -> SomeOrdering (LtS o)
          SomeOrdering o@(LtS _) -> SomeOrdering (LtS o)
          SomeOrdering o@(GtZ _) -> SomeOrdering (GtS o)
          SomeOrdering o@(GtS _) -> SomeOrdering (GtS o)
          SomeOrdering EqZ -> SomeOrdering (EqS EqZ)
          SomeOrdering o@(EqS _) -> SomeOrdering (EqS o)

reifyInt :: Int -> (forall n. Nat n => n -> a) -> a
reifyInt 0 k = k Z
reifyInt n k = reifyInt (n-1) $ \m -> k (S m)

data Vec n a where
  Nil :: Vec Z a
  (:::) :: Nat n => a -> Vec n a -> Vec (S n) a

toList :: Vec n a -> [a]
toList Nil = []
toList (x ::: xs) = x : toList xs

fromList :: [a] -> (forall n. Nat n => Vec n a -> b) -> b
fromList [] k = k Nil
fromList (x:xs) k = fromList xs $ \xs' -> k (x ::: xs')

length :: Vec n a -> n
length Nil = Z
length (_ ::: xs) = S (length xs)

(!!) :: (Nat n, Nat m) => Vec m a -> Ordering n m LT -> a
(x ::: _) !! (LtZ _) = x
(_ ::: xs) !! (LtS o) = xs !! o
_ !! _ = error "should not happen!"

main :: IO ()
main = do
  xs <- readLn :: IO [Int]
  x <- readLn :: IO Int
  reifyInt x $ \n -> fromList xs $ \ls ->
    case compare n (length ls) of
      SomeOrdering o@(LtZ _) -> print $ ls !! o
      SomeOrdering o@(LtS _) -> print $ ls !! o
      _ -> putStrLn "out of range!"