eq 4.2.1 → 4.3

raw patch · 6 files changed

+173/−289 lines, 6 filesdep +type-equalitydep ~basedep ~semigroupoidsPVP ok

version bump matches the API change (PVP)

Dependencies added: type-equality

Dependency ranges changed: base, semigroupoids

API changes (from Hackage documentation)

Files

• .travis.yml +0/−171
• CHANGELOG.markdown +22/−0
• README.markdown +2/−2
• eq.cabal +12/−8
• src/Data/Eq/Type.hs +66/−35
• src/Data/Eq/Type/Hetero.hs +71/−73

@@ -1,171 +0,0 @@-# This Travis job script has been generated by a script via-#-#   haskell-ci '--output=.travis.yml' '--config=cabal.haskell-ci' 'cabal.project'-#-# 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-os: linux-dist: xenial-git:-  # whether to recursively clone submodules-  submodules: false-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-    - $HOME/.hlint-before_cache:-  - rm -fv $CABALHOME/packages/hackage.haskell.org/build-reports.log-  # remove files that are regenerated by 'cabal update'-  - 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-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-before_install:-  - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')-  - WITHCOMPILER="-w $HC"-  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')-  - HCPKG="$HC-pkg"-  - unset CC-  - 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-  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"-  - |-    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:-  - 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 -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} 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 ("0.10",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"])-# EOF

@@ -1,3 +1,25 @@+4.3 [2021.10.31]+----------------+* Generalize the types of `Data.Eq.Type.lower{,2,3}`:++  ```diff+  -lower :: f a := f b -> a := b+  +lower :: f a := g b -> a := b++  -lower2 :: f a c := f b c  -> a := b+  +lower2 :: f a c := g b c' -> a := b++  -lower3 :: f a c d := f b c  d  -> a := b+  +lower3 :: f a c d := g b c' d' -> a := b+  ```++  The types of `Data.Eq.Type.Hetero.lower{,2,3}` have been generalized+  analogously.+* `Data.Eq.Type.Hetero.lower{,2,3}` now have the same order of type variables+  as their counterparts in `Data.Eq.Type`.+* Add an `apply` function to `Data.Eq.Type` and `Data.Eq.Type.Hetero`.+* Drop support for pre-7.0 versions of GHC.+ 4.2.1 [2020.10.01] ------------------ * Allow building with GHC 9.0.

@@ -1,11 +1,11 @@ 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)+[![Hackage](https://img.shields.io/hackage/v/eq.svg)](https://hackage.haskell.org/package/eq) [![Build Status](https://github.com/ekmett/eq/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/eq/actions?query=workflow%3AHaskell-CI)  This package provides a data type that witnesses equality between two types using Leibnizian equality. -It includes a [refinement to the notion of Leibnizian equality by Oleg Kiselyov](http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html) +It includes a [refinement to the notion of Leibnizian equality by Oleg Kiselyov](http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html) that permits it to refine equality using the injectively of type constructors via type families.  Contact Information

@@ -1,6 +1,6 @@ name:          eq category:      Type System-version:       4.2.1+version:       4.3 license:       BSD3 cabal-version: >= 1.10 license-file:  LICENSE@@ -23,13 +23,14 @@              , GHC == 8.2.2              , GHC == 8.4.4              , GHC == 8.6.5-             , GHC == 8.8.3-             , GHC == 8.10.1+             , GHC == 8.8.4+             , GHC == 8.10.7+             , GHC == 9.0.1+             , GHC == 9.2.1  extra-source-files:   .gitignore   .vim.custom-  .travis.yml   CHANGELOG.markdown   README.markdown @@ -44,18 +45,21 @@     TypeOperators    build-depends:-    base          == 4.*,+    base          >= 4.3 && <5,     semigroupoids >= 4 && < 6    exposed-modules:     Data.Eq.Type -  if impl(ghc >= 7.0)-    default-extensions: TypeFamilies-    cpp-options: -DLANGUAGE_TypeFamilies+  -- We always have TypeFamilies, we don't support pre GHC-7 compilers.+  -- TypeFamilies are needed to implement lower combinators.+  default-extensions: TypeFamilies    if impl(ghc >= 8.2)     exposed-modules: Data.Eq.Type.Hetero++  if !impl(ghc >= 7.8)+     build-depends: type-equality >=1 && <2    ghc-options: -Wall   default-language: Haskell2010

@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}+{-# LANGUAGE CPP, Rank2Types, ScopedTypeVariables, TypeOperators #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706 #define LANGUAGE_PolyKinds {-# LANGUAGE PolyKinds #-}@@ -7,10 +7,9 @@ {-# LANGUAGE RoleAnnotations #-} #endif #if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0)-#define HAS_DATA_TYPE_EQUALITY 1-{-# LANGUAGE GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}+#define HAS_DATA_TYPE_COERCION 1 #endif+{-# LANGUAGE GADTs #-}  ----------------------------------------------------------------------------- -- |@@ -37,22 +36,23 @@   , trans   , symm   , coerce+#ifdef LANGUAGE_PolyKinds+  , apply+#endif   -- * Lifting equality   , lift   , lift2, lift2'   , lift3, lift3'-#ifdef LANGUAGE_TypeFamilies   -- * Lowering equality   , lower   , lower2   , lower3-#endif-#ifdef HAS_DATA_TYPE_EQUALITY   -- * 'Eq.:~:' equivalence   -- | "Data.Type.Equality" GADT definition is equivalent in power   , fromLeibniz   , toLeibniz +#ifdef HAS_DATA_TYPE_COERCION   -- * 'Co.Coercion' conversion   -- | Leibnizian equality can be converted to representational equality   , reprLeibniz@@ -64,10 +64,10 @@ import Data.Semigroupoid import Data.Groupoid -#ifdef HAS_DATA_TYPE_EQUALITY+#ifdef HAS_DATA_TYPE_COERCION import qualified Data.Type.Coercion as Co-import qualified Data.Type.Equality as Eq #endif+import qualified Data.Type.Equality as Eq  infixl 4 := @@ -87,6 +87,14 @@ coerce :: a := b -> a -> b coerce f = uncoerce . subst f . Coerce +#ifdef LANGUAGE_PolyKinds+newtype Apply a b f g = Apply { unapply :: f a := g b }++-- | Apply one equality to another, respectively+apply :: f := g -> a := b -> f a := g b+apply fg ab = unapply (subst fg (Apply (lift ab)))+#endif+ -- | Equality forms a category instance Category (:=) where   id = Refl id@@ -127,40 +135,62 @@ lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` lift ef -#ifdef LANGUAGE_TypeFamilies-# ifdef LANGUAGE_PolyKinds-type family Inj  (f :: j -> k)           (a :: k) :: j-type family Inj2 (f :: i -> j -> k)      (a :: k) :: i-type family Inj3 (f :: h -> i -> j -> k) (a :: k) :: h-# else-type family Inj  (f :: * -> *)           (a :: *) :: *-type family Inj2 (f :: * -> * -> *)      (a :: *) :: *-type family Inj3 (f :: * -> * -> * -> *) (a :: *) :: *-# endif+#ifdef LANGUAGE_PolyKinds+-- This is all more complicated than it needs to be. Ideally, we would just+-- write:+--+--   data family Lower (a :: j) (b :: k)+--   newtype instance Lower a (f x) = Lower { unlower :: a := x }+--+--   lower :: forall a b f g. f a := g b -> a := b+--   lower eq = unlower (subst eq (Lower refl :: Lower a (f a)))+--+-- And similarly for Lower{2,3}. Unfortunately, this won't typecheck on+-- GHC 7.6 through 7.10 due to an old typechecker bug. To work around the+-- issue, we must:+--+-- 1. Pass `f` and `g` as explicit arguments to the GenInj{,2,3} type family,+--    and+--+-- 2. Define overlapping instances for GenInj{,2,3}.+--+-- Part (2) of this workaround prevents us from using a data family here, as+-- GHC will reject overlapping data family instances as conflicting.+type family GenInj  (f :: j -> k)           (g :: j -> k)             (x :: k) :: j+type family GenInj2 (f :: i -> j -> k)      (g :: i -> j' -> k)       (x :: k) :: i+type family GenInj3 (f :: h -> i -> j -> k) (g :: h -> i' -> j' -> k) (x :: k) :: h+#else+type family GenInj  (f :: * -> *)           (g :: * -> *)           (x :: *) :: *+type family GenInj2 (f :: * -> * -> *)      (g :: * -> * -> *)      (x :: *) :: *+type family GenInj3 (f :: * -> * -> * -> *) (g :: * -> * -> * -> *) (x :: *) :: *+#endif -type instance Inj  f (f a)     = a-type instance Inj2 f (f a b)   = a-type instance Inj3 f (f a b c) = a+type instance GenInj  f g (f a) = a+type instance GenInj  f g (g b) = b -newtype Lower  f a b = Lower  { unlower  :: Inj  f a := Inj  f b }-newtype Lower2 f a b = Lower2 { unlower2 :: Inj2 f a := Inj2 f b }-newtype Lower3 f a b = Lower3 { unlower3 :: Inj3 f a := Inj3 f b }+type instance GenInj2 f g (f a c)  = a+type instance GenInj2 f g (g b c') = b --- | Type constructors are injective, so you can lower equality through any--- type constructor ...-lower :: forall a b f. f a := f b -> a := b-lower eq = unlower (subst eq (Lower refl :: Lower f (f a) (f a)))+type instance GenInj3 f g (f a c  d)  = a+type instance GenInj3 f g (g b c' d') = b +newtype Lower  f g a x = Lower  { unlower  :: a := GenInj  f g x }+newtype Lower2 f g a x = Lower2 { unlower2 :: a := GenInj2 f g x }+newtype Lower3 f g a x = Lower3 { unlower3 :: a := GenInj3 f g x }++-- | Type constructors are generative and injective, so you can lower equality+-- through any type constructors ...+lower :: forall a b f g. f a := g b -> a := b+lower eq = unlower (subst eq (Lower refl :: Lower f g a (f a)))+ -- | ... in any position ...-lower2 :: forall a b c f. f a c := f b c -> a := b-lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f (f a c) (f a c)))+lower2 :: forall a b f g c c'. f a c := g b c' -> a := b+lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f g a (f a c)))  -- | ... these definitions are poly-kinded on GHC 7.6 and up.-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 (f a c d) (f a c d)))-#endif+lower3 :: forall a b f g c c' d d'. f a c d := g b c' d' -> a := b+lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 f g a (f a c d))) -#ifdef HAS_DATA_TYPE_EQUALITY fromLeibniz :: a := b -> a Eq.:~: b fromLeibniz a = subst a Eq.Refl @@ -170,6 +200,7 @@ instance Eq.TestEquality ((:=) a) where   testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb)) +#ifdef HAS_DATA_TYPE_COERCION reprLeibniz :: a := b -> Co.Coercion a b reprLeibniz a = subst a Co.Coercion 

@@ -1,6 +1,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}@@ -29,6 +30,7 @@   , trans   , symm   , coerce+  , apply   -- * Lifting equality   , lift   , lift2, lift2'@@ -61,7 +63,6 @@ import qualified Data.Type.Equality as Eq import           Data.Kind import qualified Data.Eq.Type as ET-import           GHC.Exts (Any) import           Prelude hiding (id, (.))  infixl 4 :==@@ -78,16 +79,37 @@ refl :: a :== a refl = HRefl id -newtype Coerce (a :: k) = Coerce { uncoerce :: MassageKind Type a }--type family MassageKind (j :: Type) (a :: k) :: j where-  MassageKind j (a :: j) = a-  MassageKind _ _        = Any+data family Coerce :: forall k. k -> Type+newtype instance Coerce (a :: Type) = Coerce { uncoerce :: a }  -- | If two things are equal, you can convert one to the other. coerce :: a :== b -> a -> b coerce f = uncoerce . hsubst f . Coerce +newtype Pair1 :: forall j1 k1 j2.+                 j1 -> k1 -> j2+              -> forall k2. k2 -> Type where+  Pair1 :: { unpair1 :: '(a1, a2) :== '(b1, b2) } -> Pair1 a1 b1 a2 b2++newtype Pair2 :: forall j2 k2 j1.+                 j2 -> k2 -> j1+              -> forall k1. k1 -> Type where+  Pair2 :: { unpair2 :: '(a1, a2) :== '(b1, b2) } -> Pair2 a2 b2 a1 b1++-- | Lift two equalities pairwise.+pair :: a1 :== b1 -> a2 :== b2 -> '(a1, a2) :== '(b1, b2)+pair ab1 ab2 = unpair2 $ hsubst ab1 $ Pair2 $ unpair1 $ hsubst ab2 $ Pair1 refl++data family Apply :: forall j1 j2.+                     (j1 -> j2) -> j1+                  -> forall k. k -> Type+newtype instance Apply (f :: j1 -> j2) (a :: j1) '((g :: k1 -> k2), (b :: k1))+  = Apply { unapply :: f a :== g b }++-- | Apply one equality to another, respectively+apply :: f :== g -> a :== b -> f a :== g b+apply fg ab = unapply $ hsubst (pair fg ab) $ Apply refl+ 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)@@ -123,24 +145,22 @@ symm :: a :== b -> b :== a symm ab = unpush $ unsymm $ hsubst ab $ Symm $ Push refl -newtype Lift :: forall j r.-                (j -> r) -> j-             -> forall k. k-             -> Type where-  Lift :: forall j r k (f :: j -> r) (a :: j) (b :: k).-          { unlift :: f a :== f (MassageKind j b) } -> Lift f a b+data family Lift :: forall j r. (j -> r) -> j+                 -> forall k. k+                 -> Type+newtype instance Lift f (a :: j) (b :: j) =+  Lift { unlift :: f a :== f 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 j2 r.-                 (j1 -> j2 -> r) -> j1 -> j2-              -> forall k. k-              -> Type where-  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+data family Lift2 :: forall j1 j2 r.+                     (j1 -> j2 -> r) -> j1 -> j2+                  -> forall k. k+                  -> Type+newtype instance Lift2 f (a :: j1) (c :: j2) (b :: j1) =+  Lift2 { unlift2 :: f a c :== f b c }  -- | ... in any position. lift2 :: a :== b -> f a c :== f b c@@ -149,13 +169,12 @@ 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 j2 j3 r.-                 (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3-              -> forall k. k-              -> Type where-  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+data family Lift3 :: forall j1 j2 j3 r.+                     (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3+                  -> forall k. k+                  -> Type+newtype instance Lift3 f (a :: j1) (c :: j2) (d :: j3) (b :: j1) =+  Lift3 { unlift3 :: f a c d :== f b c d }  lift3 :: a :== b -> f a c d :== f b c d lift3 f = unlift3 $ hsubst f $ Lift3 refl@@ -163,58 +182,37 @@ lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f lift3' ab cd ef = unpush $ unpush (lift3 ab `hsubst` Push (lift2 cd)) `hsubst` Push (lift ef) -newtype Lower :: Type-              -> 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-  Inj j (f (a :: j)) = a-  Inj _ _            = Any---- | Type constructors are injective, so you can lower equality through any type constructor.-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. 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+data family Lower :: forall j. j+                  -> forall k. k+                  -> Type+newtype instance Lower a (f x) = Lower { unlower :: a :== x } -type family Inj2 (j :: Type) (a :: k) :: j where-  Inj2 j (f (a :: j) b) = a-  Inj2 _ _              = Any+-- | Type constructors are generative and injective, so you can lower equality+-- through any type constructors.+lower :: forall a b f g. f a :== g b -> a :== b+lower f = unlower $ hsubst f (Lower refl :: Lower a (f a)) -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))+data family Lower2 :: forall j. j+                   -> forall k. k+                   -> Type+newtype instance Lower2 a (f x c) = Lower2 { unlower2 :: a :== x } -newtype Lower3 :: Type-               -> 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+lower2 :: forall a b f g c c'. f a c :== g b c' -> a :== b+lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 a (f a c)) -type family Inj3 (j :: Type) (a :: k) :: j where-  Inj3 j (f (a :: j) b c) = a-  Inj3 _ _                = Any+data family Lower3 :: forall j. j+                   -> forall k. k+                   -> Type+newtype instance Lower3 a (f x c d) = Lower3 { unlower3 :: a :== x } -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))+lower3 :: forall a b f g c c' d d'. f a c d :== g b c' d' -> a :== b+lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 a (f a c d)) -newtype Flay :: forall j.-                (j -> j -> Type) -> j-             -> 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+data family Flay :: forall j.+                    (j -> j -> Type) -> j+                 -> forall k. k+                 -> Type+newtype instance Flay p (a :: j) (b :: j) = Flay { unflay :: p a b }  -- | Convert an appropriately kinded heterogeneous Leibnizian equality into -- a homogeneous Leibnizian equality '(ET.:=)'.@@ -233,7 +231,7 @@ toLeibniz Eq.Refl = refl  heteroFromLeibniz :: a :== b -> a Eq.:~~: b-heteroFromLeibniz f = unpush $ hsubst f $ Push $ Eq.HRefl+heteroFromLeibniz f = unpush $ hsubst f $ Push Eq.HRefl  heteroToLeibniz :: a Eq.:~~: b -> a :== b heteroToLeibniz Eq.HRefl = refl