4079f54 · Idris-dev · git.iko.soy

CHANGELOG.md+6

compare with master

unifiedsplit

@@ -52,6 +52,12 @@

52 Java codegen and has now been deprecated, together with the

53 corresponding `--mvn` option.

54

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+

55## Reflection changes

61## Reflection changes

56

62

57* The implicit coercion from String to TTName was removed.

63* The implicit coercion from String to TTName was removed.

idris.cabal+5

@@ -328,6 +328,10 @@ Extra-source-files:

328 test/reg071/run

329 test/reg071/*.idr

330 test/reg071/expected

331+ test/reg072/run

332+ test/reg072/*.idr

333+ test/reg072/expected

334+

331

335

332 test/basic001/run

336 test/basic001/run

333 test/basic001/*.idr

337 test/basic001/*.idr

@@ -1015,6 +1019,7 @@ Library

1015 , filepath < 1.5

1019 , filepath < 1.5

1016 , fingertree >= 0.1 && < 0.2

1020 , fingertree >= 0.1 && < 0.2

1017 , haskeline >= 0.7 && < 0.8

1021 , haskeline >= 0.7 && < 0.8

1022+ , ieee754 >= 0.7 && < 0.8

1018 , mtl >= 2.1 && < 2.3

1023 , mtl >= 2.1 && < 2.3

1019 , network < 2.7

1024 , network < 2.7

1020 , optparse-applicative >= 0.11 && < 0.13

1025 , optparse-applicative >= 0.11 && < 0.13

src/Idris/Core/TT.hs+26−1

@@ -73,6 +73,8 @@ import qualified Data.Binary as B

73import Data.Binary hiding (get, put)

74import Foreign.Storable (sizeOf)

75

76+import Numeric.IEEE (IEEE (identicalIEEE))

77+

76import Util.Pretty hiding (Str)

78import Util.Pretty hiding (Str)

77

79

78data Option = TTypeInTType

80data Option = TTypeInTType

@@ -708,7 +710,30 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

708 | AType ArithTy | StrType

710 | AType ArithTy | StrType

709 | WorldType | TheWorld

711 | WorldType | TheWorld

710 | VoidType | Forgot

712 | 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+

712{-!

737{-!

713deriving instance Binary Const

738deriving instance Binary Const

714deriving instance NFData Const

739deriving 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