Make all the cross-references consistent.

Also a comment about how there is an abuse of notation in the
diagram.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

NOTUSED-backpack-symbol-tables.tex

@@ -30,18 +30,18 @@ \chapter{Symbol tables}
 Specifically:
 
 \begin{itemize}
-    \item We describe GHC's \emph{graph representation} (Section~\ref{sec:graph}), in
+    \item We describe GHC's \emph{graph representation} (\cref{sec:graph}), in
     which there are no symbol tables, contrast it with
-    the \emph{interface representation} (Section~\ref{sec:interface}), which utilizes symbol
+    the \emph{interface representation} (\cref{sec:interface}), which utilizes symbol
     tables, is serialized to disk, and describe how we convert
-    between these two representations (Section~\ref{sec:convert}).  Most operations like type
+    between these two representations (\cref{sec:convert}).  Most operations like type
     equality are implemented only for the graph representation, but
     operations which involve \emph{updating} information associated with
     a symbol can only conveniently be done on the interface
     representation.
 
     \item We describe the process for typechecking
-    \verb|hs-boot| files (Section~\ref{sec:boot}). The
+    \verb|hs-boot| files (\cref{sec:boot}). The
     difficulty is that the incomplete symbols supplied
     by the \verb|hs-boot| file must eventually be improved
     with the information from their implementations in the

NOTUSED-old-tour.tex

@@ -33,7 +33,7 @@
 %
 A client can instantiate a requirement merely by having a module
 in scope with the same module name as the requirement; a process called \emph{mixin linking} instantiates the requirement.  Below, we instantiate \verb|db-dsl| with \verb|mysql| and
-\verb|bytestring| (depicted in Figure~\ref{fig:programming-against-interface}):
+\verb|bytestring| (depicted in \cref{fig:programming-against-interface}):
 
 \begin{verbatim}
   name: mysql-dsl
@@ -78,7 +78,7 @@ \section{Reusing libraries with different instantiations}
 
 Suppose an application wants to use \verb|db-dsl| with two different databases
 at the same time. It can do so by mentioning \verb|db-dsl| twice in
-\verb|backpack-includes| (depicted in Figure~\ref{fig:reusing-packages-functors}):
+\verb|backpack-includes| (depicted in \cref{fig:reusing-packages-functors}):
 
 \begin{verbatim}
   name: myapp
@@ -148,7 +148,7 @@ \section{Composing libraries with requirements}
 We can use this package to create a version of \verb|db-dsl|
 which is partially instantiated: that is, it is instantiated
 with \verb|mysql-indef|, but leaves \verb|Data.ByteString|
-unimplemented (depicted in Figure~\ref{fig:composing-requirements}):
+unimplemented (depicted in \cref{fig:composing-requirements}):
 
 \begin{verbatim}
   name: mysql-dsl-indef

NOTUSED-problem.tex

@@ -116,7 +116,7 @@ \section{The problem}
 \end{figure}
 
 But there's a problem: \emph{applicative sharing}. Consider the
-situation in Figure~\ref{fig:problem}:  we have two, independently
+situation in \cref{fig:problem}:  we have two, independently
 written packages which both want to instantiate a component (A) in the
 same way (HImpl).  Applicativity demands that both instantiations
 represent precisely the same type, and thus, a very natural thing to

appendix.tex

@@ -7,7 +7,7 @@ \section{Mixins help reduce sharing constraints}
 
 The goal of this appendix is to explain why mixins help ``avoid the
 preponderance of sharing constraints that occur with ML functors.''
-(as claimed in Section~\ref{sec:intro})  For concreteness, the ML
+(as claimed in \cref{sec:intro})  For concreteness, the ML
 examples in this section will be written in OCaml.
 
 \paragraph{What is a sharing constraint?}
@@ -419,7 +419,7 @@ \section{Challenges}
 the ability to use a type synonym to implement an abstract data type.
 This introduces a form of ``translucency'', where the abstract data type
 is opaque while the implementation is unknown, and transparent afterwards.
