eq 4.2 → 4.2.1

raw patch · 6 files changed

+194/−165 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• .ghci +0/−1
• .travis.yml +140/−114
• CHANGELOG.markdown +4/−0
• eq.cabal +8/−5
• src/Data/Eq/Type.hs +4/−4
• src/Data/Eq/Type/Hetero.hs +38/−41

@@ -1,1 +0,0 @@-:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h

@@ -1,145 +1,171 @@ # 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'+#   haskell-ci '--output=.travis.yml' '--config=cabal.haskell-ci' 'cabal.project' #-# For more information, see https://github.com/hvr/multi-ghc-travis+# To regenerate the script (for example after adjusting tested-with) run #+#   haskell-ci regenerate+#+# For more information, see https://github.com/haskell-CI/haskell-ci+#+# version: 0.10+#+version: ~> 1.0 language: c-sudo: false-+os: linux+dist: xenial git:-  submodules: false  # whether to recursively clone submodules-+  # whether to recursively clone submodules+  submodules: false notifications:   irc:     channels:-      - "irc.freenode.org#haskell-lens"+      - 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-+    - $HOME/.hlint before_cache:-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log+  - rm -fv $CABALHOME/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:+  - rm -fv $CABALHOME/packages/hackage.haskell.org/00-index.*+  - rm -fv $CABALHOME/packages/hackage.haskell.org/*.json+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.cache+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar.idx+  - rm -rfv $CABALHOME/packages/head.hackage+jobs:   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.2"-    # env: TEST=--disable-tests BENCH=--disable-benchmarks-      addons: {apt: {packages: [*apt_packages,cabal-install-2.2,ghc-8.4.2], sources: [hvr-ghc]}}-    - compiler: "ghc-head"-      env: GHCHEAD=true-      addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-head], sources: [hvr-ghc]}}-+    - compiler: ghc-8.10.1+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.10.1","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-8.8.3+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.8.3","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-8.6.5+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.6.5","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-8.4.4+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.4.4","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-8.2.2+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.2.2","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-8.0.2+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.0.2","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.10.3+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.10.3","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.8.4+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.8.4","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.6.3+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.6.3","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.4.2+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.4.2","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.2.2+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.2.2","cabal-install-3.2"]}}+      os: linux+    - compiler: ghc-7.0.4+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.0.4","cabal-install-3.2"]}}+      os: linux   allow_failures:-    - compiler: "ghc-7.0.4"-    - compiler: "ghc-7.2.2"-    - compiler: "ghc-head"-+    - compiler: ghc-7.0.4+    - compiler: ghc-7.2.2 before_install:-  - HC=${CC}-  - HCPKG=${HC/ghc/ghc-pkg}+  - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')+  - WITHCOMPILER="-w $HC"+  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')+  - HCPKG="$HC-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/') ))+  - CABAL=/opt/ghc/bin/cabal+  - CABALHOME=$HOME/.cabal+  - export PATH="$CABALHOME/bin:$PATH"+  - TOP=$(pwd)+  - "HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\\d+)\\.(\\d+)\\.(\\d+)(\\.(\\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')"   - echo $HCNUMVER-+  - CABAL="$CABAL -vnormal+nowrap"+  - set -o pipefail+  - TEST=--enable-tests+  - BENCH=--enable-benchmarks+  - HEADHACKAGE=false+  - rm -f $CABALHOME/config+  - |+    echo "verbose: normal +nowrap +markoutput"          >> $CABALHOME/config+    echo "remote-build-reporting: anonymous"            >> $CABALHOME/config+    echo "write-ghc-environment-files: always"          >> $CABALHOME/config+    echo "remote-repo-cache: $CABALHOME/packages"       >> $CABALHOME/config+    echo "logs-dir:          $CABALHOME/logs"           >> $CABALHOME/config+    echo "world-file:        $CABALHOME/world"          >> $CABALHOME/config+    echo "extra-prog-path:   $CABALHOME/bin"            >> $CABALHOME/config+    echo "symlink-bindir:    $CABALHOME/bin"            >> $CABALHOME/config+    echo "installdir:        $CABALHOME/bin"            >> $CABALHOME/config+    echo "build-summary:     $CABALHOME/logs/build.log" >> $CABALHOME/config+    echo "store-dir:         $CABALHOME/store"          >> $CABALHOME/config+    echo "install-dirs user"                            >> $CABALHOME/config+    echo "  prefix: $CABALHOME"                         >> $CABALHOME/config+    echo "repository hackage.haskell.org"               >> $CABALHOME/config+    echo "  url: http://hackage.haskell.org/"           >> $CABALHOME/config install:-  - cabal --version+  - ${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--      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.+    echo "program-default-options"                >> $CABALHOME/config+    echo "  ghc-options: $GHCJOBS +RTS -M6G -RTS" >> $CABALHOME/config+  - cat $CABALHOME/config+  - rm -fv cabal.project cabal.project.local cabal.project.freeze+  - travis_retry ${CABAL} v2-update -v+  # Generate cabal.project+  - rm -rf cabal.project cabal.project.local cabal.project.freeze+  - touch cabal.project+  - |+    echo "packages: ." >> cabal.project+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> cabal.project ; fi+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"+  - |+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(eq)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"+  - cat cabal.project || true+  - cat cabal.project.local || true+  - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi+  - ${CABAL} v2-freeze $WITHCOMPILER ${TEST} ${BENCH}+  - "cat cabal.project.freeze | sed -E 's/^(constraints: *| *)//' | sed 's/any.//'"+  - rm  cabal.project.freeze+  - travis_wait 40 ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} --dep -j2 all script:-  # test that source-distributions can be generated-  - (cd "." && cabal sdist)-  - mv "."/dist/eq-*.tar.gz ${DISTDIR}/+  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)+  # Packaging...+  - ${CABAL} v2-sdist all+  # Unpacking...+  - mv dist-newstyle/sdist/*.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--+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec tar -xvf '{}' \;+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec rm       '{}' \;+  - PKGDIR_eq="$(find . -maxdepth 1 -type d -regex '.*/eq-[0-9.]*')"+  # Generate cabal.project+  - rm -rf cabal.project cabal.project.local cabal.project.freeze+  - touch cabal.project+  - |+    echo "packages: ${PKGDIR_eq}" >> cabal.project+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> cabal.project ; fi+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"+  - |+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(eq)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"+  - cat cabal.project || true+  - cat cabal.project.local || true+  # Building with tests and benchmarks...   # build & run tests, build benchmarks-  - cabal new-build -w ${HC} ${TEST} ${BENCH} all--  # cabal check-  - (cd eq-* && cabal check)--  # haddock-  - rm -rf ./dist-newstyle-  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi+  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} all+  # cabal check...+  - (cd ${PKGDIR_eq} && ${CABAL} -vnormal check)+  # haddock...+  - ${CABAL} v2-haddock $WITHCOMPILER --with-haddock $HADDOCK ${TEST} ${BENCH} all -# REGENDATA ["-o",".travis.yml","--irc-channel=irc.freenode.org#haskell-lens","--no-no-tests-no-bench","--no-installed","cabal.project"]+# REGENDATA ("0.10",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"]) # EOF

@@ -1,3 +1,7 @@+4.2.1 [2020.10.01]+------------------+* Allow building with GHC 9.0.+ 4.2 [2018.04.24] ---------------- * Make `lower`, `lower2`, and `lower3` in `Data.Eq.Type` poly-kinded.

@@ -1,8 +1,8 @@ name:          eq category:      Type System-version:       4.2+version:       4.2.1 license:       BSD3-cabal-version: >= 1.6+cabal-version: >= 1.10 license-file:  LICENSE author:        Edward A. Kmett maintainer:    Edward A. Kmett <ekmett@gmail.com>@@ -21,10 +21,12 @@              , GHC == 7.10.3              , GHC == 8.0.2              , GHC == 8.2.2-             , GHC == 8.4.2+             , GHC == 8.4.4+             , GHC == 8.6.5+             , GHC == 8.8.3+             , GHC == 8.10.1  extra-source-files:-  .ghci   .gitignore   .vim.custom   .travis.yml@@ -49,11 +51,12 @@     Data.Eq.Type    if impl(ghc >= 7.0)-    extensions: TypeFamilies+    default-extensions: TypeFamilies     cpp-options: -DLANGUAGE_TypeFamilies    if impl(ghc >= 8.2)     exposed-modules: Data.Eq.Type.Hetero    ghc-options: -Wall+  default-language: Haskell2010   hs-source-dirs: src

@@ -59,7 +59,7 @@ #endif   ) where -import Prelude (Maybe(..), flip)+import Prelude (Maybe(..)) import Control.Category import Data.Semigroupoid import Data.Groupoid@@ -90,17 +90,17 @@ -- | Equality forms a category instance Category (:=) where   id = Refl id-  (.) = subst+  bc . ab = subst bc ab  instance Semigroupoid (:=) where-  o = subst+  bc `o` ab = subst bc ab  instance Groupoid (:=) where   inv = symm  -- | Equality is transitive trans :: a := b -> b := c -> a := c-trans = flip subst+trans ab bc = subst bc ab  newtype Symm p a b = Symm { unsymm :: p b a } -- | Equality is symmetric

@@ -15,7 +15,7 @@ -- Stability   :  provisional -- Portability :  GHC ----- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogenous+-- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogeneous -- using higher-rank kinds. -- -- This module is only exposed on GHC 8.2 and later.@@ -71,7 +71,7 @@ -- Leibnizian equality states that two things are equal if you can -- substitute one for the other in all contexts. newtype (a :: j) :== (b :: k)-  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }+  = HRefl { hsubst :: forall (c :: forall i. i -> Type). c a -> c b } type role (:==) nominal nominal  -- | Equality is reflexive.@@ -88,10 +88,10 @@ coerce :: a :== b -> a -> b coerce f = uncoerce . hsubst f . Coerce -newtype Push :: (forall (j :: Type) (k :: Type). j -> k -> Type)-             -> forall (j :: Type). j -> forall (k :: Type). k -> Type where-  Push :: forall (p :: forall (j :: Type) (k :: Type). j -> k -> Type)-                 (j :: Type) (k :: Type) (a :: j) (b :: k).+newtype Push :: (forall j k. j -> k -> Type)+             -> forall j. j -> forall k. k -> Type where+  Push :: forall (p :: forall j k. j -> k -> Type)+                 j k (a :: j) (b :: k).           { unpush :: p a b } -> Push p a b  -- | Equality is compositional.@@ -113,36 +113,32 @@ trans :: a :== b -> b :== c -> a :== c trans = flip comp -newtype Symm :: (forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)-             -> forall (j :: Type). j-             -> forall (k :: Type). k-             -> Type where-  Symm :: forall (p :: forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)-                 (j :: Type) (k :: Type)-                 (a :: j) (b :: k).+newtype Symm :: (forall j. j -> forall k. k -> Type)+             ->  forall j. j -> forall k. k -> Type where+  Symm :: forall (p :: forall j. j -> forall k. k -> Type)+                 j k (a :: j) (b :: k).           { unsymm :: p b a } -> Symm p a b  -- | Equality is symmetric. symm :: a :== b -> b :== a symm ab = unpush $ unsymm $ hsubst ab $ Symm $ Push refl -newtype Lift :: forall (j :: Type) (r :: Type).+newtype Lift :: forall j r.                 (j -> r) -> j-             -> forall (k :: Type). k+             -> forall k. k              -> Type where-  Lift :: forall (j :: Type) (k :: Type) (r :: Type)-                 (f :: j -> r) (a :: j) (b :: k).+  Lift :: forall j r k (f :: j -> r) (a :: j) (b :: k).           { unlift :: f a :== f (MassageKind j b) } -> Lift f a b  -- | You can lift equality into any type constructor... lift :: a :== b -> f a :== f b lift f = unlift $ hsubst f $ Lift refl -newtype Lift2 :: forall (j1 :: Type) (j2 :: Type) (r :: Type).+newtype Lift2 :: forall j1 j2 r.                  (j1 -> j2 -> r) -> j1 -> j2-              -> forall (k :: Type). k+              -> forall k. k               -> Type where-  Lift2 :: forall (j1 :: Type) (j2 :: Type) (k :: Type) (r :: Type)+  Lift2 :: forall j1 j2 r k                   (f :: j1 -> j2 -> r) (a :: j1) (b :: k) (c :: j2).            { unlift2 :: f a c :== f (MassageKind j1 b) c } -> Lift2 f a c b @@ -153,11 +149,11 @@ lift2' :: a :== b -> c :== d -> f a c :== f b d lift2' ab cd = unpush $ lift2 ab `hsubst` Push (lift cd) -newtype Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (r :: Type).+newtype Lift3 :: forall j1 j2 j3 r.                  (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3-              -> forall (k :: Type). k+              -> forall k. k               -> Type where-  Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (k :: Type) (r :: Type)+  Lift3 :: forall j1 j2 j3 r k                   (f :: j1 -> j2 -> j3 -> r) (a :: j1) (b :: k) (c :: j2) (d :: j3).            { unlift3 :: f a c d :== f (MassageKind j1 b) c d } -> Lift3 f a c d b @@ -168,9 +164,10 @@ lift3' ab cd ef = unpush $ unpush (lift3 ab `hsubst` Push (lift2 cd)) `hsubst` Push (lift ef)  newtype Lower :: Type-              -> forall (j :: Type). j-              -> forall (k :: Type). k -> Type where-  Lower :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+              -> forall j. j+              -> forall k. k+              -> Type where+  Lower :: forall i j k (a :: j) (b :: k).            { unlower :: Inj i a :== Inj i (MassageKind j b) } -> Lower i a b  type family Inj (j :: Type) (a :: k) :: j where@@ -178,45 +175,45 @@   Inj _ _            = Any  -- | Type constructors are injective, so you can lower equality through any type constructor.-lower :: forall (j :: Type) (k :: Type) (f :: j -> k) (a :: j) (b :: j).+lower :: forall j k (f :: j -> k) (a :: j) (b :: j).          f a :== f b -> a :== b lower f = unlower $ hsubst f (Lower refl :: Lower j (f a) (f a))  newtype Lower2 :: Type-               -> forall (j :: Type). j-               -> forall (k :: Type). k -> Type where-  Lower2 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+               -> forall j. j+               -> forall k. k+               -> Type where+  Lower2 :: forall i j k (a :: j) (b :: k).             { unlower2 :: Inj2 i a :== Inj2 i (MassageKind j b) } -> Lower2 i a b  type family Inj2 (j :: Type) (a :: k) :: j where   Inj2 j (f (a :: j) b) = a   Inj2 _ _              = Any -lower2 :: forall (i :: Type) (j :: Type) (k :: Type)-                 (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).+lower2 :: forall i j k (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).           f a c :== f b c -> a :== b lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 i (f a c) (f a c))  newtype Lower3 :: Type-               -> forall (j :: Type). j-               -> forall (k :: Type). k -> Type where-  Lower3 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).+               -> forall j. j+               -> forall k. k+               -> Type where+  Lower3 :: forall i j k (a :: j) (b :: k).             { unlower3 :: Inj3 i a :== Inj3 i (MassageKind j b) } -> Lower3 i a b  type family Inj3 (j :: Type) (a :: k) :: j where   Inj3 j (f (a :: j) b c) = a   Inj3 _ _                = Any -lower3 :: forall (h :: Type) (i :: Type) (j :: Type) (k :: Type)-                 (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).+lower3 :: forall h i j k (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).           f a c d :== f b c d -> a :== b lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 h (f a c d) (f a c d)) -newtype Flay :: forall (j :: Type).+newtype Flay :: forall j.                 (j -> j -> Type) -> j-             -> forall (k :: Type). k -> Type where-  Flay :: forall (j :: Type) (k :: Type)-                 (p :: j -> j -> Type) (a :: j) (b :: k).+             -> forall k. k+             -> Type where+  Flay :: forall j k (p :: j -> j -> Type) (a :: j) (b :: k).           { unflay :: p a (MassageKind j b) } -> Flay p a b  -- | Convert an appropriately kinded heterogeneous Leibnizian equality into