[GHC] #8695: Arithmetic overflow from (minBound :: Int) `quot` (-1)

[GHC]

#8695: Arithmetic overflow from (minBound :: Int) `quot` (-1)
------------------------------------------------+--------------------------
        Reporter:  rleslie                      |            Owner:
            Type:  bug                          |           Status:  new
        Priority:  normal                       |        Milestone:
       Component:  libraries/haskell2010        |          Version:  7.6.3
      Resolution:                               |         Keywords:
Operating System:  Unknown/Multiple             |     Architecture:
 Type of failure:  Incorrect result at runtime  |  Unknown/Multiple
       Test Case:                               |       Difficulty:
        Blocking:                               |  Unknown
                                                |       Blocked By:
                                                |  Related Tickets:
------------------------------------------------+--------------------------

Comment (by ekmett):

 One could argue that it is the status quo making the special case out of
 {{{y = -1}}}.

 But, without prejudging the answer, let's look at what the class is
 attempting to model.

 It has taken me a few times to get this to come out to the correct answer
 here, so I'm going to be very very pedantic. =)

 The current class laws are insufficient to properly model the notion of a
 Euclidean domain.

 To be a proper Euclidean domain

 {{{(x `quot` y)*y + (x `rem` y) == x}}}

 isn't the only law.

 The standard statement of the Euclidean domain axiom is that there exists
 a Euclidean gauge function `f :: r -> Nat` such that if `a` and `b` are in
 the domain and `b /= 0`, then there are `q` and `r` such that `a = bq + r`
 and either `r = 0` or `f(r) < f(b)`.

 Both the (`div`,`mod`) pair and the (`quot`, `rem`) pair (more or less)
 satisfy these conditions with `f = abs`, so whenever I say `f` in the
 sequel, you can just think `abs`, but I'm using it to keep my head
 straight. It'll only matter that I'm making this distinction at the very
 end.

 The assumption that `b` is non-zero rules out Herbert's case directly, but
 if you remove the side-condition that `b /= 0`, it is ruled out by the
 conditions on `r`.

 e.g. If `(q,r) = quotRem x 0` then {{{x = q*0 + r}}} by the simplified
 definition, but then `x = r`, so `f(x) < f(r)` fails to hold and the `r ==
 0` case only saves you when you divide 0 by 0.

 These rules kind of rule out the tongue-in-cheek extension of `quotRem` to
 cover `0` in one sense.

 In another, however, the definition doesn't say what happens when `b ==
 0`. For simplicity I'd like to carry on with the convention that either `r
 = 0` or `f(r) < f(y)` holds regardless and continue to treat `b == 0` as
 an error it makes sense both by convention and by the underlying
 mathematics.

 With that as a warmup, let's get back to {{{(x `quot` -1)}}} in {{{Z mod
 2^n}}}.

 {{{
 (minBound `quot` -1)* (-1)  + (minBound `rem` y)
 minBound + (minBound `rem` y) = minBound
 }}}

 says that `q = minBound` and `r = 0` would be the required answers.

 The only issue here is that stating `f = abs` doesn't work as we have the
 wart forced on us by the asymmetry of 2s complement arithmetic

 {{{
 >>> abs (minBound :: Int)
 -9223372036854775808
 }}}

 on the other hand, we've been using `abs` as an approximation of an
 injection into the natural numbers `f`, which does not have this
 limitation!

 Basically this requires `f = abs . toInteger`, then the side condition on
 `f` holds.

 So all of this indicates to me that the extension to support

 {{{minBound `quot` -1 = minBound}}}

 is correct and _is_ consistent with the definition of a Euclidean domain
 independent of 2s complement concerns.

 This frankly seems like a slam dunk to me and I'm in favor of the change.

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