eq 4.0.4 → 4.1

raw patch · 6 files changed

+225/−66 lines, 6 filesnew-uploaderPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• .gitignore +18/−0
• .travis.yml +132/−47
• CHANGELOG.markdown +10/−0
• README.markdown +1/−1
• eq.cabal +12/−3
• src/Data/Eq/Type.hs +52/−15

@@ -11,3 +11,21 @@ *.hi *~ *#+.stack-work/+cabal-dev+*.chi+*.chs.h+*.dyn_o+*.dyn_hi+.hpc+.hsenv+.cabal-sandbox/+cabal.sandbox.config+*.prof+*.aux+*.hp+*.eventlog+cabal.project.local+cabal.project.local~+.HTF/+.ghc.environment.*

@@ -1,61 +1,146 @@-# NB: don't set `language: haskell` here+# This Travis job script has been generated by a script via+#+#   runghc make_travis_yml_2.hs '-o' '.travis.yml' '--irc-channel=irc.freenode.org#haskell-lens' '--no-no-tests-no-bench' '--no-installed' 'cabal.project'+#+# For more information, see https://github.com/hvr/multi-ghc-travis+#+language: c+sudo: false -# See also https://github.com/hvr/multi-ghc-travis for more information-env:- # we have to use CABALVER=1.16 for GHC<7.6 as well, as there's- # no package for earlier cabal versions in the PPA- - GHCVER=7.4.2 CABALVER=1.16- - GHCVER=7.6.3 CABALVER=1.16- - GHCVER=7.8.2 CABALVER=1.18- # NOTE: we can't use Cabal 1.20 yet due to- #  https://github.com/haskell/cabal/issues/1806- - GHCVER=head  CABALVER=1.20+git:+  submodules: false  # whether to recursively clone submodules +notifications:+  irc:+    channels:+      - "irc.freenode.org#haskell-lens"+    skip_join: true+    template:+      - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"++cache:+  directories:+    - $HOME/.cabal/packages+    - $HOME/.cabal/store++before_cache:+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log+  # remove files that are regenerated by 'cabal update'+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.*+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx++  - rm -rfv $HOME/.cabal/packages/head.hackage+ matrix:+  include:+    - compiler: "ghc-7.0.4"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.0.4], sources: [hvr-ghc]}}+    - compiler: "ghc-7.2.2"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.2.2], sources: [hvr-ghc]}}+    - compiler: "ghc-7.4.2"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.4.2], sources: [hvr-ghc]}}+    - compiler: "ghc-7.6.3"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.6.3], sources: [hvr-ghc]}}+    - compiler: "ghc-7.8.4"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.8.4], sources: [hvr-ghc]}}+    - compiler: "ghc-7.10.3"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.10.3], sources: [hvr-ghc]}}+    - compiler: "ghc-8.0.2"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.0.2], sources: [hvr-ghc]}}+    - compiler: "ghc-8.2.2"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.2.2], sources: [hvr-ghc]}}+    - compiler: "ghc-8.4.1"+      env: GHCHEAD=true+      addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-8.4.1], sources: [hvr-ghc]}}+    - compiler: "ghc-head"+      env: GHCHEAD=true+      addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-head], sources: [hvr-ghc]}}+   allow_failures:-   - env: GHCVER=head  CABALVER=1.20+    - compiler: "ghc-7.0.4"+    - compiler: "ghc-7.2.2"+    - compiler: "ghc-8.4.1"+    - compiler: "ghc-head" -# Note: the distinction between `before_install` and `install` is not-#       important. before_install:- - travis_retry sudo add-apt-repository -y ppa:hvr/ghc- - travis_retry sudo apt-get update- - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER- - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH- - cabal --version+  - HC=${CC}+  - HCPKG=${HC/ghc/ghc-pkg}+  - unset CC+  - ROOTDIR=$(pwd)+  - mkdir -p $HOME/.local/bin+  - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH"+  - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))+  - echo $HCNUMVER  install:- - travis_retry cabal update- - cabal install --only-dependencies+  - cabal --version+  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"+  - BENCH=${BENCH---enable-benchmarks}+  - TEST=${TEST---enable-tests}+  - HADDOCK=${HADDOCK-true}+  - INSTALLED=${INSTALLED-true}+  - GHCHEAD=${GHCHEAD-false}+  - travis_retry cabal update -v+  - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config"+  - rm -fv cabal.project cabal.project.local+  # Overlay Hackage Package Index for GHC HEAD: https://github.com/hvr/head.hackage+  - |+    if $GHCHEAD; then+      sed -i.bak 's/-- allow-newer:.*/allow-newer: *:base, *:template-haskell, *:ghc, *:Cabal/' ${HOME}/.cabal/config -# Here starts the actual work to be performed for the package under-# test; any command which exits with a non-zero exit code causes the-# build to fail.+      echo 'repository head.hackage'                                                        >> ${HOME}/.cabal/config+      echo '   url: http://head.hackage.haskell.org/'                                       >> ${HOME}/.cabal/config+      echo '   secure: True'                                                                >> ${HOME}/.cabal/config+      echo '   root-keys: 07c59cb65787dedfaef5bd5f987ceb5f7e5ebf88b904bbd4c5cbdeb2ff71b740' >> ${HOME}/.cabal/config+      echo '              2e8555dde16ebd8df076f1a8ef13b8f14c66bad8eafefd7d9e37d0ed711821fb' >> ${HOME}/.cabal/config+      echo '              8f79fd2389ab2967354407ec852cbe73f2e8635793ac446d09461ffb99527f6e' >> ${HOME}/.cabal/config+      echo '   key-threshold: 3'                                                            >> ${HOME}/.cabal.config++      cabal new-update head.hackage -v+    fi+  - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$'+  - "printf 'packages: \".\"\\n' > cabal.project"+  - cat cabal.project+  - if [ -f "./configure.ac" ]; then+      (cd "." && autoreconf -i);+    fi+  - rm -f cabal.project.freeze+  - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all+  - rm -rf "."/.ghc.environment.* "."/dist+  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)++# Here starts the actual work to be performed for the package under test;+# any command which exits with a non-zero exit code causes the build to fail. script:- # -v2 provides useful information for debugging- - cabal configure -v2+  # test that source-distributions can be generated+  - (cd "." && cabal sdist)+  - mv "."/dist/eq-*.tar.gz ${DISTDIR}/+  - cd ${DISTDIR} || false+  - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \;+  - "printf 'packages: eq-*/*.cabal\\n' > cabal.project"+  - cat cabal.project - # this builds all libraries and executables- # (including tests/benchmarks)- - cabal build - # tests that a source-distribution can be generated- - cabal sdist+  # build & run tests, build benchmarks+  - cabal new-build -w ${HC} ${TEST} ${BENCH} all - # check that the generated source-distribution can be built & installed- - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;-   cd dist/;-   if [ -f "$SRC_TGZ" ]; then-      cabal install --force-reinstalls "$SRC_TGZ";-   else-      echo "expected '$SRC_TGZ' not found";-      exit 1;-   fi+  # cabal check+  - (cd eq-* && cabal check) -notifications:-  irc:-    channels:-      - "irc.freenode.org#haskell-lens"-    skip_join: true-    template:-      - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"+  # haddock+  - rm -rf ./dist-newstyle+  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi++# REGENDATA ["-o",".travis.yml","--irc-channel=irc.freenode.org#haskell-lens","--no-no-tests-no-bench","--no-installed","cabal.project"]+# EOF

