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/Ve...
On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba
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