TypeLits vs. Z|Sn naturals

[Richard Eisenberg]

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 <carter.schonwald at gmail.com> 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 <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
> 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/20140518/e1564e38/attachment.html>