@@ -1,3 +1,13 @@+4.1+---+* Add `TestEquality` and `TestCoercion` instances for `(:=)`.+* Add `fromLeibniz` and `toLeibniz` functions for converting between `(:~:)`+  (from `Data.Type.Equality`) and `(:=)`.+* Add a `reprLeibniz` function to convert `(:=)` to a `Coercion`+  (i.e., representational equality).+* Make `(:=)` a newtype.+* We can remove the `Trustworthy` claim and infer as `Safe` on modern GHCs.+ 4.0.2 ----- * Made := kind polymorphic.

@@ -1,7 +1,7 @@ eq == -[![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq)+[![Hackage](https://img.shields.io/hackage/v/eq.svg)](https://hackage.haskell.org/package/eq) [![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq)  This package provides a data type that witnesses equality between two types using Leibnizian equality. 

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       4.0.4+version:       4.1 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -11,8 +11,17 @@ bug-reports:   http://github.com/ekmett/eq/issues copyright:     Copyright (C) 2011-2013 Edward A. Kmett synopsis:      Leibnizian equality-description:   Leibnizian equality+description:   Leibnizian equality. build-type:    Simple+tested-with:   GHC == 7.0.4+             , GHC == 7.2.2+             , GHC == 7.4.2+             , GHC == 7.6.3+             , GHC == 7.8.4+             , GHC == 7.10.3+             , GHC == 8.0.2+             , GHC == 8.2.2+             , GHC == 8.4.1  extra-source-files:   .ghci@@ -39,7 +48,7 @@   exposed-modules:     Data.Eq.Type -  if impl(ghc >= 7.0) && impl(ghc < 7.6)+  if impl(ghc >= 7.0)     extensions: TypeFamilies     cpp-options: -DLANGUAGE_TypeFamilies 

@@ -1,13 +1,15 @@ {-# LANGUAGE CPP, Rank2Types, TypeOperators #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706 {-# LANGUAGE PolyKinds #-} #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 {-# LANGUAGE RoleAnnotations #-} #endif+#if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0)+#define HAS_DATA_TYPE_EQUALITY 1+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+#endif  ----------------------------------------------------------------------------- -- |@@ -20,7 +22,7 @@ -- Portability :  rank2 types, type operators, (optional) type families -- -- Leibnizian equality. Injectivity in the presence of type families--- is provided by a generalization of a trick by Oleg Kiselyv posted here:+-- is provided by a generalization of a trick by Oleg Kiselyov posted here: -- -- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html> ----------------------------------------------------------------------------@@ -44,18 +46,33 @@   , lower2   , lower3 #endif+#ifdef HAS_DATA_TYPE_EQUALITY+  -- * 'Eq.:~:' equivalence+  -- | "Data.Type.Equality" GADT definition is equivalent in power+  , fromLeibniz+  , toLeibniz++  -- * 'Co.Coercion' conversion+  -- | Leibnizian equality can be converted to representational equality+  , reprLeibniz+#endif   ) where -import Prelude (flip)+import Prelude (Maybe(..), flip) import Control.Category import Data.Semigroupoid import Data.Groupoid +#ifdef HAS_DATA_TYPE_EQUALITY+import qualified Data.Type.Coercion as Co+import qualified Data.Type.Equality as Eq+#endif+ infixl 4 :=  -- | Leibnizian equality states that two things are equal if you can--- substite one for the other in all contexts-data a := b = Refl { subst :: forall c. c a -> c b }+-- substitute one for the other in all contexts+newtype a := b = Refl { subst :: forall c. c a -> c b } #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 type role (:=) nominal nominal #endif@@ -110,24 +127,44 @@ lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` lift ef  #ifdef LANGUAGE_TypeFamilies-type family Inj f+type family Inj (f :: *) :: * type instance Inj (f a) = a newtype Lower a b = Lower { unlower :: Inj a := Inj b } -- | Type constructors are injective, so you can lower equality through any type constructor-lower :: f a := f b -> a := b+lower :: forall (a :: *) (b :: *) (f :: * -> *). f a := f b -> a := b lower eq = unlower (subst eq (Lower refl :: Lower (f a) (f a))) -type family Inj2 f-type instance Inj2 (f a b) = a+type family Inj2 (f :: *) :: *+type instance Inj2 (f a (b :: *)) = a newtype Lower2 a b = Lower2 { unlower2 :: Inj2 a := Inj2 b } -- | ... in any position-lower2 :: f a c := f b c -> a := b+lower2 :: forall (a :: *) (b :: *) (c :: *) (f :: * -> * -> *).+    f a c := f b c -> a := b lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 (f a c) (f a c))) -type family Inj3 f-type instance Inj3 (f a b c) = a+type family Inj3 (f :: *) :: *+type instance Inj3 (f a (b :: *) (c :: *)) = a newtype Lower3 a b = Lower3 { unlower3 :: Inj3 a := Inj3 b }-lower3 :: f a c d := f b c d -> a := b+-- | But unfortunately these definitions aren't polykinded. Everything is just a star.+lower3 :: forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> * -> *).+    f a c d := f b c d -> a := b lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 (f a c d) (f a c d))) +#endif++#ifdef HAS_DATA_TYPE_EQUALITY+fromLeibniz :: a := b -> a Eq.:~: b+fromLeibniz a = subst a Eq.Refl++toLeibniz :: a Eq.:~: b -> a := b+toLeibniz Eq.Refl = refl++instance Eq.TestEquality ((:=) a) where+  testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb))++reprLeibniz :: a := b -> Co.Coercion a b+reprLeibniz a = subst a Co.Coercion++instance Co.TestCoercion ((:=) a) where+  testCoercion fa fb = Just (reprLeibniz (trans (symm fa) fb)) #endif