TypeLits vs. Z|Sn naturals

[Herbert Valerio Riedel]

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