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. <div><br></div><div>For that reason I'm using peano style Nats in my own lib engineering. <span></span><br>
<br>On Sunday, May 18, 2014, Herbert Valerio Riedel <<a href="mailto:hvriedel@gmail.com">hvriedel@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello again,<br>
<br>
...while experimenting with TypeLits I stumbled over the following<br>
simple case failing to type-check with GHC 7.8.2:<br>
<br>
    {-# LANGUAGE DataKinds, GADTs #-}<br>
<br>
    data List l t where<br>
        Nil  :: List 0 t<br>
        Cons :: { lstHead :: t, lstTail ::  List l t } -> List (l+1) t<br>
<br>
with the error message<br>
<br>
,----<br>
| Could not deduce (l1 ~ l) from the context ((l + 1) ~ (l1 + 1))<br>
|   bound by a pattern with constructor<br>
|              Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) t,<br>
|            in an equation for ‘lstTail’<br>
|<br>
|   ‘l1’ is a rigid type variable bound by<br>
|        a pattern with constructor<br>
|          Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) t,<br>
|        in an equation for ‘lstTail’<br>
|<br>
|   ‘l’ is a rigid type variable bound by<br>
|       the type signature for lstTail :: List (l + 1) t -> List l t<br>
|<br>
| Expected type: List l t<br>
|   Actual type: List l1 t<br>
| Relevant bindings include<br>
|   lstTail :: List l1 t<br>
|   lstTail :: List (l + 1) t -> List l t<br>
|<br>
| In the expression: lstTail<br>
| In an equation for ‘lstTail’:<br>
|     lstTail (Cons {lstTail = lstTail}) = lstTail<br>
`----<br>
<br>
While the code below happily type-checks:<br>
<br>
    {-# LANGUAGE DataKinds, GADTs #-}<br>
<br>
    data Nat = Z | S Nat<br>
<br>
    data List l t where<br>
        Nil  :: List Z t<br>
        Cons :: { lstHead :: t, lstTail :: List n t } -> List (S n) t<br>
<br>
Is this a known issue with the TypeLit solver?<br>
<br>
Cheers,<br>
  hvr<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="javascript:;" onclick="_e(event, 'cvml', 'ghc-devs@haskell.org')">ghc-devs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>