[GHC] #11992: RFC, add Suc to base

[GHC]

#11992: RFC, add Suc to base
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  libraries/base    |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Basically the same [https://prime.haskell.org/wiki/RemoveNPlusK rationale]
 as for `NPlusKPatterns` without some of its problems (doesn't require an
 extension or non-standard syntax), natural numbers are one of the most
 prominent inductive definitions (`data N = O | S N`) and a lot of code
 mirrors that. Little mental prowess is needed to translate

 {{{#!hs
 fac (S n) = (S n) * fac n
 }}}

 into

 {{{#!hs
 fac n = n * fac (n - 1)
 }}}

 but I have found myself itching for it in larger examples. Not a great
 rationale? Agreed. `BUT!`, no-one said ever, `does it even cover patterns
 like (5 + n)`? Funny you ask, in GHC head we can define (but ''not
 actually use'' `S` as a pattern, I'm interested being wrong):

 {{{#!hs
 hasS :: forall n. KnownNat n => Integer -> Maybe Integer
 hasS n = [ n - natVal @n Proxy | n >= natVal @n Proxy ]

 pattern S :: forall n. KnownNat n => Integer -> Integer
 pattern S n <- (hasS @n -> Just n)
   where S n = n + natVal @n Proxy
 }}}

 and if #11350 gets implemented hopefully it can be used as `S @5 n`.

 Then all we need is some type defaulting such that `S m` and `S @1 m` are
 equivalent, where if a constraint `KnownNat n` is not satisfied it
 defaults to `n ~ 1`... or is that beyond the pale?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11992#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler