Inductive type definitions on Nat

If you define your own type-level natural numbers by promoting

data Nat = Zero | Successor Nat

you can then define both data and type families inductively, for example

data family Vector1 :: Nat -> * -> *
data instance Vector1 Zero a = EmptyVector
data instance Vector1 (Successor n) a = MkVector a (Vector1 n a)

Using the built-in Nat, there is no way to define inductive data families, and inductive type families such as

type family Vector2 :: Nat -> * -> * where
    Vector2 0 a = ()
    Vector2 n a = (a, (Vector2 (n-1) a))

require UndecidableInstances (and must be closed).

This proposal is to add (n+k) patterns for Nat, so that the built-in naturals can be used in the same way that the user defined naturals can, to define type and data families inductively.

Trac metadata

Trac field	Value
Version	7.8.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture