coerce-with-substitution (empty) → 0.0.0.0

raw patch · 4 files changed

+813/−0 lines, 4 filesdep +base

Dependencies added: base

Files

• CHANGELOG.md +5/−0
• LICENSE +29/−0
• coerce-with-substitution.cabal +60/−0
• src/Data/CoerceSubst.hs +719/−0

@@ -0,0 +1,5 @@+# Revision history for coerce-with-substitution++## 0.0.0.0 -- 2025-07-21++* Proof of concept release.

@@ -0,0 +1,29 @@+Copyright (c) 2025, Ryan Hendrickson+++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of the copyright holder nor the names of its+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,60 @@+cabal-version:      3.4+name:               coerce-with-substitution+version:            0.0.0.0+synopsis:           Coercions with improved type inference+description:+    This package defines aliases of 'Data.Coerce.coerce' and+    'Unsafe.Coerce.unsafeCoerce' that accept a type argument containing type+    substitutions, creating a relationship between the argument and result+    types of the coercion that GHC can use when inferring one type from the+    other.++    See "Data.CoerceSubst" for a full introduction to this package.++    Requires GHC 9.6 or later, due to use of the+    [`TypeData`](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_data.html)+    extension.+license:            BSD-3-Clause+license-file:       LICENSE+author:             Ryan Hendrickson+maintainer:         contact-project+rhendric-haskell-coerce-with-substitution-71023049-issue-@incoming.gitlab.com+homepage:           https://gitlab.com/rhendric/haskell-coerce-with-substitution+bug-reports:        https://gitlab.com/rhendric/haskell-coerce-with-substitution/-/issues+copyright:          © 2025 Ryan Hendrickson+category:           Development+build-type:         Simple+extra-doc-files:    CHANGELOG.md+tested-with:        GHC == { 9.12.2, 9.10.2, 9.8.4, 9.6.7, 9.6.1 }++source-repository head+    type: git+    location: https://gitlab.com/rhendric/haskell-coerce-with-substitution.git++library+    hs-source-dirs:   src+    exposed-modules:  Data.CoerceSubst+    build-depends:    base >=4.7 && <5+    ghc-options:+        -fprint-unicode-syntax+        -haddock+        -Wall+        -Wcompat+        -Winvalid-haddock+        -Wmissing-export-lists+        -Woperator-whitespace+        -Wunused-packages+        -Wunused-type-patterns+    if impl(ghc >= 9.10.1)+        ghc-options:+            -Wmissing-poly-kind-signatures+    default-language: GHC2021+    default-extensions:+        AllowAmbiguousTypes,+        DataKinds,+        FunctionalDependencies,+      NoImplicitPrelude,+      NoStarIsType,+        TypeData,+        TypeFamilies,+        UndecidableInstances,+        UnicodeSyntax,

@@ -0,0 +1,719 @@+{-# LANGUAGE CPP #-}+{-# OPTIONS_HADDOCK redact-type-synonyms #-}+-- |+-- Copyright: © 2025 Ryan Hendrickson+-- License: BSD-3-Clause+-- +-- This module exposes two functions, 'coerceSubst' and 'unsafeCoerceSubst',+-- which are aliases for 'coerce' and 'unsafeCoerce' respectively. Use these+-- functions to help guide type inference for the types you are coercing.+--+module Data.CoerceSubst (+  -- * Motivation++  -- $motivation++  -- * Reference+  coerceSubst,+  -- $basicRef+  type (↦), (:\), (:/),+  -- $injectiveIntroduction+  type (↦!), (:\!), (:/!),+  -- $injectiveRef++  -- ** Advanced usage+  -- $advancedRef++  -- *** @To@ and @Un@+  -- $asUnIntroduction+  To, Un, ToI, UnI,+  -- $polymorphicToUn+  To_, Un_, ToI_, UnI_,++  -- *** @Within@+  -- $withinIntroduction+  Within,+  -- $withinRef++  -- ** Unsafe+  unsafeCoerceSubst,+  -- $unsafeRef++  -- ** Auxiliary types+  Subst,+  Substitute,+) where++import Data.Bool (Bool(..))+import Data.Coerce (Coercible, coerce)+import Data.Kind (Constraint)+import Data.Type.Equality (type (~))+import GHC.List (List)+import GHC.TypeLits (type (-))+import Numeric.Natural (Natural)+import Unsafe.Coerce (unsafeCoerce)++#ifdef DOCTEST+import Prelude++import Control.Applicative (Const(..), ZipList(..))+import Data.Kind (Type)+import Data.Ord (Down(..))+#endif+++infix 6 ↦, :\, :/, ↦!, :\!, :/!++-- $setup+--+-- >>> :set -XQuantifiedConstraints+-- >>> :{+-- >>> -- (This omits features irrelevant to the demonstration.)+-- >>> class Constrained (f :: Type -> Type) where+-- >>>   type Dom f (a :: Type) :: Constraint+-- >>>   type Dom f a = ()+-- >>> class Constrained f => CFunctor f+-- >>> class CFunctor m => CBind m where+-- >>>   (>>-) :: (Dom m a, Dom m b) => m a -> (a -> m b) -> m b+-- >>> newtype WrapFunctor f (a :: Type) = WrapFunctor {runFunctor :: f a}+-- >>> instance Constrained (WrapFunctor f) where+-- >>>   type Dom (WrapFunctor f) a = ()+-- >>> instance Functor f => CFunctor (WrapFunctor f)+-- >>> :}++-- $motivation+--+-- The type signature of 'coerce' does nothing to relate the argument and+-- result types to each other. If both types are already known to the compiler,+-- this is fine:+--+-- > coerceMaybe ∷ Maybe A → Maybe B+-- > coerceMaybe = coerce+--+-- But if you are leaning on the compiler to infer one or both types, using+-- 'coerce' to greatest effect can be frustrating. Take+-- [this](/package/subcategories-0.2.1.1/docs/src/Control.Subcategory.Bind.html#line-37)+-- example from the @subcategories@ package:+--+-- > instance (Monad m) => CBind (WrapFunctor m) where+-- >   (>>-) :: forall a b.+-- >            WrapFunctor m a+-- >         -> (a -> WrapFunctor m b) -> WrapFunctor m b+-- >   (>>-) = coerce @(m a -> (a -> m b) -> m b) (>>=)+--+-- All that type information is there because 'coerce' does nothing to relate+-- the type of @(>>=)@ to the expected type of @(>>-)@. But the only piece of+-- information that the compiler is missing is that the result of the coercion+-- is the type of @(>>=)@, but with @m@ replaced by @WrapFunctor m@.+-- +-- 'coerceSubst' allows for that information to be encoded directly, with less+-- ceremony and more clarity:+--+-- >>> :{+-- >>> instance (Monad m) => CBind (WrapFunctor m) where+-- >>>   (>>-) = coerceSubst @'[m ↦! WrapFunctor m] (>>=)+-- >>> :}++-- $basicRef+--+-- The first type argument to 'coerceSubst' is a list of substitutions. Simple+-- substitutions can be written as @original '↦' replacement@.+--+-- >>> coerceSubst @'[Bool ↦ Down Bool] (True, False, 'x')+-- (Down True,Down False,'x')+--+-- For the Unicode-averse, two alternate spellings are provided:+--+--   * @replacement ':/' original@ is inspired by the other notation frequently+--     used for substitutions (\(M[N/x]\), in which free occurrences of \(x\)+--     in \(M\) are to be replaced with \(N\)).+--   * @original ':\' replacement@ mirrors the above to match the left-to-right+--     order of '↦'.+--+-- >>> coerceSubst @'[Bool :\ Down Bool] (True, False, 'x')+-- (Down True,Down False,'x')+--+-- (I couldn't make up my mind which is best so you get all three.)++-- $injectiveIntroduction+--+-- However it is written, the effect of a substitution is to start with the+-- type of the argument of 'coerceSubst', and replace every occurrence of the+-- ‘original’ type with the ‘replacement’ type. The result is the type of the+-- result of 'coerceSubst'.+--+-- This presumes that the type of the argument is known, and the type of the+-- result is to be inferred. Sometimes, the opposite is the case. For such+-- cases, a substitution operator can be marked as /injective/ with a @!@+-- character. An injective substitution will additionally look for occurrences+-- of the /replacement/ type in the type of the /result/, and+-- reverse-substitute them into the argument type.++-- $injectiveRef+--+-- An example of this was shown in the Motivation section, above. Without the+-- injectivity marker, GHC would not infer that the @(>>=)@ operator is to be+-- instantiated at the type @m@. With it, GHC can infer this by working+-- backwards from the occurrences of @WrapFunctor m@ in the expected type of+-- @(>>-)@.+--+-- (Not all substitutions should be injective! You may want to coerce multiple+-- types to the same ‘replacement’ type, or there may be existing occurrences+-- of a ‘replacement’ type in the input.)++-- $advancedRef+--+-- Substitutions that match a whole type take precedence over substitutions+-- that match a part of a type. In this next example, see how the @Const Bool+-- Int@ value is not translated by the first substitution into a @Const (Down+-- Bool) Int@, because the second substitution takes precedence.+--+-- >>> coerceSubst @[Bool ↦ Down Bool, Const Bool Int ↦ Bool] (True, Const @_ @Int False)+-- (Down True,False)+--+-- (Aside: the @'@ character that appeared in the examples before this one is+-- for+-- [distinguishing](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/data_kinds.html#distinguishing-between-types-and-constructors)+-- between @[a]@, a list with @a@ as its single element, and @[a]@, the type of+-- lists of @a@. It is optional if you compile with+-- [@NoListTuplePuns@](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/data_kinds.html#unique-syntax-for-type-level-lists-and-tuples),+-- or if the list of substitutions has more than one element, as in this most+-- recent example.)+--+-- This behavior can be used to ‘protect’ a type from another substitution via+-- an identity substitution. In this example, 'Data.String.String' is a+-- specific kind of 'List' that we don't want to become a+-- 'Control.Applicative.ZipList'.+--+-- >>> coerceSubst @[String ↦ String, [] ↦ ZipList] ("hello", [True])+-- ("hello",ZipList {getZipList = [True]})+--+-- Once part of a type has been substituted, that part is not considered for+-- any further substitutions. In other words, multiple substitutions can be+-- thought of as executed in parallel, not in sequence.+--+-- >>> coerceSubst @[Bool ↦ Down Bool, Down Bool ↦ Bool] (True, Down False)+-- (Down True,False)+--+-- If two substitutions have the same ‘original’ type, the earlier substitution+-- takes precedence.+--+-- >>> coerceSubst @[Bool ↦ Down Bool, Bool ↦ Const Bool Int] True+-- Down True+--+-- Likewise if two injective substitutions have the same ‘replacement’ type.+--+-- >>> coerceSubst @[Down Bool ↦! Bool, Const Bool Int ↦! Bool] (read "Down True") ∷ Bool+-- True+-- >>> coerceSubst @[Down Bool ↦! Bool, Const Bool Int ↦! Bool] (read "Const True") ∷ Bool+-- *** Exception: Prelude.read: no parse+--+-- Order in a substitution list doesn't matter otherwise.+--+-- (This is little more than a curiosity with only simple substitutions, but+-- will become more relevant when 'Within' substitutions are introduced.)+--+-- Finally, a known limitation: A polykinded type can't be substituted in its+-- general form; it must be instantiated at each kind for which it is used. (If+-- only one side of the substitution is polykinded, you won't need to worry+-- about this, as the kind of '(↦)' ensures that both operands have the same+-- kind.)++-- $asUnIntroduction+--+-- A very common case for coercions is wrapping and unwrapping newtypes. It+-- isn't terribly burdensome to write these out as substitutions in some cases+-- (@Bool '↦' Down Bool@, as an example we have seen several times already).+-- However, you may not want to write out @(Int, String, Bool) '↦' Down (Int,+-- String, Bool)@ in full, with a complex type repeated unnecessarily. Some+-- newtypes use their type parameters multiple times, increasing the+-- duplication.+--+-- For such cases, this module offers the following convenience types.++-- $polymorphicToUn+--+-- The above conveniences work for 'Data.Kind.Type'-kinded substitutions.+-- Function-kinded substitutions, which replace type constructors instead of+-- ground types, can also be expressed with a similar shorthand.+--+-- As a demonstration, the example given in the Motivation section used the+-- substitution @m '↦!' WrapFunctor m@. @WrapFunctor@ is a newtype, but we+-- can't use 'ToI' with this wrapping operation because @m@ and @WrapFunctor m@+-- are function-kinded. But we can use the polymorphic version, 'ToI_',+-- providing (as a ‘subscript’) the number of parameters over which to be+-- polymorphic.+--+-- >>> :{+-- >>> instance (Monad m) => CBind (WrapFunctor m) where+-- >>>   (>>-) = coerceSubst @'[ToI_ 1 ('WrapFunctor @m)] (>>=)+-- >>> :}+--+-- As in the 'Data.Kind.Type'-kinded case, this is exactly equivalent to @m+-- '↦!' WrapFunctor m@, and in such a simple case one is likely to prefer to+-- write @m@ twice instead of using this more advanced (and longer!)+-- ‘shorthand’.+--+-- Note that while @WrapFunctor@ has two type parameters, since the last one is+-- being abstracted away, only the @\@m@ needs to be written out. In general,+-- if \(n\) is the subscript, you shouldn't need to explicitly instantiate the+-- last \(n\) type parameters. (If you do, they are ignored.)++-- $withinIntroduction+--+-- In more complex scenarios, you may not want to substitute everywhere inside+-- a type. The 'Within' combinator allows some substitutions to be active only+-- in the arguments to a provided type constructor, which acts as a selector.+--+-- >>> x = (True, Left False ∷ Either Bool Int)+-- >>> coerceSubst @'[Within Either '[Bool ↦ Down Bool]] x+-- (True,Left (Down False))++-- $withinRef+--+-- A 'Within' combinator, when active, behaves as if expanded to its contents+-- in place. For example, any substitutions that follow the 'Within' will be+-- considered after the contents of the 'Within'. In this next example, because+-- the 'Within' precedes the @Bool '↦' Const Bool Int@ substitution, the @Bool+-- '↦' Down Bool@ substitution takes precedence inside the pair, while the+-- @Bool '↦' Const Bool Int@ has an effect outside of it.+--+-- >>> x = (False, ([True], [True]), [False])+-- >>> coerceSubst @[Within (,) '[Bool ↦ Down Bool], Bool ↦ Const Bool Int] x+-- (Const False,([Down True],[Down True]),[Const False])+--+-- The 'Within' would not have any effect in the opposite order.+--+-- >>> x = (False, ([True], [True]), [False])+-- >>> coerceSubst @[Bool ↦ Down Bool, Within (,) '[Bool ↦ Const Bool Int]] x+-- (Down False,([Down True],[Down True]),[Down False])+--+-- The selector of a 'Within' can be any type-level expression, including+-- compounds formed by applying a constructor to other type expressions, but+-- keep in mind that the effect of the 'Within' is on the selector's arguments,+-- not types in the selector itself. Notice how in this example, the selector+-- @(,) Bool@ causes the payload of the 'Within' to apply to the second element+-- of the pair, but not the first.+--+-- >>> coerceSubst @'[Within ((,) Bool) '[Bool ↦ Down Bool]] (False, True)+-- (False,Down True)+--+-- The type of the pair is @(,) Bool Bool@, and only the second @Bool@ is in+-- the argument of the selector @(,) Bool@. The first @Bool@ is /part/ of the+-- selector.+--+-- You can even use type parameters as 'Within' selectors, though in such+-- circumstances you will need to ensure that the relevant 'Coercible'+-- instances are available.+--+-- >>> :{+-- >>> example ∷ ∀ f g a.+-- >>>   (∀ b b'. Coercible b b' ⇒ Coercible (f (g b)) (f (g b'))) ⇒+-- >>>   Show (a, f (g (Down a))) ⇒+-- >>>   (a, f (g a)) →+-- >>>     String+-- >>> example = show . coerceSubst @'[Within g '[a ↦ Down a]]+-- >>> :}+--+-- 'Within' selectors are always matched against the argument type, even if the+-- selector is also substituted to another type constructor.+--+-- >>> coerceSubst @'[Within [] '[Bool ↦ Down Bool], [] ↦ ZipList] (False, [True])+-- (False,ZipList {getZipList = [Down True]})+--+-- This remains the case even when injective substitutions are used; the 'Within'+-- matches the argument type, even though an injective substitution could cause+-- inference of the argument type to be driven by the result type.+--+-- >>> :{+-- >>> coerceSubst @'[Within [] '[Bool ↦! Down Bool], [] ↦! ZipList]+-- >>>   (read "(False, [True])")+-- >>>   ∷ (Bool, ZipList (Down Bool))+-- >>> :}+-- (False,ZipList {getZipList = [Down True]})+--+-- 'Within's can be nested, resulting in substitutions that will take effect+-- only if multiple selectors are matched in the correct order.+--+-- >>> x = ([(True, True)], ([False], [False]), ())+-- >>> coerceSubst @'[Within [] '[Within (,) '[Bool ↦ Down Bool]]] x+-- ([(Down True,Down True)],([False],[False]),())++-- $unsafeRef+--+-- All of the above applies equally to 'unsafeCoerceSubst' (except for+-- requiring 'Coercible' instances), though with this function you gain the+-- ability to do less safe things, like coercing through an unknown+-- 'Data.Functor.Functor'.+--+-- >>> caution = unsafeCoerceSubst @'[Bool ↦ Down Bool] . fmap even+-- >>> :t caution+-- caution ∷ (Functor f', Integral a) ⇒ f' a → f' (Down Bool)+-- >>> caution [3..5] -- not so dangerous on lists!+-- [Down False,Down True,Down False]++-- | The kind of an element in the type substitution DSL.+--+-- To make 'Subst's, see '(↦)', '(:\)', '(:/)', '(↦!)', '(:\!)', '(:/!)', 'To',+-- 'Un', 'ToI', 'UnI', 'To_', 'Un_', 'ToI_', 'UnI_', and 'Within'.+type data Subst+  = ∀ k. k :\ k+    -- ^ An alternate spelling of '↦', representing a substitution replacing+    -- the left operand with the right.++  | ∀ k. k :\! k+    -- ^ An alternate spelling of '↦!', representing an injective substitution+    -- replacing the left operand with the right.++  | ∀ k. Within k (List Subst)+    -- ^ A list of substitutions scoped to take effect only within arguments to+    -- the provided type expression.++-- | A simple substitution, replacing the left operand with the right.+type (↦) ∷ ∀ k. k → k → Subst+type (↦) = (:\)++-- | A simple injective substitution, replacing the left operand with the+-- right.+type (↦!) ∷ ∀ k. k → k → Subst+type (↦!) = (:\!)++-- | A reversed spelling of '↦', representing a substitution replacing the+-- /right/ operand with the /left/.+type (:/) ∷ ∀ k. k → k → Subst+type a :/ b = b ↦ a++-- | A reversed spelling of '↦!', representing a injective substitution+-- replacing the /right/ operand with the /left/.+type (:/!) ∷ ∀ k. k → k → Subst+type a :/! b = b ↦! a++-- | An alias for 'coerce' that accepts a type-level list of type substitutions+-- to perform. As with 'coerce', the compiler will check that the argument and+-- result types are safely coercible using the 'Coercible' constraint, and the+-- coercion is free of cost at run time.+coerceSubst ∷ ∀ σ a b. Substitute σ a b ⇒ Coercible a b ⇒ a → b+coerceSubst = coerce+{-# INLINE coerceSubst #-}++-- | Just like 'coerceSubst', but without the compiler-checked guarantee that+-- the argument and result types are safely coercible.+unsafeCoerceSubst ∷ ∀ σ a b. Substitute σ a b ⇒ a → b+unsafeCoerceSubst = unsafeCoerce+{-# INLINE unsafeCoerceSubst #-}+++-- | As a shorthand for the common case of substituting a type with a newtype+-- that wraps it, you can write @'To' 'MkNewtype@. The argument to 'To' should+-- be the promoted data constructor for the newtype, not the newtype's type+-- constructor (in many cases, these names are punned, and the @'@ is necessary+-- to disambiguate them).+--+-- If the constructor is polymorphic, you must instantiate all of its type+-- parameters, as in this example.+--+-- >>> coerceSubst @'[To ('Down @(String, Bool))] (("a", True), ("b", False))+-- (Down ("a",True),Down ("b",False))+--+-- This is a bit more concise than the equivalent @(String, Bool) '↦' Down+-- (String, Bool)@, but may look less natural. The trade-off is yours to make.+type To (_con ∷ a → b) = a ↦ b++-- | Like 'To', but injective.+type ToI (_con ∷ a → b) = a ↦! b+-- $+-- >>> f x = coerceSubst @'[ToI ('Down @(String, Bool))] x ∷ (Down (String, Bool), Bool)+-- >>> f $ read "((\"a\", True), False)"+-- (Down ("a",True),False)++-- | Like 'To', but for unwrapping a newtype.+--+-- >>> coerceSubst @'[Un ('Down @(String, Bool))] (Down ("a", True), Down ("b", False))+-- (("a",True),("b",False))+type Un (_con ∷ a → b) = b ↦ a++-- | Like 'Un', but injective.+type UnI (_con ∷ a → b) = b ↦! a+-- $+-- >>> f x = coerceSubst @'[UnI ('Down @(String, Bool))] x ∷ ((String, Bool), Bool)+-- >>> f $ read "(Down (\"a\", True), False)"+-- (("a",True),False)++-- | A variant of 'To' for polymorphic substitution, accepting the number of+-- type arguments over which to abstract. @'To_' 0 'Con@ is equivalent to @'To'+-- 'Con@.+type To_ n (_con ∷ a → b) = MkTo_ False n a b+-- $+-- >>> coerceSubst @'[To_ 1 'ZipList] ("a", ([True], False))+-- (ZipList {getZipList = "a"},(ZipList {getZipList = [True]},False))++-- | Like 'To_', but injective. @'ToI_' 0 'Con@ is equivalent to @'ToI' 'Con@.+type ToI_ n (_con ∷ a → b) = MkTo_ True n a b+-- $+-- >>> f x = coerceSubst @'[ToI_ 1 'ZipList] x ∷ (ZipList Char, (ZipList Bool, Bool))+-- >>> f $ read "(\"a\", ([True], False))"+-- (ZipList {getZipList = "a"},(ZipList {getZipList = [True]},False))++-- | Like 'To_', but for unwrapping a newtype. @'Un_' 0 'Con@ is equivalent to+-- @'Un' 'Con@.+type Un_ n (_con ∷ a → b) = MkTo_ False n b a+-- $+-- >>> coerceSubst @'[Un_ 1 'ZipList] (ZipList "a", (ZipList [True], False))+-- ("a",([True],False))++-- | Like 'Un_', but injective. @'UnI_' 0 'Con@ is equivalent to @'UnI' 'Con@.+type UnI_ n (_con ∷ a → b) = MkTo_ True n b a+-- $+-- >>> f x = coerceSubst @'[UnI_ 1 'ZipList] x ∷ (String, ([Bool], Bool))+-- >>> f $ read "(ZipList {getZipList = \"a\"}, (ZipList {getZipList = [True]}, False))"+-- ("a",([True],False))++-- | The shared implementation of polymorphic 'To_', 'ToI_', 'Un_', and 'UnI_'.+type MkTo_ ∷ ∀ k. Bool → Natural → k → k → Subst+type family MkTo_ inj n a b where+  MkTo_ False 0 a b = a ↦ b+  MkTo_ True 0 a b = a ↦! b+  MkTo_ inj n (f x) (g x) = MkTo_ inj (n - 1) f g+++-- What follows is hideous, and I make no apologies for it.+--+-- The type-level computation needed to perform substitutions is, when+-- distilled into a more familiar term-level pseudocode form, not very+-- complicated.+--+-- > substitute ∷ ∀ k₀. List Subst → k₀ → k₀ → Constraint+-- > substitute σ₀ = go σ₀+-- >   where+-- >   go ∷ ∀ k. List Subst → k → k → Constraint+-- >   go = \cases+-- >     (from ↦  to : _) arg res | from ~ arg → to ~ res+-- >     (from ↦! to : _) arg res | from ~ arg → to ~ res+-- >                              | to ~ res → from ~ arg+-- >     (_ : σ) arg res → go σ arg res+-- >     [] (f a) res → ∃ f' a'.+-- >       (substitute σ₀ f f', substitute (expand σ₀ f) a a', f' a' ~ res)+-- >     [] arg (f b) → ∃ f' b'.+-- >       (substitute σ₀ f' f, substitute (expand σ₀ f') b' b, arg ~ f' b')+-- >     [] arg res → arg ~ res+-- > +-- > expand ∷ ∀ k₀. List Subst → k₀ → List Subst+-- > expand (Within w_f w_σ : σ) f₀ = doWithin f₀+-- >   where+-- >   doWithin ∷ ∀ k. k → List Subst+-- >   doWithin = \case+-- >     f | w_f ~ f → w_σ ++ σ'+-- >     (f _) → doWithin f+-- >     _ → Within w_f w_σ : σ'+-- >   σ' = expand σ f₀+-- > expand (s : σ) f = s : expand σ f+-- > expand [] _ = []+--+-- As much as possible of the above has been translated into type families. One+-- might ask, why not all of it? To which I would reply, type families have no+-- ability to do incoherent matches, which would make this module unusable with+-- parameterized types. There are a few places in the above where I have+-- written pseudocode representing testing two types for equality, or+-- decomposing a type into an @f a@ application. One can encode these matches+-- with type families, but the resulting type gets stuck in cases like @IsEq a+-- Char@ (@IsEq@ being the notional type-family-based equality tester), because+-- the compiler will nobly insist on not telling us any convenient lies. (@a@+-- /could/ be @Char@!)+--+-- So instead I am incorporating incoherent instances with functional+-- dependencies, which enable a more allistic disposition on such questions as+-- whether @a@ and @Char@ are the same (‘shut up nerd, they aren't’). They are+-- also, sadly, much more verbose and difficult to write (not to mention read),+-- so rather than encode the entire type-level algorithm in class instances, I+-- have put the bulk of the pattern matching and control flow into a+-- 'Constraint'-kinded closed type family named, uncreatively, 'Eval', which+-- dispatches on a single 'Expr'. (‘Haskell is a dynamically-typed, interpreted+-- language,’ as Vidrun helpfully teaches us.) Returning a 'Constraint' allows+-- us to step outside the type family paradigm as needed by returning a real+-- class, but fortunately this isn't necessary very much: only for terminal+-- equalities ('(~)'), the incoherent-by-design instances ('KnownEq' and+-- 'KnownApp'), and a pair of auxiliary classes representing tuples of+-- constraints related by newly-introduced unknown type parameters+-- ('EvalSubstituteApp' and '(:&:)', of which the latter is more often invoked+-- through the '(:?:)' / '(:::)' ternary interface than directly).+--+-- Note that having monolithic 'Expr' and 'Eval' instead of a number of smaller+-- type families is very useful, as it enables one set of generic operators to+-- be reused in different parts of the algorithm. They work by holding+-- partially-applied 'Expr' values instead of attempting to partially apply a+-- type family (which is illegal).+++-- | An empty class witnessing a substitution relationship between two types.+type Substitute ∷ List Subst → k → k → Constraint+type Substitute σ a b = Eval (Substitute_go σ σ a b)+++-- | A representation of work to be done while solving a 'Substitute'+-- constraint. Some of these constructors are ad-hoc for this application, and+-- some are generic combinators that save me from repeating the same pattern+-- multiple times.+--+-- The choice of final argument is often significant, so that it can be used+-- with '(:&:)'.+type data Expr+  -- | The worker function of 'Substitute'.+  = ∀ k. Substitute_go+    (List Subst)+    -- ^ initial list of substitutions+    (List Subst)+    -- ^ substitutions still to be handled+    k+    -- ^ input type of the coercion+    k+    -- ^ result type of the coercion++  -- | Find any matching 'Within' substitutions and expand them in place.+  | ∀ k. Expand+    (List Subst)+    -- ^ list of substitutions+    k+    -- ^ type to scrutinize for matching 'Within' fragments+    (List Subst)+    -- ^ expanded list++  -- | Helper function for expanding a single 'Within'.+  | ∀ k₁ k₂. Expand_doWithin+    (ExpandWithinEnv k₁)+    k₂+    -- ^ type to scrutinize+    (List Subst)+    -- ^ a suffix of already-expanded substitutions to append to the result++  -- | Helper function for continuing a 'Within' expansion in an applied type.+  | ∀ k₁ k₂. Expand_doWithinApp+    (ExpandWithinEnv k₁)+    k₂+    -- ^ type to scrutinize+    (List Subst)+    -- ^ a suffix of already-expanded substitutions to append to the result++  -- | Helper function for building a list.+  | ∀ k. DoCons k {-^ head -} (List k) {-^ head : tail -} (List k) {-^ tail -}++  -- | Generic holder for a unary 'Constraint'-kinded function.+  | ∀ k. Lift1 (k → Constraint) k++  -- | Generic holder for a pair of control branches.+  | (:::) Constraint {-^ if true -} Constraint {-^ if false -} Bool++type ExpandWithinEnv k =+  ( k          -- selector of the 'Within'+  , List Subst -- payload of the 'Within'+  , List Subst -- result of the expansion, starting with either this payload or+               -- a re-wrapped 'Within'+  )+++-- | Constraint-kinded ternary operator: @Condition :?: IfTrue ::: IfFalse@+type (:?:) ∷ (Bool → Constraint) → (Bool → Expr) → Constraint+type (:?:) cond = (:&:) (Lift1 cond)+infixr 0 :?:, :::+++-- | Generic operator for cutting two 'Expr's with an unknown parameter to be+-- solved. A little bit like a symmetric type-level @$@ or @&@, but don't lean+-- on that too hard.+class (f ∷ k → Expr) :&: (g ∷ k → Expr)+instance (Eval (f a), Eval (g a)) ⇒ f :&: g+++type family Eval (expr ∷ Expr) ∷ Constraint where+  Eval (Substitute_go σ₀ (from ↦  to : σ) arg res) =+    from `KnownEq` arg :?: to ~ res ::: Eval (Substitute_go σ₀ σ arg res)++  Eval (Substitute_go σ₀ (from ↦! to : σ) arg res) =+    from `KnownEq` arg :?: to ~ res :::+    to `KnownEq` res :?: from ~ arg ::: Eval (Substitute_go σ₀ σ arg res)++  Eval (Substitute_go σ₀ (_ : σ) arg res) = Eval (Substitute_go σ₀ σ arg res)++  Eval (Substitute_go σ₀ '[] arg res) =+    -- Once all 'Subst's have been examined, if we can recurse into @arg@ or+    -- @res@, do so; otherwise @arg@ doesn't get modified.+    KnownApp arg :?: EvalSubstituteApp σ₀ arg res False :::+    KnownApp res :?: EvalSubstituteApp σ₀ arg res True ::: arg ~ res++  -- Expand this 'Within' and prepend it to the result of expanding the+  -- remaining 'Subst's.+  Eval (Expand (Within w_f w_σ : σ) f₀ res_σ) =+    Expand_doWithin '(w_f, w_σ, res_σ) f₀ :&: Expand σ f₀++  -- Non-'Within's don't get expanded, but they are preserved.+  Eval (Expand (s : σ) f₀ res_σ) = DoCons s res_σ :&: Expand σ f₀+  Eval (Expand '[] _ res_σ) = '[] ~ res_σ++  Eval (Expand_doWithin '(w_f, w_σ, res_σ) f σ') =+    -- If this 'Within' matches the current scrutinee, prepend its payload.+    w_f `KnownEq` f :?: w_σ ++ σ' ~ res_σ :::+    -- Otherwise, advance up the spine of the scrutinee if we can.+    KnownApp f :?: Eval (Expand_doWithinApp '(w_f, w_σ, res_σ) f σ') :::+    -- If we can't, this 'Within' does not trigger. Preserve it as-is in the+    -- result.+      Within w_f w_σ : σ' ~ res_σ++  -- Exists only to decompose the scrutinee into @f _@. Generally, doing this+  -- in a type family would risk getting stuck on unknown cases, but this+  -- helper is only used guarded by 'KnownApp'.+  Eval (Expand_doWithinApp env (f _) σ') = Eval (Expand_doWithin env f σ')+++  Eval (DoCons a α₁ α₂) = a : α₂ ~ α₁+  Eval ((c ::: _) True) = c+  Eval ((_ ::: c) False) = c+  Eval (Lift1 f a) = f a+++-- | Independently substitute in the two parts of a type application and+-- recombine the results. Can be driven ‘forward’ or ‘in reverse’, meaning that+-- @f_a@ or @f_b@ respectively are to be used as the source of type information+-- for the next substitution passes.+class EvalSubstituteApp+  (σ ∷ List Subst)+  -- ^ list of substitutions+  (f_a ∷ k)+  -- ^ a type, known to be an application, and not matching anything in @σ@+  (f_b ∷ k)+  -- ^ @f_a@ after applying @σ@, known to be an application, and not matching+  -- anything injective in @σ@+  (in_reverse ∷ Bool)+instance+  ( Substitute σ f f'+  , Eval (Expand σ f σ')+  , Substitute σ' a a'+  , f' a' ~ f_b+  ) ⇒ EvalSubstituteApp σ (f a) f_b False+instance+  ( Substitute σ f' f+  , Eval (Expand σ f' σ')+  , Substitute σ' b' b+  , f_a ~ f' b'+  ) ⇒ EvalSubstituteApp σ f_a (f b) True+++-- | Put 'True' in @result@ if the compiler knows that the two argument types+-- are equal, and 'False' if there is any doubt. For this use case, this level+-- of certainty is good enough.+class KnownEq (a ∷ k₁) (b ∷ k₂) (result ∷ Bool) | a b → result+instance                    True  ~ result ⇒ KnownEq a a result+instance {-# INCOHERENT #-} False ~ result ⇒ KnownEq _₁ _₂ result+++-- | Put 'True' in @result@ if the compiler knows that the argument type is an+-- application of one type to another, and 'False' if there is any doubt. For+-- this use case, this level of certainty is good enough.+class KnownApp (a ∷ k) (result ∷ Bool) | a → result+instance                    True  ~ result ⇒ KnownApp (f _₁) result+instance {-# INCOHERENT #-} False ~ result ⇒ KnownApp _₁ result+++-- | Append two type-level lists. Come on, did you expect anything else?+type (++) ∷ List a → List a → List a+type family α₁ ++ α₂ where+  '[] ++ α = α+  (a : α₁) ++ α₂ = a : (α₁ ++ α₂)