swift-mirror/docs/Generics/chapters/class-inheritance.tex

\documentclass[../generics]{subfiles}

\begin{document}

\chapter[]{Class Inheritance}\label{classinheritance}

\ifWIP

TODO:
\begin{itemize}
\item various rules around classes conforming to protocols---need to understand restrictions on protocol requirements and witnesses
\item silly example:
\begin{Verbatim}
class Base<T, U> {
 init(_: T) { print("a") }
 init(_: U) { print("b") }
}
class Derived: Base<Int, Int> { }

Derived(123)
\end{Verbatim}
\end{itemize}

When a subclass inherits from a superclass, there is a subtype relationship between the subclass and superclass. If neither class is generic, the relationship is straightforward. Here, we have a pair of classes \texttt{C} and \texttt{D}; \texttt{D} inherits from \texttt{C}, so instances of \texttt{D} are also instances of \texttt{C}:
\begin{Verbatim}
class C {}
class D {}

let instanceOfD: D = D()
let instanceOfC: C = instanceOfD  // okay
\end{Verbatim}
With generic classes, the situation is more subtle. The subclass \emph{declaration} states a superclass \emph{type}. The superclass type appears in the inheritance clause of the subclass, and can reference the subclass's generic parameters:
\begin{Verbatim}
class Base<T, U> {}
class Derived<A>: Base<String, A> {}
\end{Verbatim}
Now, the declaration \texttt{Derived} has the generic superclass type \texttt{Base<String, A>}. We expect that \texttt{Derived<A>} is a subtype of \texttt{Base<String, A>}, and \texttt{Derived<Int>} is a subtype of \texttt{Base<String, Int>}, but that \texttt{Derived<Int>} and \texttt{Base<String, String>} are unrelated types.

To get a complete picture of the subtype relationship, we need to define the concept of the superclass type \emph{of a type}, and not just the superclass type of a declaration.

First of all, what is the superclass type of the declared interface type of a class? The superclass type of the class declaration is an interface type for the class declaration's generic signature, so we say that the superclass type of the declared interface type is just the superclass type of the declaration. In our example, this tells us that \texttt{Derived<A>} is a subtype of \texttt{Base<String, A>} and an unrelated type to \texttt{Base<Int, A>}.

What about the superclass type of an arbitrary specialization of the class? Here, we rely on the property that a specialized type is the result of applying its context substitution map to the declared interface type. If we instead apply the context substitution map to the superclass type of the class declaration, we get the superclass type of our specialized type. This can be shown with a commutative diagram:
\begin{quote}
\begin{tikzcd}[column sep=3cm,row sep=1cm]
\mathboxed{declared interface type} \arrow[d, "\text{superclass type}"{left}] \arrow[r, "\text{substitution}"] &\mathboxed{specialized type} \arrow[d, "\text{superclass type}"] \\
\mathboxed{superclass type of declaration} \arrow[r, "\text{substitution}"]&\mathboxed{superclass type of type}
\end{tikzcd}
\end{quote}

Now that we can compute the superclass type of a type, we can walk up the inheritance hierarchy by iterating the process, to get the superclass type of a superclass type, and so on.

\begin{algorithm}[Iterated superclass type]\label{superclassfordecl} As input, takes a class type \texttt{T} and a superclass declaration \texttt{D}. Returns the superclass type of \texttt{T} for \texttt{D}.
\begin{enumerate}
\item Let \texttt{C} be the class declaration referenced by \texttt{T}. If $\texttt{C}=\texttt{D}$, return \texttt{T}.
\item If \texttt{C} does not have a superclass type, fail with an invariant violation; \texttt{D} is not actually a superclass of \texttt{T}.
\item Otherwise, apply the context substitution map of \texttt{T} to the superclass type of \texttt{C}. Assign this new type to \texttt{T}, and go back to Step~1.
\end{enumerate}
\end{algorithm}

\begin{listing}\captionabove{Satisfied and unsatisfied superclass requirements}\label{unsatisfied requirements superclass}
\begin{Verbatim}
class Base<T> {}
class Derived: Base<Int> {}

struct G<T: Base<U>, U> {}

struct H<X: Derived, Y> {
  // (1) requirement is satisfied
  typealias A = G<Base<Y>, Y>

  // (1) requirement is satisfied
  typealias B = G<X, Int>

  // (2) requirement is unsatisfied
  typealias C = G<Derived, Y>
}
\end{Verbatim}
\end{listing}
\begin{example}
\ListingRef{unsatisfied requirements superclass} shows two examples involving superclass requirements. The generic signature of \texttt{G} is:
\begin{quote}
\begin{verbatim}
<T, U where T: Base<U>>
\end{verbatim}
\end{quote}
The generic signature has a single requirement:
\begin{quote}
\begin{tabular}{|l|l|l|}
\hline
Kind&Subject type&Constraint type\\
\hline
Superclass&\texttt{T}&\texttt{Base<U>}\\
\hline
\end{tabular}
\end{quote}

\paragraph{First type alias} The context substitution map of the underlying type of \texttt{A}:
\[
\SubstMap{
\SubstType{T}{Base<$\archetype{Y}$>}\\
\SubstType{U}{$\archetype{Y}$}
}
\]
We apply this substitution map to the requirement of our generic signature:
\begin{quote}
\begin{tabular}{|l|l|l|c|}
\hline
Kind&Subject type&Constraint type&Satisfied?\\
\hline
Superclass&\texttt{Base<$\archetype{Y}$>}&\texttt{Base<$\archetype{Y}$>}&$\checkmark$\\
\hline
\end{tabular}
\end{quote}
The requirement is satisfied, because the subject type is canonical-equal to the constraint type.

