Hi,
yep that's exactly the case---the current solver can only do things like "2
+ 3 ~ 5". The interesting new solver, which knows about linear
arithmetic, is currently on branch "decision-procedure" but that's quite
out of date. I am waiting for 7.8 to get out the door, and than I plan to
restart working on this, to get it updated and on the master branch,
hopefully to be part of the following GHC release.
-Iavor
On Sat, Feb 1, 2014 at 8:03 AM, Carter Schonwald wrote: Hey Gabriel,
As far as I could determine, there is no solver powers in 7.8
the "solver" can simply just check that (2 + 3 )~5 and other simple
"compute to get equality" situations On Sat, Feb 1, 2014 at 10:52 AM, Christiaan Baaij <
christiaan.baaij@gmail.com> wrote: 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 _______________________________________________
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