The following code:

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

import GHC.TypeLits

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n + 1) a

infixr 5 :>

when loaded in GHCi 7.8.3, and asking for the type of (1 :> 2 :> 3 :> Nil), gives:

$ ghci example/vec.hs 
GHCi, version 7.8.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a

while in GHCi 7.10.1 it gives:

$ ghci example/vec.hs 
GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a

That is, the type-level computation, ((0 + 1) + 1) + 1 is only simplified to 2 + 1 in GHC 7.10.1, whereas in 7.8.3 2+1 was further simplified to 3.

The same still happens in HEAD (20150417)

$ ghci example/vec.hs 
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a

I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.