-For example, in Section~\ref{sec:instantiating-the-matcher}, we demonstrated
+For example, in \cref{sec:instantiating-the-matcher}, we demonstrated
 how we could instantiate a generic regular expression matcher to match on strings.
 Inside the implementation of the matcher, we knew nothing about the abstract
 type \verb|Str|; after instantiating it, the \verb|accept| function

compiler.tex

@@ -24,7 +24,7 @@ \section{Semantic objects}
 \end{figure}
 
 The semantic objects of GHC Haskell, extended with \Backpack{}, are
-given in Figure~\ref{fig:semantic-objects}.  These semantic objects
+given in \cref{fig:semantic-objects}.  These semantic objects
 correspond closely to the top-level declarations supported by
 Haskell's syntax, but with a few key differences: first, every
 identifier is resolved to an \emph{original name} ($N$) which identifies
@@ -48,7 +48,7 @@ \section{Semantic objects}
     \item The type declarations ($\Utys$), which give
     definitions for each entity provided by a module.  Every defined
     entity list defines a particular entity $n$ (shaded in gray
-    in Figure~\ref{fig:semantic-objects}).  Like export lists,
+    in \cref{fig:semantic-objects}).  Like export lists,
     each declaration in a module has a unique occurrence name
     (e.g., $\Utys(n) = \Uty$).
 
@@ -153,15 +153,15 @@ \section{Typing rules}
 concerns:
 
 \begin{itemize}
-    \item The assumed Haskell judgments (Figure~\ref{typing:haskell}) are the
+    \item The assumed Haskell judgments (\cref{typing:haskell}) are the
         Haskell type-checking judgments we assume are available, but which
         we do not formalize.
 
-    \item The top-level typing rules (Figure~\ref{typing:main}) tell us
+    \item The top-level typing rules (\cref{typing:main}) tell us
         how to typecheck the declarations of a component and form the final
         component type.
 
-    \item The type lookup and renaming rules (Figure~\ref{typing:lookup}) tell us how to
+    \item The type lookup and renaming rules (\cref{typing:lookup}) tell us how to
         get the type of a module by looking up the original type from
         the context, and then \emph{renaming} it according to the substitution
         recorded in the module identifier.
@@ -170,7 +170,7 @@ \section{Typing rules}
         specify when one module type is a subtype of another, and is used
         by both signature merging and dependency matching.
 
-    \item The merging rules (Figure~\ref{typing:merging}) specify how the
+    \item The merging rules (\cref{typing:merging}) specify how the
         module types are merged together during signature merging.
 
 \end{itemize}
@@ -184,7 +184,7 @@ \section{Typing rules}
         $\Gamma = \mathtt{base} : \Xi_b, \mathtt{containers} : \Xi_c$
         would be one where the components \verb|base| and \verb|containers| (with
         component types $\Xi_b$ and $\Xi_c$ respectively) were in the context.
-        A component with holes, e.g., \verb|regex-indef| (Section~\ref{sec:functorizing-the-matcher}),
+        A component with holes, e.g., \verb|regex-indef| (\cref{sec:functorizing-the-matcher}),
         would occur only \emph{once} in this context (even if we have a dependency
         on an instantiated version of it.)
 
@@ -401,7 +401,7 @@ \subsection{Top-level typing rules}
 recorded in $\mathcal{D} ::= \overline{m \mapsto \overline{M}}$).
 
 \emph{Example.}  To make things more concrete, we'll work through
