[Haskell-cafe] induction on type-level Nat

[Henning Thielemann]

On Fri, 13 Jan 2023, Henning Thielemann wrote:

> I want to define a list with type-level Nat length:
>
> type family List (n::Nat) :: Type -> Type where
>   List 0 = End
>   List n = Cons (List (n-1))
>
> data End a = End
> data Cons f a = Cons { head :: a, tail :: f a }


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.