Hi List, When I try to build below program, the compiler complains Couldn't match type ‘n’ with ‘1 + (n - 1)’ … Why GHC (7.10.3) cannot do type level natural number arithmetic? `` n /= 1 + (n-1)`` at type level? -- | main.hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE DeriveGeneric #-} module Main where import qualified Data.ByteString as B import Data.ByteString(ByteString) import Data.Serialize -- require cereal import GHC.TypeLits data Scalar :: Nat -> * -> * where Nil :: Scalar 0 a Cons :: a -> Scalar m a -> Scalar (1+m) a instance (Serialize a) => Serialize (Scalar 0 a) where get = return Nil put _ = return $ mempty instance (Serialize a) => Serialize (Scalar n a) where get = do x <- get :: Get a xs <- get :: Get (Scalar (n-1) a) return $! Cons x xs put (Cons x xs) = do put (x :: a) put xs -- /tmp/vect1/app/Main.hs:31:15: Couldn't match type ‘n’ with ‘1 + (n - 1)’ … ‘n’ is a rigid type variable bound by the instance declaration at /tmp/vect1/app/Main.hs:27:10 Expected type: Scalar n a Actual type: Scalar (1 + (n - 1)) a Relevant bindings include xs :: Scalar (n - 1) a (bound at /tmp/vect1/app/Main.hs:30:5) get :: Get (Scalar n a) (bound at /tmp/vect1/app/Main.hs:28:3) In the second argument of ‘($!)’, namely ‘Cons x xs’ In a stmt of a 'do' block: return $! Cons x xs Compilation failed. - baojun