#9731: Inductive type definitions on Nat -------------------------------------+------------------------------------- Reporter: barney | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- If you define your own type-level natural numbers by promoting {{{#!hs data Nat = Zero | Successor Nat }}} you can then define both data and type families inductively, for example {{{#!hs 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 {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9731 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler