Yes, the TypeLits solver is still in early stages, but there's active work being done to improve the situation. For better concrete syntax with Peano naturals, I recommend the following construction:

type family U n where -- U stands for "unary" U 0 = Z U n = S (n - 1)

It works well in practice for writing literals. Richard On May 18, 2014, at 2:50 PM, Carter Schonwald wrote:

Type lits currently can't do anyyyy abstract reasoning. It can only decide if two concrete literals are equal or reduce an expression made from concrete literals to a new concrete literal.

For that reason I'm using peano style Nats in my own lib engineering.

On Sunday, May 18, 2014, Herbert Valerio Riedel wrote: Hello again,

...while experimenting with TypeLits I stumbled over the following simple case failing to type-check with GHC 7.8.2:

{-# LANGUAGE DataKinds, GADTs #-}

data List l t where Nil :: List 0 t Cons :: { lstHead :: t, lstTail :: List l t } -> List (l+1) t

with the error message

,---- | Could not deduce (l1 ~ l) from the context ((l + 1) ~ (l1 + 1)) | bound by a pattern with constructor | Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) t, | in an equation for ‘lstTail’ | | ‘l1’ is a rigid type variable bound by | a pattern with constructor | Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) t, | in an equation for ‘lstTail’ | | ‘l’ is a rigid type variable bound by | the type signature for lstTail :: List (l + 1) t -> List l t | | Expected type: List l t | Actual type: List l1 t | Relevant bindings include | lstTail :: List l1 t | lstTail :: List (l + 1) t -> List l t | | In the expression: lstTail | In an equation for ‘lstTail’: | lstTail (Cons {lstTail = lstTail}) = lstTail `----

While the code below happily type-checks:

{-# LANGUAGE DataKinds, GADTs #-}

data Nat = Z | S Nat

data List l t where Nil :: List Z t Cons :: { lstHead :: t, lstTail :: List n t } -> List (S n) t

Is this a known issue with the TypeLit solver?

Cheers, hvr _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs