TypeLits vs. Z|Sn naturals

[Carter Schonwald]

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 <hvriedel at gmail.com> 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 at haskell.org <javascript:;>
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140518/f25e459b/attachment.html>