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 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 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.