#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