{-# 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 :: ∀ (σ ∷ [Subst]) a b. (Substitute σ a b, Coercible a b) ⇒ a → b
coerceSubst = a → b
∀ a b. Coercible a b ⇒ a → b
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 :: ∀ (σ ∷ [Subst]) a b. Substitute σ a b ⇒ a → b
unsafeCoerceSubst = a → b
∀ a b. a → b
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, it is necessary to 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 : (α₁ ++ α₂)