https://gist.github.com/notogawa/1eb31c647bf230dbaebd88283a8b1699 を GHC 7.10 で動くよう変更。元コードの意図をちゃんと汲めてないかも・・

MatrixProd2.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module MatrixProd2 where

import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits

-- 補助関数
withSingNat :: Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
withSingNat s f =
  case someNatVal s of
   Just sn -> withSomeNat sn f
   Nothing -> error "withSingNat: invalid singleton"

withSomeNat :: SomeNat -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
withSomeNat sn f = case sn of SomeNat p -> f p

-- サイズを型で保持する行列 (行列の要素は省略)
data Matrix (row :: Nat) (col :: Nat) where
  Matrix :: (KnownNat row, KnownNat col) => Matrix row col

instance Show (Matrix row col) where
  show Matrix = show r ++ " x " ++ show c
    where
      r = natVal (Proxy :: Proxy row)
      c = natVal (Proxy :: Proxy col)

-- サイズの整合性を型によって保証する行列積
prod :: Matrix a b -> Matrix b c -> Matrix a c
prod Matrix Matrix = Matrix

-- サイズをProxyにもたせて保持するラッパー
-- 存在型を利用してサイズの型情報を隠蔽する
data SomeMatrix = forall row col.
                  SomeMatrix (Proxy row) (Proxy col) (Matrix row col)

-- 継続の中に限定して隠蔽されたサイズ情報にアクセスさせる
withSomeMatrix :: SomeMatrix
                -> (forall row col.
                   Proxy row -> Proxy col -> Matrix row col -> r)
                -> r
withSomeMatrix (SomeMatrix pr pc m@Matrix) f = f pr pc m

instance Show SomeMatrix where
  show sm = withSomeMatrix sm (\_ _ -> show)

-- 標準入力から行列を読み込む (行列の要素は省略)
-- サイズが動的に決まるのでSomeMatrixで包んでサイズ情報を隠蔽
readMatrix :: IO SomeMatrix
readMatrix = do
  line <- getLine
  let [a, b] = map read (words line)
  withSingNat a $ \sa ->
    withSingNat b $ \sb ->
      return $ SomeMatrix sa sb Matrix

-- サイズ整合性を動的にチェックする行列積
maybeProd :: SomeMatrix -> SomeMatrix -> Maybe SomeMatrix
maybeProd sm1 sm2 =
  withSomeMatrix sm1 $ \sr1 sc1 m1@Matrix ->
  withSomeMatrix sm2 $ \sr2 sc2 m2@Matrix ->
  -- 実質的にはKnownNat制約の辞書を経て値レベルのサイズ情報を得ている
  case sameNat sc1 sr2 of
   -- 動的な同値チェックだがチェックが成功した場合の整合性は型で保証される
   Just Refl -> Just (SomeMatrix sr1 sc2 (prod m1 m2))
   Nothing   -> Nothing
   -- 同値チェックに失敗してサイズが整合している証明が得られていないため
   -- Justケースの本体で置き換えるとprodの呼び出しで型エラーになる
   -- Nothing   -> Just (SomeMatrix sr1 sc2 (prod m1 m2))

main :: IO ()
main = do
  m1 <- readMatrix
  m2 <- readMatrix
  case maybeProd m1 m2 of
    Nothing -> error "Invalid"
    Just m3 -> print m3