haskell - kindsignature と typeoperators を使用した型レベルの算術演算?

Question

私はghc 7.6でデータ型をいじっていましたが、思ったようにうまくいきませんでした。

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
import GHC.TypeLits

data Array (i :: Nat) a = Array {
  num :: Int,
  elems :: [a]
} deriving (Eq, Show)

arr10 :: Array 10 Int
arr10 = arrn 10

arr20 :: Array 20 Int
arr20 = arrn 20

arrn :: Int -> Array a Int
arrn n = Array n (replicate n 0)

arrconcat :: Array a e -> Array b e -> Array (a+b) e
arrconcat (Array a as) (Array b bs) = Array (a+b) (as ++ bs)

ghciで：

*Main> arr10 
Array {num = 10, elems = [0,0,0,0,0,0,0,0,0,0]}

*Main> arr10 == arr10
True

*Main> arr20
Array {num = 20, elems = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]}

*Main> arr10 `arrconcat` arr20
Array {num = 30, elems = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]}

*Main> :t arr10 `arrconcat` arr20
arr10 `arrconcat` arr20 :: Array (10 + 20) Int

*Main> :t arr10 `arrconcat` arr10 == arr20
<interactive>:1:1:
    Couldn't match type `10 + 10' with `20'
    Expected type: Array 20 Int
      Actual type: Array (10 + 10) Int
    In the first argument of `(==)', namely `arr10 `arrconcat` arr10'
    In the expression: arr10 `arrconcat` arr10 == arr20

この種のタイプレベルの数値で私がやろうとしていることを行う方法はありますか、それとも最終的に機能する予定ですか?