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@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@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs