TypeNats trial on new ghc branch 7.8

1 Feb 2014


      I know that the TypeNats solver may not have been merged with 7.8 branch

but the compiler error looks so simple:

Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’

    ---------------------------------
    {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, PolyKinds, 
ExistentialQuantification #-} 

    import GHC.TypeLits

    data Vect :: Nat -> * -> * where 
      Nil ::  Vect 0 a
      Cons :: a -> Vect (n-1) a -> Vect n a

    data MyProxy (n::Nat) = forall a. MyProxy (Vect n a)

    toProxy :: Vect (n::Nat) a -> MyProxy n
    toProxy v = MyProxy v

    len :: KnownNat n => Vect (n::Nat) a -> Integer
    len v = (natVal . toProxy) v                         -- Ok

    append :: Vect n a -> Vect m a -> Vect (n+m) a
    append Nil ys = ys
    append (Cons x xs) ys = Cons x (append xs ys)  -- compiler error


    main = do
      print $ len Nil                          -- Ok
      print $ len (Cons (1::Int) Nil)          -- Ok 
    ------------------------------------------------------


Error on "append  (Cons x xs) ys = ..."

    Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’
    Expected type: Vect ((n + m) - 1) a
      Actual type: Vect ((n - 1) + m) a

TypeNats trial on new ghc branch 7.8

Gabriel Riba