[Haskell-cafe] induction on type-level Nat

[Olaf Klinke]

> 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