Hi all, I was doing the “Singletons” problem at codewars[1]. The basic idea is to use dependent types to encode the length of the vector in types. It uses data Nat = Zero | Succ Nat data SNat a where SZero :: SNat Zero SSucc :: SNat a -> SNat (Succ a) to do the encoding. The vector is defined based on the natural number encoding: data Vec a n where VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a (Succ n) There are some type families declared for manipulating the natural numbers, and one of them that is relevant to the question is type family (Add (a :: Nat) (b :: Nat)) :: Nat type instance Add Zero b = b type instance Add a Zero = a type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b)) where the `Add` function adds natural numbers. The problem I am stuck with is the concatenation of two vectors: (++) :: Vec v m -> Vec v n -> Vec v (Add m n) VNil ++ b = b (VCons x xs) ++ b = VCons x $ xs ++ b The program would not compile because the compiler found that `VCons x $ xs ++ b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the declared type `Vec v (Add m n)`. Is it because ghc does not expand `Add m n’ that the type does not match? I read Brent Yorgey’s blog on type-level programming[2] and he mentioned that would not automatically expand types. But the posted time of the blog is 2010 and I am wondering if there is any improvement to the situation since then? Besides, what would be the solution to this problem Warm Regards, Qingbo Liu [1] https://www.codewars.com/kata/singletons/train/haskell [2] https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-has...