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 <[email protected] > 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 < > [email protected]> 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/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 >> >> > > _______________________________________________ > 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
