git.iko.soy/Idris-dev
on master help sign in
Use bit-pattern identity for Double

Change the conversion checker to use bit-pattern identity on Double instead of the IEEE comparison that Haskell's Eq type class implements. Previously, we had definitionally equal values like -0.0 and 0.0 that could nevertheless be distinguished by programs. This breaking of functionality allowed proving a contradiction. Thanks to Ryan Scott for the tip on how to do the bit-pattern comparison! Fixes #2609.

commit4079f544345145b571898db0bff154e380eb663c authorDavid Christiansen <david@davidchristiansen.dk> dateFri 8 Apr 2016, 19:30 (11 years ago) parent89401f2
6 files changed+60−1
compare with master
unifiedsplit
CHANGELOG.md+6 idris.cabal+5 src/Idris/Core/TT.hs+26−1 test/reg072/DoubleEquality.idr+5 test/reg072/expected+15 test/reg072/run+3
CHANGELOG.md+6
@@ -52,6 +52,12 @@
5252 Java codegen and has now been deprecated, together with the
5353 corresponding `--mvn` option.
5454
55+* Definitional equality on Double is now bit-pattern identity rather
56+ than IEEE's comparison operator. This prevents a bug where programs
57+ could distinguish between -0.0 and 0.0, but the type theory could
58+ not, leading to a contradiction. The new fine-grained equality
59+ prevents this.
60+
5561## Reflection changes
5662
5763* The implicit coercion from String to TTName was removed.
idris.cabal+5
@@ -328,6 +328,10 @@ Extra-source-files:
328328 test/reg071/run
329329 test/reg071/*.idr
330330 test/reg071/expected
331+ test/reg072/run
332+ test/reg072/*.idr
333+ test/reg072/expected
334+
331335
332336 test/basic001/run
333337 test/basic001/*.idr
@@ -1015,6 +1019,7 @@ Library
10151019 , filepath < 1.5
10161020 , fingertree >= 0.1 && < 0.2
10171021 , haskeline >= 0.7 && < 0.8
1022+ , ieee754 >= 0.7 && < 0.8
10181023 , mtl >= 2.1 && < 2.3
10191024 , network < 2.7
10201025 , optparse-applicative >= 0.11 && < 0.13
src/Idris/Core/TT.hs+26−1
@@ -73,6 +73,8 @@ import qualified Data.Binary as B
7373import Data.Binary hiding (get, put)
7474import Foreign.Storable (sizeOf)
7575
76+import Numeric.IEEE (IEEE (identicalIEEE))
77+
7678import Util.Pretty hiding (Str)
7779
7880data Option = TTypeInTType
@@ -708,7 +710,30 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
708710 | AType ArithTy | StrType
709711 | WorldType | TheWorld
710712 | VoidType | Forgot
711− deriving (Eq, Ord, Data, Typeable)
713+ deriving (Ord, Data, Typeable)
714+
715+-- We need to compare Double using bit-pattern identity rather than
716+-- Haskell's Eq, which equates 0.0 and -0.0, leading to a
717+-- contradiction in the type theory. Bit-pattern identity will also
718+-- avoid similar problems for NaNs.
719+instance Eq Const where
720+ I i == I j = i == j
721+ BI i == BI j = i == j
722+ Fl i == Fl j = identicalIEEE i j
723+ Ch i == Ch j = i == j
724+ Str i == Str j = i == j
725+ B8 i == B8 j = i == j
726+ B16 i == B16 j = i == j
727+ B32 i == B32 j = i == j
728+ B64 i == B64 j = i == j
729+ AType i == AType j = i == j
730+ StrType == StrType = True
731+ WorldType == WorldType = True
732+ TheWorld == TheWorld = True
733+ VoidType == VoidType = True
734+ Forgot == Forgot = True
735+ _ == _ = False
736+
712737{-!
713738deriving instance Binary Const
714739deriving instance NFData Const
test/reg072/DoubleEquality.idrnew file+5
@@ -0,0 +1,5 @@
1+module DoubleEquality
2+
3+oops : Void
4+oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
5+
test/reg072/expectednew file+15
@@ -0,0 +1,15 @@
1+DoubleEquality.idr:4:87:
2+When checking right hand side of oops with expected type
3+ Void
4+
5+When checking argument value to function Prelude.Basics.the:
6+ Type mismatch between
7+ x = x (Type of Refl)
8+ and
9+ negate 0.0 = 0.0 (Expected type)
10+
11+ Specifically:
12+ Type mismatch between
13+ -0.0
14+ and
15+ 0.0
test/reg072/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ DoubleEquality.idr --check
3+rm -f *.ibc