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.

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 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] (>>=)
>>> :}

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.)

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.

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.)

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 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, 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, String is a specific kind of [] that we don't want to become a 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.)

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.

The above conveniences work for 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 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.)

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))

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]})

Withins 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]),())

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 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]