-the typechecking process for package \verb|r| from Figure~\ref{fig:linked-example}.
+the typechecking process for package \verb|r| from \cref{fig:linked-example}.
 For your convenience, we've reproduced the \unit{} below:
 
 \[
@@ -879,8 +879,8 @@ \subsection{Subtyping rules}
 show $\tau \sim_\textsf{N} \sigma$; we could \emph{not} infer
 this under the module.
 Fortunately, abstract data is \emph{not}
-representationally injective (Figure~\ref{fig:representational-injectivity}), as it can be implemented via
-a newtype (\textsc{SubNewtypeAbsData} in Figure~\ref{typing:subtyping}),
+representationally injective (\cref{fig:representational-injectivity}), as it can be implemented via
+a newtype (\textsc{SubNewtypeAbsData} in \cref{typing:subtyping}),
 so this counterexample does not hold.
 
 \paragraph{Subtyping synonyms}
@@ -905,7 +905,7 @@ \subsection{Merging rules}
 
 Finally, \emph{merging} finds the greatest lower bound on our subtyping relation,
 finding a signature which is a subtype of all the original signatures (or failing
-if no such signature exists).  Let's recall our example from Section~\ref{sec:signature-merging}
+if no such signature exists).  Let's recall our example from \cref{sec:signature-merging}
 (now written as module types), extended slightly with some instances:
 
 \[
@@ -1250,7 +1250,7 @@ \section{Substitutability and type inference}
 continue to typecheck.
 
 In the absence of type classes and type families (see
-Section~\ref{sec:metatheory} for a detailed discussion on these
+\cref{sec:metatheory} for a detailed discussion on these
 features), this property largely holds for Haskell's type system.
 However, we found one subtle case related to GHC's treatment
 of \emph{inaccessible code}.  Inaccessible code occurs when

implementation.tex

@@ -53,13 +53,13 @@ \section{Opaque unit identifiers}
 \section{Modifications to GHC}
 
 As far as possible, the typechecking rules described in
-Section~\ref{sec:compiler} are a faithful rendering of our
+\cref{sec:compiler} are a faithful rendering of our
 actual implementation of \Backpack{} in GHC\@: each rule
 is in direct correspondence to some functionality in
 GHC\@.  To help readers interested in perusing \Backpack{} in GHC's
-source code, Table~\ref{table:semantic-objs} gives a correspondence
+source code, \cref{table:semantic-objs} gives a correspondence
 between a semantic object and its corresponding type name in GHC\@;
-similarly, Table~\ref{table:judgments} gives a correspondence between
+similarly, \cref{table:judgments} gives a correspondence between
 our judgments and their implementations in GHC\@.
 
 In our primary \Backpack{} patch (not counting subsequent bugfix
@@ -92,8 +92,8 @@ \section{Modifications to GHC}
 External component type context & $\Gamma$ & \verb|ExternalPackageState| & \verb|HscTypes| \\
 Local type context & $\Delta$ & \verb|HomePackageTable| & \verb|HscTypes| \\
 \end{tabular}
-\caption{Mapping from semantic objects in this thesis (Figure~\ref{fig:lcomponents} and Figure~\ref{fig:semantic-objects}) to their definitions
-in GHC\@.  In some cases, a semantic object maps to two types in GHC\@; see Section~\ref{sec:no-symbol-tables} for details.}
+\caption{Mapping from semantic objects in this thesis (\cref{fig:lcomponents} and \cref{fig:semantic-objects}) to their definitions
+in GHC\@.  In some cases, a semantic object maps to two types in GHC\@; see \cref{sec:no-symbol-tables} for details.}
 \label{table:semantic-objs}
 \end{table}
 
@@ -103,30 +103,30 @@ \section{Modifications to GHC}
 Figure & Judgment & GHC Function & Defined In \\
 \midrule
 
-Fig.~\ref{typing:haskell} & Module/signature typechecking & \verb|tcRnModule| & \verb|TcRnDriver| \\
+\Cref{typing:haskell} & Module/signature typechecking & \verb|tcRnModule| & \verb|TcRnDriver| \\
 & Type/kind equality & \verb|eqType| & \verb|Type| \\
 & Instance resolution & \verb|check_inst| & \verb|TcBackpack| \\
 
-Fig.~\ref{typing:main} & Top-level typing & \verb|load| & \verb|GhcMake| \\
+\Cref{typing:main} & Top-level typing & \verb|load| & \verb|GhcMake| \\
 & \quad\textsf{exposes} & \verb|applyPackageFlag| & \verb|Packages| \\
 & \quad\textsf{inherits} & \verb|collectHoles| & \verb|Packages| \\
 & Declaration typing & \verb|hscTypecheck| & \verb|HscMain| \\
 & Dependency typing & \verb|tcRnCheckUnitId| & \verb|TcBackpack| \\
 & Declaration sequencing & \verb|upsweep| & \verb|GhcMake| \\
 
-Fig.~\ref{typing:lookup} & Original name type lookup & \verb|importDecl| & \verb|LoadIface| \\
+\Cref{typing:lookup} & Original name type lookup & \verb|importDecl| & \verb|LoadIface| \\
 & Module type lookup & \verb|loadInterface| & \verb|LoadIface| \\
 & Substitution & \verb|rnModIface| & \verb|RnModIface| \\
 & Name substitution & \verb|rnIfaceGlobal| & \verb|RnModIface| \\
 %& Orphan substitution & (implicit) & \\
 
-Fig.~\ref{typing:merging} & Signature type merging & \verb|tcRnMergeSignatures| & \verb|TcBackpack| \\
+\Cref{typing:merging} & Signature type merging & \verb|tcRnMergeSignatures| & \verb|TcBackpack| \\
 & Export list merging & \verb|extendNameShape| & \verb|NameShape| \\
 & Declaration list merging & \verb|mergeIfaceDecls| & \verb|TcIface| \\
 
-Fig.~\ref{typing:top-subtyping} & Module subtyping & \verb|checkImplements| & \verb|TcBackpack| \\
+\Cref{typing:top-subtyping} & Module subtyping & \verb|checkImplements| & \verb|TcBackpack| \\
 
-Fig.~\ref{typing:subtyping} & Declaration subtyping & \verb|checkBootDecl| & \verb|TcRnDriver| \\
+\Cref{typing:subtyping} & Declaration subtyping & \verb|checkBootDecl| & \verb|TcRnDriver| \\
 & Declaration pre-subtyping & \verb|checkBootTyCon| & \verb|TcRnDriver| \\
 \end{tabular}
 \caption{Mapping from typing judgments to implementations in GHC.}
@@ -138,7 +138,7 @@ \subsection{No symbol tables}
 \label{sec:no-symbol-tables}
 
 The most important aspect of the implementation not captured by
-the rules in Section~\ref{sec:compiler} is GHC's lack of traditional
+the rules in \cref{sec:compiler} is GHC's lack of traditional
 symbol tables.
 Traditionally, compilers have one or more data structures known as
 \emph{symbol tables}, which are mappings from symbols to information
@@ -200,7 +200,7 @@ \subsection{No symbol tables}
 this is referred to as ``typechecking'' the interface.
 
 \paragraph{Consequences for \Backpack{}}
-In Section~\ref{sec:overview-compiler}, we informally described
+In \cref{sec:overview-compiler}, we informally described
 types as graphs, with original names pointing to the corresponding
 declaration.  In fact, this is an accurate representation of how
 these operations are implemented in GHC\@!
@@ -241,7 +241,7 @@ \subsection{No symbol tables}
 each of the input \verb|ModIface|s for the signatures, wiring any
 local \verb|Name|s to point to the merged signature, and then performs
 the subtyping tests on the resulting graph.  In other words, the
-informal description of signature merging in Section~\ref{sec:signature-merging}
+informal description of signature merging in \cref{sec:signature-merging}
 is actually quite close to what actually occurs in GHC proper!
 
 \subsection{Miscellaneous differences}
@@ -330,7 +330,7 @@ \subsection{Miscellaneous differences}
 
     \item Modifications to GHC's \verb|UnitId| data type to support module
         substitutions.  We try to keep \uid{}s represented as plain
-        strings as much as possible; see Section~\ref{sec:opaque-uid} for
+        strings as much as possible; see \cref{sec:opaque-uid} for
         more details.
 
     \item We applied a slight optimization when testing that an instantiated
@@ -352,7 +352,7 @@ \subsection{Miscellaneous differences}
 \section{Modifications to Cabal}
 
 Our implementation of \Backpack{} in Cabal also closely follows the description
-from Section~\ref{sec:overview}.  There are three primary phases in our
+from \cref{sec:overview}.  There are three primary phases in our
 implementation:
 
 \begin{enumerate}
@@ -367,7 +367,7 @@ \section{Modifications to Cabal}
     where every \cid{} has been further elaborated into a \uid{}
     representing exactly how the dependencies are instantiated.
     Mixin linking is essentially a direct implementation of the
-    description we gave in Section~\ref{sec:mix-in}.
+    description we gave in \cref{sec:mix-in}.
 
     \item Finally, we zip through all fully instantiated components
     and recursively instantiate their dependencies, producing one or

intro.tex

@@ -184,14 +184,14 @@ \chapter{Introduction}
 
     \item We describe a package language which can be \emph{mixin
     linked} without knowing anything about the Haskell programming
-    language. (Section~\ref{sec:mix-in})  This gives us a language agnostic mechanism for
+    language. (\cref{sec:mix-in})  This gives us a language agnostic mechanism for
     expressing separate modular development, in contrast to
     \OldBackpack{}, whose semantics critically relies on the import structure
     of Haskell modules.  As a result, \Backpack{}
     employs a far simpler mixin linking procedure essentially equivalent
     to early descriptions of mixin linking in the literature.~\cite{cardelli:linksets}
     In doing so, we adjust \OldBackpack{}'s primary technical device,
-    the \emph{module identity} into a new concept, the \emph{unit identity} (Section~\ref{sec:uid}),
+    the \emph{module identity} into a new concept, the \emph{unit identity} (\cref{sec:uid}),
     which can be computed by language agnostic mixin linking.
     Our new package language is order-independent, which is
     essential for backwards-compatibility with Haskell's existing
@@ -207,7 +207,7 @@ \chapter{Introduction}
     semantics to the ones that were pioneered by \OldBackpack{}.
 
     \item We describe how to typecheck the \emph{\unit{} language} in the
-    real world (Section~\ref{sec:compiler}), typechecking the source into semantic objects that
+    real world (\cref{sec:compiler}), typechecking the source into semantic objects that
     faithfully reflect the full glory of GHC Haskell's type system.
     We give an unsound but pragmatic mechanism for supporting \emph{type classes}
     (it is unsolvable in the presence of open type families), support
@@ -217,18 +217,18 @@ \chapter{Introduction}
     roles annotations.
 
     \item This is not a paper design: Backpack has been fully
-    implemented in the upcoming GHC 8.2 and cabal-install 2.0 releases.
+    implemented GHC 8.2 and cabal-install 2.0.
     We give a tour of the modifications we made to GHC to
     implement the necessary instantiation and merging operations
     required by the \unit{} language, as well as the architectural
     changes that were necessary in Cabal (the package manager)
     to orchestrate the typechecking and building of the mixin
-    packages. (Section~\ref{sec:implementation})
+    packages. (\cref{sec:implementation})
 
     \item Does \Backpack{} work?
     We have done a number of case studies to give evidence
     that \Backpack{} works, including conversions of complex,
-    real-world packages to use \Backpack{}. (Section~\ref{sec:evaluation})
+    real-world packages to use \Backpack{}. (\cref{sec:evaluation})
 
 %   Among other things, these case studies
 %   have motivated the introduction of \emph{signature thinning}

limitations.tex

@@ -171,7 +171,7 @@ \section{Mutually recursive packages}
 We have not described how to handle mutual recursion in \Backpack{},
 although we believe that \Backpack{} can be extended to accommodate it,
 based off of GHC's existing support for \verb|hs-boot| files.
-Indeed, we showed in Section~\ref{sec:recursive-uids} that recursive
+Indeed, we showed in \cref{sec:recursive-uids} that recursive
 \uid{}s can be handled in the same way as they were done in \OldBackpack{}.
 
 One challenge that we face is how to handle the ``double vision
@@ -290,7 +290,7 @@ \section{Relaxing signature matching}
 that we should accept an implementation with type $\tau$ for a signature
 type $\tau'$, so long as there exists a \emph{coercion} from $\tau$ to
 $\tau'$ and augment our subtyping relation accordingly.  However, this will
-not work with our merging rules as stated in Figure~\ref{typing:merging}.
+not work with our merging rules as stated in \cref{typing:merging}.
 Presently, merging picks an arbitrary type to add to the context; the reasoning
 is that if all the types were actually type equal, it doesn't matter which
 one we pick.  With subtyping on Haskell level type definitions, this no

main.tex

@@ -1,6 +1,7 @@
 \documentclass{report}
 \usepackage{suthesis-2e}
 \usepackage{hyperref}
+\usepackage[capitalise]{cleveref}
 \tablespagefalse%