TypeNats trial on new ghc branch 7.8

[Christiaan Baaij]

The "simplified" solver, as in
https://github.com/ghc/ghc/tree/type-nats-simple, has been integrated as
far as I know.
I've been experimenting with my own solver:
https://gist.github.com/christiaanb/8396614
Here are some examples of the stuff that works with my solver:
https://github.com/christiaanb/clash-prelude/blob/newnats/src/CLaSH/Sized/Vector.hs


On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba <griba2001 at gmail.com> wrote:

> 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
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140201/a2c17792/attachment-0001.html>