<div dir="ltr">Hey Gabriel, <div style>As far as I could determine, there is no solver powers in 7.8</div><div style>the "solver" can simply just check that  (2 + 3 )~5 and other simple "compute to get equality" situations</div>

</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Feb 1, 2014 at 10:52 AM, Christiaan Baaij <span dir="ltr"><<a href="mailto:christiaan.baaij@gmail.com" target="_blank">christiaan.baaij@gmail.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">The "simplified" solver, as in <a href="https://github.com/ghc/ghc/tree/type-nats-simple" target="_blank">https://github.com/ghc/ghc/tree/type-nats-simple</a>, has been integrated as far as I know.<div>

I've been experimenting with my own solver: <a href="https://gist.github.com/christiaanb/8396614" target="_blank">https://gist.github.com/christiaanb/8396614</a></div>
<div>Here are some examples of the stuff that works with my solver: <a href="https://github.com/christiaanb/clash-prelude/blob/newnats/src/CLaSH/Sized/Vector.hs" target="_blank">https://github.com/christiaanb/clash-prelude/blob/newnats/src/CLaSH/Sized/Vector.hs</a></div>


</div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba <span dir="ltr"><<a href="mailto:griba2001@gmail.com" target="_blank">griba2001@gmail.com</a>></span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I know that the TypeNats solver may not have been merged with 7.8 branch<br>
<br>
but the compiler error looks so simple:<br>
<br>
Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’<br>
<br>
    ---------------------------------<br>
    {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, PolyKinds,<br>
ExistentialQuantification #-}<br>
<br>
    import GHC.TypeLits<br>
<br>
    data Vect :: Nat -> * -> * where<br>
      Nil ::  Vect 0 a<br>
      Cons :: a -> Vect (n-1) a -> Vect n a<br>
<br>
    data MyProxy (n::Nat) = forall a. MyProxy (Vect n a)<br>
<br>
    toProxy :: Vect (n::Nat) a -> MyProxy n<br>
    toProxy v = MyProxy v<br>
<br>
    len :: KnownNat n => Vect (n::Nat) a -> Integer<br>
    len v = (natVal . toProxy) v                         -- Ok<br>
<br>
    append :: Vect n a -> Vect m a -> Vect (n+m) a<br>
    append Nil ys = ys<br>
    append (Cons x xs) ys = Cons x (append xs ys)  -- compiler error<br>
<br>
<br>
    main = do<br>
      print $ len Nil                          -- Ok<br>
      print $ len (Cons (1::Int) Nil)          -- Ok<br>
    ------------------------------------------------------<br>
<br>
<br>
Error on "append  (Cons x xs) ys = ..."<br>
<br>
    Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’<br>
    Expected type: Vect ((n + m) - 1) a<br>
      Actual type: Vect ((n - 1) + m) a<br>
<br>
<br>
<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>