Hi,

yeah, I know :-)  The current solver can only evaluate concrete things, for example it knows that 5 + 3 ~ 8,

but it can't do any abstract reasoning (i.e., when there are variables around).  So things like GADTs pretty much don't work at the moment.

-Iavor

On Tue, Oct 8, 2013 at 2:08 PM, Carter Schonwald <carter.schonwald@gmail.com> wrote:

hey Iavor,

I just tried out today's head on a slightly more interesting example, and i hit the limits of the type nat solver,

http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1

it seems like something where the solver *should* work

On Mon, Oct 7, 2013 at 1:35 AM, Iavor Diatchki <iavor.diatchki@gmail.com> wrote:

Hi,

On Sun, Oct 6, 2013 at 4:36 PM, Carter Schonwald <carter.schonwald@gmail.com> wrote:

hrmm, Why don't we have a proper bijection?

lets assume we have ToPeano and a corresponding ToNat, as above,

couldn't we have something like 

asPeano :: (b~ ToPeano a, a ~ ToNat b)=> Proxy a -> Proxy b

or a suitable type level representaion thereof?

 I think it should be quite easy to define such a function, but I am afraid I don't fully understand how to use it...

 

or are you saying that in 7.8, i should be able to just efficiently work directly on the nat rep

and have  

class Cl (n::Nat) where

instance CL 0 where

instance Cl n => Cl (n+1)

and essentially get peano for free?

I am not sure if this would help with your specific task, but things like this work:

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}

{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}

import GHC.TypeLits

import Data.Proxy

class C (n :: Nat) where

  txt :: Proxy n -> String

instance C 0 where

  txt _ = "0"

instance C (n - 1) => C n where

  txt x = "1 + " ++ txt (prev x)

prev :: Proxy x -> Proxy (x - 1)

prev _ = Proxy

example = txt (Proxy :: Proxy 3)

*Main> example 

"1 + 1 + 1 + 0"

-Iavor

PS: All of this is committed in HEAD, please try it out and let me know if we need to do any last minute changes before the upcoming release.