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>