\index{superclass type}
\paragraph{Second type alias} The context substitution map of the underlying type of \texttt{B}:
\[
\SubstMap{
\SubstType{T}{$\archetype{X}$}\\
\SubstType{U}{Int}
}
\]
We apply this substitution map to the requirement of our generic signature:
\begin{quote}
\begin{tabular}{|l|l|l|}
\hline
Kind&Subject type&Constraint type\\
\hline
Superclass&\archetype{X}&\texttt{Base<Int>}\\
\hline
\end{tabular}
\end{quote}
The requirement hits the recursive case for superclass requirements in \AlgRef{reqissatisfied}. The archetype \archetype{X} is replaced with its superclass type \texttt{Derived}, via the generic signature of \texttt{H}:
\begin{quote}
\begin{tabular}{|l|l|l|}
\hline
Kind&Subject type&Constraint type\\
\hline
Superclass&\texttt{Derived}&\texttt{Base<Int>}\\
\hline
\end{tabular}
\end{quote}
The algorithm recurses again, after replacing the class type \texttt{Derived} with its superclass type \texttt{Base<Int>}:
\begin{quote}
\begin{tabular}{|l|l|l|c|}
\hline
Kind&Subject type&Constraint type&Satisfied?\\
\hline
Superclass&\texttt{Base<Int>}&\texttt{Base<Int>}&$\checkmark$\\
\hline
\end{tabular}
\end{quote}
In its final form, the substituted requirement is trivially seen to be satisfied because the subject type is canonical-equal to the constraint type.

\index{superclass type}
\paragraph{Third type alias} The context substitution map of the underlying type of \texttt{C}:
\[
\SubstMap{
\SubstType{T}{$\archetype{X}$}\\
\SubstType{U}{$\archetype{Y}$}
}
\]
We apply this substitution map to the requirement of our generic signature:
\begin{quote}
\begin{tabular}{|l|l|l|}
\hline
Kind&Subject type&Constraint type\\
\hline
Superclass&\archetype{X}&\texttt{Base<\archetype{Y}>}\\
\hline
\end{tabular}
\end{quote}
The requirement is seen to be unsatisfied, as follows. As above, the archetype \archetype{X} is replaced with its superclass type \texttt{Derived}, which is replaced with its superclass type \texttt{Base<Int>}:
\begin{quote}
\begin{tabular}{|l|l|l|c|}
\hline
Kind&Subject type&Constraint type&Satisfied?\\
\hline
Superclass&\texttt{Base<Int>}&\texttt{Base<$\archetype{Y}$>}&$\times$\\
\hline
\end{tabular}
\end{quote}
At this point, the substituted requirement is between two different specializations of the same class declaration, \texttt{Base<Int>} and \texttt{Base<$\archetype{Y}$>}. They are not canonical-equal, because $\archetype{Y}$ is not \texttt{Int}, so the requirement is unsatisfied.
\end{example}

\begin{listing}\captionabove{Computing superclass types}\label{generic superclass example listing}
\begin{Verbatim}
class Base<T> {
  typealias C = () -> T
}
class Middle<T, U>: Base<(T, T)> {}
class Derived: Middle<Int, String> {}

let derived = Derived()
let instanceOfMiddle: Middle<Int, String> = derived  // okay
let instanceOfBase: Base<(Int, Int)> = derived  // okay
\end{Verbatim}
\end{listing}

\begin{example}\label{genericsuperclassexample}
\ListingRef{generic superclass example listing} shows a class hierarchy demonstrating these behaviors:
\begin{enumerate}
\item The superclass type of \texttt{Derived} is \texttt{Middle<Int, String>}.
\item The superclass type of \texttt{Middle} is \texttt{Base<(T, T)>}.
\end{enumerate}
The superclass type of the type \texttt{Middle<Int, String>} is the superclass type of \texttt{Middle} with the context substitution map of \texttt{Middle<Int, String>} applied:
\[\texttt{Base<(T, T)>}\otimes
\SubstMap{
\SubstType{T}{Int}\\
\SubstType{U}{String}
} = \texttt{Base<(Int, Int)>}
\]
This means the superclass type of \texttt{Derived} with respect to \texttt{Base} is \texttt{Base<(Int, Int)>}.

What is the type \texttt{Derived.C}? The type alias \texttt{C} is declared in \texttt{Base}. The superclass type of \texttt{Derived} with respect to \texttt{Base} is \texttt{Base<(Int, Int)>}. We can apply the context substitution map of this superclass type to the declared interface type of \texttt{C}:
\[\texttt{() -> T}\otimes
\SubstMap{
\SubstType{T}{(Int, Int)}
} = \texttt{() -> (Int, Int)}
\]
\end{example}

We can finally describe the implementation of Case~3 of a context substitution map for a declaration context from \SecRef{checking generic arguments}.

The base type here is a class type, and the declaration context is some superclass declaration or an extension thereof. We first apply \AlgRef{superclassfordecl} to the base type and superclass declaration to get the correct superclass type. Then, we compute the context substitution map of this superclass type with respect to our declaration context, which is now either the exact superclass declaration or an extension. Thus we have reduced the problem to Case~1, which we already know how to solve.

TODO: example

\fi

\section[]{Inherited Conformances}\label{inheritedconformance}

\ifWIP

TODO:
\begin{itemize}
\item example where base class is not generic but subclass is -- two inherited conformances with same underlying specialized conformance
\item behavior of inherited conformances under substitution
\item restrictions on class conformances
\item longest possible delegation chain is $inherited \rightarrow specialized \rightarrow normal$.
\end{itemize}

Protocol conformances are inherited from superclass to subclass. At each level of class inheritance, the conformance table of a subclass is initialized with a copy of the conformance table of the superclass, with the superclass substitution map applied to each inherited conformance.

This behavior can be broken down into two cases. If a superclass directly conforms to a protocol, the superclass's conformance table will store a normal conformance. The subclass will inherit a specialized conformance built from this normal conformance together with the superclass substitution map. In the general case, the superclass conforms via an inherited conformance from further up the hierarchy, and the subclass conformance is built by composing the substitution map in some other specialized conformance with the superclass substitution map. In this way, an inherited conformance is ultimately derived from the normal conformance of some class further up in the hierarchy, specialized by the substitution map obtained by composing all superclass substitution maps at every level of inheritance, up to the base class declaring the conformance.

The lookup conformance table machinery actually introduces an additional level of indirection by wrapping these specialized conformances in a bespoke \emph{inherited conformance} data type. Conformances store their conforming type; the defining invariant is that if a conformance was the result of a lookup, the stored conforming type should equal the original type of the lookup. With class inheritance however, the conforming type of a conformance declared on the superclass is ultimately always some substitution of the type of the superclass. An inherited conformance stores the original subclass type, but otherwise just delegates to an underlying conformance, either normal or specialized. By wrapping inherited conformances in a special type, the compiler is able to keep track of the original type of a conformance lookup.
\begin{example}
We can amend \ExRef{genericsuperclassexample} to add a conformance to the \texttt{Base} class:
\begin{Verbatim}
protocol P {
  associatedtype A
}

