Alternative approach with a GADT:

data T n a where End :: T 0 a Cons :: a -> T n a -> T (n+1) a

viewL :: T (n+1) a -> (a, T n a) viewL (Cons x xs) = (x, xs)

testEnd :: T 0 a -> () testEnd End = ()

For viewL GHC reports a missing pattern match on 'End' and for testEnd it reports a missing match on 'Cons'. If I add the constraint (1<=n+1) to Cons then the testEnd warning disappears. If I add the constraint (1<=n+1) to viewL, then its warning disappears, as well.

So the theory of type-level nats lacks the theorem forall m n. n+m <= n :: Nat -> Nat -> Constraint The infix type operator + from GHC.TypeLits constrains n in Cons to kind Nat. So the theorem above ought to be available to the type checker. Hiromi's type-natural package has Lemmas plusLeqL and plusLeqR for this. Olaf