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

[GHC]

#8695: Arithmetic overflow from (minBound :: Int) `quot` (-1)
------------------------------------------------+--------------------------
        Reporter:  rleslie                      |            Owner:
            Type:  bug                          |           Status:  patch
        Priority:  normal                       |        Milestone:  7.8.1
       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:  #1042
------------------------------------------------+--------------------------

Comment (by lerkok):

 For whatever it is worth, the SMT community has faced this issue in the
 past.  Their axiomatization implies`quot minBound  (-1) = minBound` holds
 for all sized types. See here for the axiomatization:
 http://smtlib.cs.uiowa.edu/logics/QF_BV.smt2

 I think most theorem provers take either the approach of leaving it
 completely undefined, which they have the luxury of, or completing the
 operation similarly.

 Having said that, the same axiomatization also speculates `quot x 0 = 0`
 for any x; and obviously Haskell is not ready to take that plunge quite
 yet. (Which I actually find quite acceptable; but that's besides the
 point.)

 One final thought: We strive for Haskell programs to be "semantically"
 well defined and yearn for tool support for proofs all the time. Losing
 this bit of connection from the established theorem proving community
 would be a shame; if nothing else. In particular, any system that hooks up
 Haskell to such automated tools would have to provision for such
 discrepancies. I think it would behoove us to follow the theorem proving
 community here.

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