extension Base: P {}
\end{Verbatim}
The normal conformance \texttt{Base<T>:\ P} stores the type witness for \texttt{A}, which is \texttt{Array<T>}. Looking up the conformance \texttt{Derived:\ P} returns an inherited conformance. The inherited conformance reports its conforming type as \texttt{Derived} instead of \texttt{Base<(Int,~Int)>}, but otherwise delegates all operations to a specialized conformance with the substitution map $\texttt{T}:=\texttt{(Int, Int)}$. The specialized conformance in turn delegates to the normal conformance, but applies the substitution map when looking up type witnesses and associated conformances. Therefore, looking up the type witness for \texttt{A} in the inherited conformance \texttt{Derived:\ P} returns \texttt{Array<(Int,~Int)>}, which is the result of applying our substitution map to the type witness stored in the normal conformance.
\end{example}

\fi

\section[]{Override Checking}\label{overridechecking}

\ifWIP

When a subclass overrides a method from a superclass, the type checker must ensure the subclass method is compatible with the superclass method in order to guarantee that instances of the subclass are dynamically interchangeable with a superclass. If neither the superclass nor the subclass are generic, the compatibility check simply compares the fully concrete parameter and result types of the non-generic declarations. Otherwise, the superclass substitution map plays a critical role yet again, because the compatibility relation must project the superclass method's type into the subclass to meaningfully compare it with the override.

\paragraph{Non-generic overrides}
The simple case is when the superclass or subclass is generic, but the superclass method does not define generic parameters of its own, either explicitly or via the opaque parameters of \SecRef{requirements}. Let's call such a method ``non-generic,'' even if the class it appears inside is generic. So a non-generic method has the same generic signature as its parent context, which in our case is a class. In the non-generic case, the superclass substitution map is enough to understand the relation between the interface type of the superclass method and its override.

\begin{listing}\captionabove{Some method overrides}\label{method overrides}
\begin{Verbatim}
class Outer<T> {
  class Inner<U> {
    func doStuff(_: T, _: U) {}

    func doGeneric<A: Equatable>(_: A) {}
  }
}

class Derived<V>: Outer<Int>.Inner<(V, V)> {
  func doStuff(_: Int, _: (V, V)) {}

  override func doGeneric<A>(_: A) {}
}
\end{Verbatim}
\end{listing}

