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 <[email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
