TypeNats trial on new ghc branch 7.8

[Carter Schonwald]

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 at 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/Vector.hs
>
>
> On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba <griba2001 at gmail.com> 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
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140201/f0a17508/attachment.html>