In \ListingRef{method overrides}, the \texttt{Derived} class overrides the \texttt{doStuff()} method from \texttt{Outer.Inner}. Dropping the first level of function application from the interface type of \texttt{doStuff()} leaves us with \texttt{(T, U) -> ()}, to which we apply the superclass substitution map for \texttt{Derived} to get the final result:
\[
\texttt{(T, U) -> ()} \otimes
\SubstMap{
\SubstType{T}{Int}\\
\SubstType{U}{(V, V)}
} =
\texttt{(Int, (V, V)) -> ()}
\]
This happens to exactly equal the interface type of the subclass method \texttt{doStuff()} in \texttt{Derived}, again not including the self clause. An override with an exact type match is valid. (In fact, some variance in parameter and return types is permitted as well, but it's not particularly interesting from a generics point of view, so here is the executive summary: an override can narrow the return type, and widen the parameter types. This means it is valid to override a method returning \texttt{Optional<T>} with a method returning \texttt{T}, because a \texttt{T} can also trivially become a \texttt{Optional<T>} via an injection. Similarly, if \texttt{A} is a superclass of \texttt{B}, a method returning \texttt{A} can be overridden to return \texttt{B}, because a \texttt{B} is always an \texttt{A}. A dual set of rules are in play in method parameter position; if the original method takes an \texttt{Int} the override can accept \texttt{Optional<Int>}, etc.)

\paragraph{Generic overrides}
In the non-generic case, applying the superclass substitution map directly to the interface type of a superclass method tells us what ``the type of the superclass method should be'' in the subclass, and this happens to work because the superclass method had the same generic signature as the superclass. Once this is no longer required to be so, the problem becomes more complicated, and the below details were not worked out until \IndexSwift{5.2}Swift 5.2 \cite{sr4206}.

The generic signature of the superclass (resp. override) method is built by adding any additional generic parameters and requirements to the generic signature of the superclass (resp. subclass) itself. To relate these four generic signatures together, we generalize the superclass substitution map into something called the \emph{attaching map}. Once we can compute an attaching map, applying it to the interface type of the superclass method produces a substituted type which can be compared against the interface type of the override, just as before. However, while this part is still necessary, it is no longer sufficient, since we also need to compare the \emph{generic signatures} of the superclass method and its override for compatibility. Here the attaching map also plays a role.

Overrides with a different number of innermost generic parameters are immediately known to be invalid, and no further checking needs to take place. (Interestingly enough, the names of generic parameters do not matter. Generic parameters are uniquely identified by depth and index, not name.) Once it is known that both generic signatures have the same number of innermost parameters, we can define a 1:1 correspondence between the two generic parameter lists which preserves the index but possibly changes the depth.

We build the attaching map by ``extending'' the superclass substitution map, adding replacement types for the superclass method's innermost generic parameters, which map to the subclass method's generic parameters via the above correspondence. In addition to new replacement types, the attaching map stores conformances not present in the superclass substitution map, if the superclass method introduces conformance requirements.

\begin{algorithm}[Compute attaching map for generic method override]\label{superclass attaching map} As input, takes the superclass method's generic signature \texttt{G}, the superclass declaration \texttt{B}, and some subclass declaration \texttt{D}. Outputs a substitution map for \texttt{G}.
\begin{enumerate}
\item Initialize \texttt{R} to an empty list of replacement types.
\item Initialize \texttt{C} to an empty list of conformances.
\item Let $\texttt{G}'$ be the generic signature of \texttt{B}, and let \texttt{T} be the declared interface type of \texttt{D}.
\item (Trivial case) If $\texttt{D}=\texttt{B}$, return \texttt{G}.
\item (Remapping) Let \texttt{S} be the context substitution map of \texttt{T} for the declaration context of \texttt{B}.
\item (Replacements) For each generic parameter of \texttt{G}, check if this is a valid generic parameter in $\texttt{G}'$. If so, this is a generic parameter of the superclass, so apply \texttt{S} and record the replacement type in \texttt{R}. Otherwise, this is an innermost generic parameter of the superclass method. Adjust the depth of this parameter by subtracting the generic context depth of \texttt{B} and adding the generic context depth of \texttt{D}, and record a new generic parameter type with the adjusted depth but identical index in \texttt{R}.

\item (Conformances) For each conformance requirement \texttt{T:\ P} of \texttt{G}, first check if \texttt{T} is a valid type in $\texttt{G}'$, and if \texttt{T} conforms to \texttt{P} in $\texttt{G}'$. If so, look up the conformance \texttt{T:\ P} in \texttt{S} and record the result in \texttt{C}. Otherwise, this is a new conformance requirement present in \texttt{G} but not $\texttt{G}'$. Record the abstract conformance to \texttt{P} in \texttt{C}.

\item (Return) Return the substitution map for \texttt{G} from \texttt{R} and \texttt{C}.
\end{enumerate}
\end{algorithm}

\begin{example}
To continue the \texttt{doGeneric()} example from \ListingRef{method overrides}, the superclass method defines a generic parameter \texttt{A} at depth 2, but the ``same'' parameter has depth 1 in the subclass method of \texttt{Derived}. For clarity, the attaching map is written with canonical types (otherwise, it would replace \texttt{A} with \texttt{A}, with a different meaning of \texttt{A} on each side):
\[
\SubstMapLongC{
\SubstType{\ttgp{0}{0}}{Int}\\
\SubstType{\ttgp{1}{0}}{(\ttgp{0}{0}, \ttgp{0}{0})}\\
\SubstType{\ttgp{2}{0}}{\ttgp{1}{0}}
}{
\SubstConf{\ttgp{1}{0}}{(\ttgp{0}{0}, \ttgp{0}{0})}{Equatable}
}
\]
\end{example}

\paragraph{The override signature}
The attaching map is called such because it allows us to ``glue'' together the generic signature of the superclass method with the generic signature of the subclass type, and build the expected generic signature of the subclass method, also known as the \emph{override signature}. The expected generic signature can then be compared against the actual generic signature of the subclass method.

The actual generic signature of the subclass method is constructed from three parts:
\begin{enumerate}
\item the generic signature of the subclass type
\item the subclass method's innermost generic parameters
\item any additional generic requirements imposed by the subclass method
\end{enumerate}
The computation of the expected generic signature is similar, except in place of the third step, we build the additional requirements by applying the attaching map to each requirement of the \emph{superclass} method.
\begin{algorithm}[Compute override generic signature] As input, takes the superclass method's generic signature \texttt{G}, the superclass declaration \texttt{B}, and some subclass declaration \texttt{D}. Outputs a new generic signature.
\begin{enumerate}
\item Initialize \texttt{P} to an empty list of generic parameter types.
\item Initialize \texttt{R} to an empty list of generic requirements.
\item Let \texttt{S} be the attaching map for \texttt{G}, \texttt{B} and \texttt{D} computed using \AlgRef{superclass attaching map}.
\item (Parent signature) Let $\texttt{G}''$ be the generic signature of \texttt{D}. (In \AlgRef{superclass attaching map}, $\texttt{G}'$ was used for the generic signature of \texttt{B}.)
\item (Additional parameters) For each generic parameter of \texttt{G} at the innermost depth, apply \texttt{S} to the generic parameter. By construction, the result is another generic parameter type; record this type in \texttt{P}.
\item (Additional requirements) For each requirement of \texttt{G}, apply \texttt{S} to the requirement and record the result in \texttt{R}.
\item (Return) Build a minimized generic signature from $\texttt{G}''$, \texttt{P} and \texttt{R}, and return the result.
\end{enumerate}
\end{algorithm}

For the override to satisfy the contract of the superclass method, it should accept any valid set of concrete type arguments also accepted by the superclass method. The override might be more permissive, however. The correct relation is that each generic requirement of the actual override signature must be satisfied by the expected override signature, but not necessarily vice versa. This uses the same mechanism as conditional requirement checking for conditional conformances, described in \SecRef{conditional conformance}. The requirements of one signature can be mapped to archetypes of the primary generic environment of another signature. This makes the requirement types concrete, which allows the \texttt{isSatisfied()} predicate to be checked against the substituted requirement.

\begin{example} In \ListingRef{method overrides}, the superclass method generic signature is \texttt{<T, U, A where A: Equatable>}. The generic parameter \texttt{A} belongs to the method; the other two are from the generic signature of the superclass. The override signature glues together the innermost generic parameters and their requirements from the superclass method with the generic signature of the subclass, which is \texttt{<V>}. This operation produces the signature \texttt{<V, A where A:\ Equatable>}. This is different from the actual override generic signature of \texttt{doStuff()} in \texttt{Derived}, which is \texttt{<V, A>}. However, the actual signature's requirements are satisfied by the expected signature.
\end{example}

\fi

\section[]{Designated Initializer Inheritance}

\iffalse

TODO:
\begin{itemize}
\item Initializer or constructor?
\item Substitute requirements + build new signature
\item The rules
\item Worked example
\end{itemize}

\fi

\section[]{Witness Thunks}\label{valuerequirements}

\ifWIP

When protocol conformances were introduced in \ChapRef{conformances}, our main focus was the mapping from associated type requirements to type witnesses, and how conformances participate in type substitution. Now let's look at the other facet of conformances, which is how they map value requirements to value witnesses.\footnote{The term ``value witness'' is overloaded to have two meanings in Swift. The first is a witness to a value requirement in a protocol. The second is an implementation of an intrinsic operation all types support, like copy, move, destroy, etc., appearing in the value witness table of runtime type metadata. Here I'm talking about the first meaning.} Recording a witness for a protocol requirement requires more detail than simply stating the witness.

What is the relationship between the generic signature of a protocol requirement and the generic signature of the witness? Well, ``it's complicated.'' A protocol requirement's generic signature has a \texttt{Self} generic parameter constrained to that protocol. If the witness is a default implementation from a protocol extension, it will have a \texttt{Self} generic parameter, too, but it might conform to a \emph{different} protocol. Or if the witness is a member of the conforming type and the conforming type has generic parameters of its own, it will have its own set of generic parameters, with different requirements. A witness might be ``more generic'' than a protocol requirement, where the requirement is satisfied by a fixed specialization of the witness. Conditional conformance and class inheritance introduce even more possibilities. (There will be examples of all of these different cases at the end of \SecRef{witnessthunksignature}.)

\index{SILGen}
All of this means that when the compiler generates a witness table to represent a conformance at runtime, the entries in the witness table cannot simply point directly to the witness implementations. The protocol requirement and the witness will have different calling conventions, so SILGen must emit a \emph{witness thunk} to translate the calling convention of the requirement into that of each witness. Conformance checking records a mapping between protocol requirements and witnesses together with the necessary details for witness thunk emission inside each normal conformance.

The \texttt{ProtocolConformance::getWitness()} method takes the declaration of a protocol value requirement, and returns an instance of \texttt{Witness}, which stores all of the this information, obtainable by calling getter methods:
\begin{description}
\item[\texttt{getDecl()}] The witness declaration itself.
\item[\texttt{getWitnessThunkSignature()}] The \emph{witness thunk generic signature}, which bridges the gap between the protocol requirement's generic signature and the witness generic signature. Adopting this generic signature is what allows the witness thunk to have the correct calling convention that matches the caller's invocation of the protocol requirement, while providing the necessary type parameters and conformances to invoke a member of the concrete conforming type.
\item[\texttt{getSubstitutions()}] The \emph{witness substitution map}. Maps the witness generic signature to the type parameters of the witness thunk generic signature. This is the substitution map at the call of the actual witness from inside the witness thunk.
\item[\texttt{getRequirementToWitnessThunkSubs()}] The \emph{requirement substitution map}.  Maps the protocol requirement generic signature to the type parameters of the witness thunk generic signature. This substituted map is used by SILGen to compute the interface type of the witness thunk, by applying it to the interface type of the protocol requirement.
\end{description}

TODO:
\begin{itemize}
\item diagram with the protocol requirement caller, the protocol requirement type, the witness thunk signature/type, and the witness signature/type.
\item more details about how the witness\_method CC recovers self generic parameters in a special way
\end{itemize}

\section[]{Covariant Self Problem}

In Swift, subclasses inherit protocol conformances from their superclass. If a class conforms to a protocol, a requirement of this protocol can be called on an instance of a subclass. When the protocol requirement is witnessed by a default implementation in a protocol extension, the \texttt{Self} parameter of the protocol extension method is bound to the specific subclass substituted at the call site. The subclass can be observed if, for example, the protocol requirement returns an instance of \texttt{Self}, and the default implementation constructs a new instance via an \texttt{init()} requirement on the protocol.

The protocol requirement can be invoked in one of two ways:
\begin{enumerate}
\item Directly on an instance of the class or one of its subclasses. Since the implementation is known to always be the default implementation, the call is statically dispatched to the default implementation without any indirection through the witness thunk.
\item Indirectly via some other generic function with a generic parameter constrained to the protocol. Since the implementation is unknown, the call inside the generic function is dynamically dispatched via the witness thunk stored in the witness table for the conformance. If the generic function in turn is called with an instance of the class or one of its subclasses, the witness thunk stored in the witness table for the conformance will statically dispatch to the default implementation.
\end{enumerate}
The two cases are demonstrated in \ListingRef{covariantselfexample}. The \texttt{Animal} protocol, which defines a \texttt{clone()} requirement returning an instance of \texttt{Self}. This requirement has a default implementation which constructs a new instance of \texttt{Self} via the \texttt{init()} requirement on the protocol. The \texttt{Horse} class conforms to \texttt{Animal}, using the default implementation for \texttt{clone()}. The \texttt{Horse} class also has a subclass, \texttt{Pony}. It follows from substitution semantics that both \texttt{newPony1} and \texttt{newPony2} should have a type of \texttt{Pony}:
\begin{itemize}
\item The definition of \texttt{newPony1} calls \texttt{clone()} with the substitution map $\texttt{Self} := \texttt{Pony}$. The original return type of \texttt{clone()} is \texttt{Self}, so the substituted type is \texttt{Pony}.
\item Similarly, the definition of \texttt{newPonyIndirect} calls \texttt{cloneAnimal()} with the substitution map $\texttt{A} := \texttt{Pony}$. The original return type of \texttt{cloneAnimal()} is \texttt{A}, so the substituted type is also \texttt{Pony}.
\end{itemize}
The second call dispatches through the witness thunk, so the witness thunk must also ultimately call the default implementation of \texttt{Animal.clone()} with the substitution map $\texttt{Self} := \texttt{Pony}$. When the conforming type is a struct or an enum, the \texttt{self} parameter of a witness thunk has a concrete type. If the conforming type was a class though, it would not be correct to use the concrete \texttt{Horse} type, because the witness thunk would then invoke the default implementation with the substitution map $\texttt{Self} := \texttt{Horse}$, and the second call would return an instance of \texttt{Horse} at runtime and not \texttt{Pony}, which would be a type soundness hole.

\begin{listing}\captionabove{Statically and dynamically dispatched calls to a default implementation}\label{covariantselfexample}
\begin{Verbatim}
protocol Animal {
  init()
  func clone() -> Self
}

extension Animal {
  func clone() -> Self {
    return Self()
  }
}

class Horse: Animal {}
class Pony: Horse {}

func cloneAnimal<A: Animal>(_ animal: A) -> A {
  return animal.clone()
}

let newPonyDirect = Pony().clone()
let newPonyIndirect = cloneAnimal(Pony())
\end{Verbatim}
\end{listing}

\Index{protocol Self type@protocol \texttt{Self} type}
This soundness hole was finally discovered and addressed in \IndexSwift{4.1}Swift~4.1 \cite{sr617}. The solution is to model the covariant behavior of \texttt{Self} with a superclass-constrained generic parameter. When the conforming type is a class, witness thunks dispatching to a default implementation have this special generic parameter, in addition to the generic parameters of the class itself (there are none in our example, so the witness thunk just has the single generic parameter for \texttt{Self}). In the next section, the algorithms for building the substitution map and generic signature all take a boolean flag indicating if a covariant \texttt{Self} type should be introduced. The specific conditions under which this flag is set are a bit subtle:
\begin{enumerate}
\item The conforming type must be a non-final class. If the class is final, there is no need to preserve variance since \texttt{Self} is always the exact class type.
\item The witness must be in a protocol extension. If the witness is a method on the class, there is no way to observe the concrete substitution for the protocol \texttt{Self} type, because it is not a generic parameter of the class method.
\item (The hack) The interface type of the protocol requirement must not mention any associated types.
\end{enumerate}
The determination of whether to use a static or covariant \texttt{Self} type for a class conformance is implemented by the type cheker function \texttt{matchWitness()}.

Indeed, Condition~3 is a hack; it opens up an exception where the soundness hole we worked so hard to close is once again allowed. In an ideal world, Conditions 1~and~2 would be sufficient, but by the time the soundness hole was discovered and closed, existing code had already been written taking advantage of it. The scenario necessitating Condition~3 is when the default implementation appears in a \emph{constrained} protocol extension:
\begin{Verbatim}
protocol P {
  associatedtype T = Self
  func f() -> T
}

extension P where Self.T == Self {
  func f() -> Self { return self }
}

class C: P {}
class D: C {}
\end{Verbatim}
The non-final class \texttt{C} does not declare a type witness for associated type \texttt{T} of protocol~\texttt{P}. The associated type specifies a default, so conformance checking proceeds with the default type witness. The language model is that a conformance is checked once, at the declaration of \texttt{C}, so the default type \texttt{Self} is the ``static'' \texttt{Self} type of the conformance, which is \texttt{C}. Moving on to value requirements, class \texttt{C} does not provide an implementation of the protocol requirement \texttt{f()} either, and the original intent of this code is that the default implementation of \texttt{f()} from the constrained extension of \texttt{P} should used.

Without Condition~3, the requirement \texttt{Self.T == Self} would not be satisfied when matching the requirement \texttt{f()} with its witness; the left hand side of the requirement, \texttt{C}, is not exactly equal to the right hand side, which is the covariant \texttt{Self} type that is only known to be \emph{some subclass} of \texttt{C}. The conformance would be rejected unless \texttt{C} was declared final. With Condition~3, \texttt{Self.T == Self} is satisfied because the static type \texttt{C} is used in place of \texttt{Self} during witness matching.

The compiler therefore continued to accept the above code, because it worked prior to Swift~4.1. Unfortunately, it means that a call to \texttt{D().f()} via the witness thunk will still return an instance of \texttt{C}, and not \texttt{D} as expected. One day, we might remove this exception and close the soundness hole completely, breaking source compatibility for the above example until the developer makes it type safe by declaring \texttt{C} as final. For now, a good guideline to ensure type safety when mixing classes with protocols is \textsl{only final classes should conform to protocols with associated types}.

\fi

\section[]{Witness Thunk Signatures}\label{witnessthunksignature}

\ifWIP

Now we turn our attention to the construction of the data recorded in the \texttt{Witness} type. This is done with the aid of the \texttt{RequirementEnvironment} class, which implements the ``builder'' pattern.

Building the witness thunk signature is an expensive operation. The below algorithms only depend on the conformance being checked, the generic signature of a protocol requirement, and whether the witness requires the use of a covariant \texttt{Self} type. These three pieces of information can be used as a uniquing key to cache the results of these algorithms. Conformance checking might need to consider a number of protocol requirements, each requirement having multiple candidate witnesses that have to be checked to find the best one. In the common case, many protocol requirements will share a generic signature---for example, any protocol requirement without generic parameters of its own has the simple generic signature \texttt{<Self where Self:\ P>}. Therefore this caching can eliminate a fair amount of duplicated work.

The \textbf{witness substitution map} is built by the constraint solver when matching the interface type of a witness to the interface type of a requirement. A description of this process is outside of the scope of this manual.

The \textbf{requirement substitution map} is built by mapping the requirement's \texttt{Self} parameter either to the witness thunk's \texttt{Self} parameter (if the witness has a covariant class \texttt{Self} type), or to the concrete conforming type otherwise. All other generic parameters of the requirement map over to generic parameters of the witness thunk, possibly at a different depth. The requirement's \texttt{Self} conformance is always a concrete conformance, even in the covariant \texttt{Self} case, because \texttt{Self} is subject to a superclass requirement in that case. All other conformance requirements of the requirement's generic signature remain abstract.

The \textbf{witness thunk generic signature} is constructed by stitching together the generic signature of the conformance context with the generic signature of the protocol requirement.

\begin{algorithm}[Build the requirement to witness thunk substitution map] As input, takes a normal conformance~\texttt{N}, the generic signature of a protocol requirement~\texttt{G}, and a flag indicating if the witness has a covariant class \texttt{Self} type,~\texttt{F}. Outputs a substitution map for \texttt{G}.
\begin{enumerate}
\item Initialize \texttt{R} to an empty list of replacement types.
\item Initialize \texttt{C} to an empty list of conformances.
\item (Remapping) First compute the depth at which non-\texttt{Self} generic parameters of \texttt{G} appear in the witness thunk signature. Let $\texttt{G}'$ be the generic signature of \texttt{N}, and let \texttt{D} be one greater than the depth of the last generic parameter of $\texttt{G}'$. If $\texttt{G}'$ has no generic parameters, set $\texttt{D}=0$. If \texttt{F} is set, increment \texttt{d} again.
\item (Self replacement) If \texttt{F} is set, record the replacement $\ttgp{0}{0} := \ttgp{0}{0}$ in \texttt{R}. Otherwise, let \texttt{T} be the type of \texttt{N}, and record the replacement $\ttgp{0}{0} := \texttt{T}$.
\item (Remaining replacements) Any remaining generic parameters of \texttt{G} must have a depth of 1. For each remaining generic parameter \ttgp{1}{i},  record the replacement $\ttgp{1}{i}~:=~\ttgp{D}{i}$.
\item (Self conformance) If \texttt{F} is set, build a substitution map $\texttt{S}$ for $\texttt{G}'$ mapping each generic parameter \ttgp{d}{i} to \ttgp{(d+1)}{i}. Apply this substitution map to \texttt{N} to get a specialized conformance, and record this specialized conformance in \texttt{C}.
\item (Self conformance) Otherwise if \texttt{F} is not set, just record \texttt{N} in \texttt{C}.
\item (Remaining conformances) Any remaining conformance requirements in \texttt{G} have a subject type rooted in a generic parameter at depth~1. For each remaining conformance requirement \texttt{T:~P}, record an abstract conformance to \texttt{P} in \texttt{C}. Abstract conformances do not store a conforming type, but if they did, the same remapping process would be applied here.
\item (Return) Build a substitution map for \texttt{G} from \texttt{R} and \texttt{C}.
\end{enumerate}
\end{algorithm}

\begin{algorithm}[Build the witness thunk generic signature] As input, takes a normal conformance~\texttt{N}, the generic signature of a protocol requirement~\texttt{G}, and a flag indicating if the witness has a covariant class \texttt{Self} type,~\texttt{F}. Outputs a substitution map for \texttt{G}.
\begin{enumerate}
\item Initialize \texttt{P} to an empty list of generic parameter types.
\item Initialize \texttt{R} to an empty list of generic requirements.
\item (Remapping) First compute the depth at which non-\texttt{Self} generic parameters of \texttt{G} appear in the witness thunk signature. Let $\texttt{G}'$ be the generic signature of \texttt{N}, and let \texttt{d} be one greater than the depth of the last generic parameter of $\texttt{G}'$. If $\texttt{G}'$ has no generic parameters, set $\texttt{d}=0$. If \texttt{F} is set, increment \texttt{d} again.
\item If \texttt{F} is set, we must first introduce a generic parameter and superclass requirement for the covariant \texttt{Self} type:
\begin{enumerate}
\item (Self parameter) Add the generic parameter \ttgp{0}{0} to \texttt{P}. This generic parameter will represent the covariant \texttt{Self} type.
\item (Remap Self type) Build a substitution map for $\texttt{G}'$ mapping each generic parameter \ttgp{d}{i} to \ttgp{(d+1)}{i}. Apply this substitution map to the type of \texttt{N}, and call the result \texttt{T}.
\item (Self requirement) Add a superclass requirement \texttt{\ttgp{0}{0}:\ T} to \texttt{R}.
\item (Context generic parameters) For each generic parameter \ttgp{d}{i} in $\texttt{G}'$, add the generic parameter \ttgp{(d+1)}{i} to \texttt{P}.
\item (Context generic requirements) For each requirement of $\texttt{G}'$, apply \texttt{S} to the requirement and add the substituted requirement to \texttt{R}.
\end{enumerate}
\item If \texttt{F} is not set, the generic parameters and requirements of the conformance context carry over unchanged:
\begin{enumerate}
\item (Context generic parameters) Add all generic parameters of $\texttt{G}'$ to \texttt{P}.
\item (Context generic requirements) Add all generic requirements of $\texttt{G}'$ to \texttt{R}.
\end{enumerate}
\item (Remaining generic parameters) All non-\texttt{Self} generic parameters of \texttt{G} must have a depth of 1. For each remaining generic parameter \ttgp{1}{i}, add \ttgp{D}{i} to \texttt{P}.
\item (Trivial case) If no generic parameters have been added to \texttt{P} so far, the witness thunk generic signature is empty. Return.
\item (Remaining generic requirements) For each generic requirement of \texttt{G}, apply the requirement to witness thunk substitution map to the requirement, and add the substituted requirement to \texttt{R}.
\item (Return) Build a minimized generic signature from \texttt{P} and \texttt{R} and return the result.

\end{enumerate}
\end{algorithm}

\vfill
\eject

\begin{example} If the neither the conforming type nor the witness is generic, and there is no covariant \texttt{Self} parameter, the witness thunk signature is trivial.
\begin{Verbatim}
protocol Animal {
  associatedtype CommodityType: Commodity
  func produce() -> CommodityType
}

struct Chicken: Animal {
  func produce() -> Egg {...}
}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature] None.
\item[Witness generic signature] None.
\item[Witness substitution map] None.
\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Animal>}
\end{quote}
\item[Requirement substitution map] The protocol requirement does not have its own generic parameter list, but it still inherits a generic signature from the protocol declaration.
\[
\SubstMapC{
\SubstType{Self}{Chicken}
}{
\SubstConf{Self}{Chicken}{Animal}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Generic conforming type.
\begin{Verbatim}
protocol Habitat {
  associatedtype AnimalType: Animal
  func adopt(_: AnimalType)
}

struct Barn<AnimalType: Animal, StallType>: Habitat {
  func adopt(_: AnimalType) {...}
}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature]  \vphantom{a}
\begin{quote}
\texttt{<\ttgp{0}{0}, \ttgp{0}{1} where \ttgp{0}{0}:\ AnimalType>}
\end{quote}
\item[Witness generic signature]  \vphantom{a}
\begin{quote}
\texttt{<AnimalType, StallType where AnimalType:\ Animal>}
\end{quote}
\item[Witness substitution map] This is actually the identity substitution map because each generic parameter is replaced with its canonical form.
\[
\SubstMapC{
\SubstType{AnimalType}{\ttgp{0}{0}}\\
\SubstType{StallType}{\ttgp{0}{1}}
}{
\SubstConf{AnimalType}{AnimalType}{Animal}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Habitat>}
\end{quote}
\item[Requirement substitution map] \phantom{a}
\[
\SubstMapC{
\SubstType{Self}{Barn<\ttgp{0}{0}, \ttgp{0}{1}>}
}{
\SubstConf{Self}{Barn<\ttgp{0}{0}, \ttgp{0}{1}>}{Habitat}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Conditional conformance.
\begin{Verbatim}
struct Dictionary<Key: Hashable, Value> {...}

extension Dictionary: Equatable where Value: Equatable {
  static func ==(lhs: Self, rhs: Self) -> Bool {...}
}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature]  \vphantom{a}
\begin{quote}
\texttt{<\ttgp{0}{0}, \ttgp{0}{1} where \ttgp{0}{0}:\ Hashable, \ttgp{0}{1}:\ Equatable>}
\end{quote}
\item[Witness generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Key, Value where Key:\ Hashable, Value:\ Equatable>}
\end{quote}
\item[Witness substitution map] This is again the identity substitution map because each generic parameter is replaced with its canonical form.
\[
\SubstMapLongC{
\SubstType{Key}{\ttgp{0}{0}}\\
\SubstType{Value}{\ttgp{0}{1}}
}{
\SubstConf{Key}{\ttgp{0}{0}}{Hashable}\\
\SubstConf{Value}{\ttgp{0}{1}}{Equatable}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Equatable>}
\end{quote}
\item[Requirement substitution map] \vphantom{a}
\[
\SubstMapC{
\SubstType{Self}{Dictionary<\ttgp{0}{0}, \ttgp{0}{1}>}
}{
\SubstConf{Self}{Dictionary<\ttgp{0}{0}, \ttgp{0}{1}>}{Equatable}\\
\text{with conditional requirement \texttt{\ttgp{0}{1}:\ Equatable}}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Witness is in a protocol extension.
\begin{Verbatim}
protocol Shape {
  var children: [any Shape]
}

protocol PrimitiveShape:\ Shape {
  var children: [any Shape] { return [] }
}

struct Empty: PrimitiveShape {}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature] None.
\item[Witness generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ PrimitiveShape>}
\end{quote}
\item[Witness substitution map] \vphantom{a}
\[
\SubstMapC{
\SubstType{Self}{Empty}
}{
\SubstConf{Self}{Empty}{PrimitiveShape}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Shape>}
\end{quote}
\item[Requirement substitution map] \phantom{a}
\[
\SubstMapC{
\SubstType{Self}{Empty}
}{
\SubstConf{Self}{Empty}{Shape}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Conforming type is a generic class, and the witness is in a protocol extension.
\begin{Verbatim}
protocol Cloneable {
  init(from: Self)
  func clone() -> Self
}

extension Cloneable {
  func clone() -> Self {
    return Self(from: self)
  }
}

class Box<Contents>: Cloneable {
  var contents: Contents

  required init(from other: Self) {
    self.contents = other.contents
  }
}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature]  \vphantom{a}
\begin{quote}
\texttt{<\ttgp{0}{0}, \ttgp{1}{0} where \ttgp{0}{0}:\ Box<\ttgp{1}{0}>>}
\end{quote}
\item[Witness generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Cloneable>}
\end{quote}
\item[Witness substitution map] \vphantom{a}
\[
\SubstMapC{
\SubstType{Self}{\ttgp{0}{0}}
}{
\SubstConf{Self}{Box<\ttgp{1}{0}>}{Cloneable}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ Cloneable>}
\end{quote}
\item[Requirement substitution map] \phantom{a}
\[
\SubstMapC{
\SubstType{Self}{\ttgp{0}{0}}
}{
\SubstConf{Self}{Box<\ttgp{1}{0}>}{Cloneable}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Requirement is generic.
\begin{Verbatim}
protocol Q {}

protocol P {
  func f<A: Q>(_: A)
}

struct Outer<T> {
  struct Inner<U>: P {
    func f<A: Q>(_: A) {}
  }
}
\end{Verbatim}
\begin{description}
\item[Witness thunk signature]  \vphantom{a}
\begin{quote}
\texttt{<\ttgp{0}{0}, \ttgp{1}{0}, \ttgp{2}{0} where \ttgp{2}{0}:\ Q>}
\end{quote}
\item[Witness generic signature]  \vphantom{a}
\begin{quote}
\texttt{<T, U, A where A:\ Q>}
\end{quote}
\item[Witness substitution map] \vphantom{a}
\[
\SubstMapC{
\SubstType{T}{\ttgp{0}{0}}\\
\SubstType{U}{\ttgp{1}{0}}\\
\SubstType{A}{\ttgp{2}{0}}
}{
\SubstConf{A}{\ttgp{2}{0}}{Q}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self, A where Self:\ P, A:\ Q>}
\end{quote}
\item[Requirement substitution map] \phantom{a}
\[
\SubstMapC{
\SubstType{Self}{Outer<\ttgp{0}{0}>.Inner<\ttgp{1}{0}>}\\
\SubstType{A}{\ttgp{2}{0}}
}{
\SubstConf{A}{\ttgp{2}{0}}{Q}
}
\]
\end{description}
\end{example}

\vfill
\eject

\begin{example} Witness is more generic than the requirement.
\begin{Verbatim}
protocol P {
  associatedtype A: Equatable
  associatedtype B: Equatable

  func f(_: A, _: B)
}

struct S<A: Equatable>: P {
  typealias B = Int

  func f<T: Equatable, U: Equatable>(_: T, _: U) {}
}
\end{Verbatim}
The type witness for \texttt{A} is the generic parameter \texttt{A}, and the type witness for \texttt{B} is the concrete type \texttt{Int}.
The witness \texttt{S.f()} for \texttt{P.f()} is generic, and can be called with any two types that conform to \texttt{Equatable}. Since the type witnesses for \texttt{A} and \texttt{B} are both \texttt{Equatable}, a fixed specialization of \texttt{S.f()} witnesses \texttt{P.f()}.

\begin{description}
\item[Witness thunk signature] \vphantom{a}
\begin{quote}
\texttt{<\ttgp{0}{0} where \ttgp{0}{0}:\ Equatable>}
\end{quote}
\item[Witness generic signature] \vphantom{a}
\begin{quote}
\texttt{<A, T, U where A:\ Equatable, T:\ Equatable, U:\ Equatable>}
\end{quote}
\item[Witness substitution map] \vphantom{a}
\[
\SubstMapC{
\SubstType{A}{\ttgp{0}{0}}\\
\SubstType{T}{\ttgp{0}{0}}\\
\SubstType{U}{Int}
}{
\SubstConf{A}{\ttgp{0}{0}}{Equatable}\\
\SubstConf{T}{\ttgp{0}{0}}{Equatable}\\
\SubstConf{U}{Int}{Equatable}
}
\]

\item[Requirement generic signature]  \vphantom{a}
\begin{quote}
\texttt{<Self where Self:\ P>}
\end{quote}
\item[Requirement substitution map] \phantom{a}
\[
\SubstMapC{
\SubstType{Self}{S<\ttgp{0}{0}>}
}{
\SubstConf{Self}{S<\ttgp{0}{0}>}{P}
}
\]
\end{description}
\end{example}

\fi

\section[]{Source Code Reference}

\iffalse

TODO:

\fi

\end{document}