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