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
Type lits currently can't do an 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
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
