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
