Remove obsolete Backpack manual.

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

11 files changed, 0 insertions, 5521 deletions

diff --git a/docs/backpack/.gitignore b/docs/backpack/.gitignore
deleted file mode 100644
index cdea05d264..0000000000
--- a/docs/backpack/.gitignore
+++ /dev/null
@@ -1,12 +0,0 @@
-*.aux
-*.bak
-*.bbl
-*.blg
-*.dvi
-*.fdb_latexmk
-*.fls
-*.log
-*.synctex.gz
-*.out
-*.toc
-backpack-impl.pdf
diff --git a/docs/backpack/Makefile b/docs/backpack/Makefile
deleted file mode 100644
index 1cf4a8d90a..0000000000
--- a/docs/backpack/Makefile
+++ /dev/null
@@ -1,10 +0,0 @@
-all: backpack-impl.pdf backpack-manual.pdf algorithm.pdf
-
-backpack-impl.pdf: backpack-impl.tex
-	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-impl.tex || ! rm -f $@
-
-backpack-manual.pdf: backpack-manual.tex
-	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-manual.tex || ! rm -f $@
-
-algorithm.pdf: algorithm.tex
-	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 algorithm.tex || ! rm -f $@
diff --git a/docs/backpack/algorithm.tex b/docs/backpack/algorithm.tex
deleted file mode 100644
index 1c5adbd91f..0000000000
--- a/docs/backpack/algorithm.tex
+++ /dev/null
@@ -1,1392 +0,0 @@
-% TODO
-%   - definite typechecker/compiler implies it only looks at the
-%   installed unit database, not TRUE
-
-
-\documentclass{article}
-
-\usepackage{pifont}
-\usepackage{graphicx} %[pdftex] OR [dvips]
-\usepackage{fullpage}
-\usepackage{wrapfig}
-\usepackage{float}
-\usepackage{titling}
-\usepackage{hyperref}
-\usepackage{tikz}
-\usepackage{color}
-\usepackage{footnote}
-\usepackage{float}
-\usepackage{algpseudocode}
-\usepackage{bigfoot}
-\usepackage{amssymb}
-\usepackage{amsmath}
-\usepackage{framed}
-
-% Alter some LaTeX defaults for better treatment of figures:
-% See p.105 of "TeX Unbound" for suggested values.
-% See pp. 199-200 of Lamport's "LaTeX" book for details.
-%   General parameters, for ALL pages:
-\renewcommand{\topfraction}{0.9}	% max fraction of floats at top
-\renewcommand{\bottomfraction}{0.8}	% max fraction of floats at bottom
-%   Parameters for TEXT pages (not float pages):
-\setcounter{topnumber}{2}
-\setcounter{bottomnumber}{2}
-\setcounter{totalnumber}{4}     % 2 may work better
-\setcounter{dbltopnumber}{2}    % for 2-column pages
-\renewcommand{\dbltopfraction}{0.9}	% fit big float above 2-col. text
-\renewcommand{\textfraction}{0.07}	% allow minimal text w. figs
-%   Parameters for FLOAT pages (not text pages):
-\renewcommand{\floatpagefraction}{0.7}	% require fuller float pages
-% N.B.: floatpagefraction MUST be less than topfraction !!
-\renewcommand{\dblfloatpagefraction}{0.7}	% require fuller float pages
-
-% remember to use [htp] or [htpb] for placement
-
-\newcommand{\I}[1]{\ensuremath{\mathit{#1}}}
-
-\newcommand{\optionrule}{\noindent\rule{1.0\textwidth}{0.75pt}}
-
-\newenvironment{aside}
-  {\begin{figure}\def\FrameCommand{\hspace{2em}}
-   \MakeFramed{\advance\hsize-\width}\optionrule\small}
-{\par\vskip-\smallskipamount\optionrule\endMakeFramed\end{figure}}
-
-\setlength{\droptitle}{-6em}
-
-\newcommand{\Red}[1]{{\color{red} #1}}
-
-\title{The Backpack algorithm}
-
-\begin{document}
-
-\maketitle
-
-\noindent Backpack introduces the \emph{Backpack language}, which is
-used to define \emph{Backpack units} that provide some modules given
-implementations for some signatures.  A Backpack unit can be
-immediately typechecked and elaborated into core; at some later point,
-each unit may then be compiled one or more times with different
-instantiations of its requirements.
-
-A unit is typechecked against the indefinite unit database
-(and the installed unit database, for units that have no
-requirements) in three steps:
-
-\begin{enumerate}
-    \item The \textbf{dependency solver} computes the module and unit
-    dependency structure of the declarations in a unit.  Specifically,
-    it produces (1) the set of \I{ModuleName}s which are required
-    by the unit, (2) a directed acyclic graph labeled by \I{Module} of
-    the modules and signatures of the unit, and (3) a directed (and acyclic, for now)
-    graph labeled by \I{UnitId} of the includes of the unit.
-
-    \item The \textbf{shaper} takes each module/signature in the DAG and
-    computes its \I{Shape}, i.e., the list of \I{AvailInfo}s which are
-    provided/required by each module/signature (respectively).  This
-    step is interleaved with the next step.
-
-    \item The \textbf{type checker} takes each
-    module/signature in the DAG (annotated with its shape) and type
-    checks it.  Cabal will save these type checking results
-    in the indefinite unit database under the \I{ComponentId} associated
-    with this unit.
-\end{enumerate}
-
-At some later point in time, a unit may be compiled against
-the installed unit database, if the user specifies a mapping which
-instantiates the requirements of a unit (a mapping from \I{ModuleName}s to \I{Module}s):
-
-\begin{enumerate}
-    \item The \textbf{dependency solver} operates as before, but it also
-    is responsible for computing the full set of \I{InstalledUnitId}s which
-    must be compiled before this unit can be compiled, and compiling
-    them.
-
-    \item The \textbf{shaper} is not needed. (ToDo: except for recursive
-    module loops.)
-
-    \item The \textbf{type checker and compiler} takes each
-    module/signature in the DAG, and typechecks and compiles the unit.
-    Cabal will save the type checking results and object
-    code to the installed unit database under the \I{InstalledUnitId}
-    associated with this (instantiated) unit.
-\end{enumerate}
-
-\Red{ToDo: Rewrite this for added clarity}
-
-\newpage
-
-\section{Front-end syntax}
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-p,q,r && \mbox{Component names} \\
-m,n   && \mbox{Module names} \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Units}} \\
-  \I{unit} & ::= & \verb|unit|\; p\; [\I{provreq}]\; \verb|where {| d_1 \verb|;| \ldots \verb|;| d_n \verb|}| \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Declarations}} \\
-  d & ::= & \verb|module|\;    m \; [exports]\; \verb|where|\; \I{body} \\
-    & |   & \verb|signature|\; m \; [exports]\; \verb|where|\; \I{body} \\
-    & |   & \verb|include|\; p \; [provreq] \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Provides/requires specification}} \\
-\I{provreq} & ::= & \verb|(| \, \I{rns} \, \verb|)| \; 
-        [ \verb|requires(|\, \I{rns} \, \verb|)| ] \\
-\I{rns} & ::= & \I{rn}_0 \verb|,| \, \ldots \verb|,| \, \I{rn}_n [\verb|,|] & \mbox{Renamings} \\
-\I{rn} & ::= & m\; \verb|as| \; n & \mbox{Renaming} \\[1em] 
-\multicolumn{3}{l}{\mbox{\bf Haskell code}} \\
-\I{exports} & & \mbox{A Haskell module export list} \\
-\I{body}    & & \mbox{A Haskell module body} \\
-\end{array}
-$$
-\caption{Syntax of Backpack} \label{fig:syntax}
-\end{figure}
-
-A (slightly simplified) syntax of Backpack is given in Figure~\ref{fig:syntax}.
-
-\newpage
-\section{Unit databases and the unit renamer}
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-\multicolumn{3}{l}{\mbox{\bf Identifiers}} \\
-  \I{ComponentId} & ::= & \mbox{Opaque unique identifier}  \\
-  \I{UnitId} & ::= & \I{ComponentId} \verb|(|\, \I{HoleMap}\, \verb|)|  \\
-              & | & \verb|hole| \\
-  \I{HoleMap} & ::= & \I{ModuleName}\; \verb|->|\; \I{Module}\; \verb|,|\, \ldots \\
-  \I{Module} & ::= & \I{UnitId} \verb|:| \I{ModuleName}  \\
-  \I{InstalledUnitId} & ::= & \I{UnitId} \quad \mbox{(with no occurrences of \texttt{hole})} \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Unit databases}} \\
-  \I{ComponentDb} & ::= & \I{ComponentId} \; \verb|->| \; \I{ComponentRecord} \verb|,|\, \ldots \\
-  \I{InstalledUnitDb} & ::= & \I{InstalledUnitId} \; \verb|->| \; \I{InstalledUnitRecord} \verb|,|\, \ldots \\
-\end{array}
-$$
-\caption{Unit identification} \label{fig:ids}
-\end{figure}
-
-\subsection{The component and unit database}
-
-To install a package so that it is available when other packages are compiled,
-we must record it in some sort of database (which the compiler will query later).
-The obvious design for such a database is for it to record \emph{installed packages},
-each of which has a collection of object files and interfaces from a compilation.
-However, with Backpack, we have to refine this picture in two ways:
-
-\begin{enumerate}
-    \item A package is always a unit of distribution: something that has
-    single authorship and is uploaded to Hackage.  It would seriously hamper
-    modular programming in the small, however, if you always had to create
-    a new package to abstract over some requirements.  So we say that a
-    package can define multiple \emph{components}.  The \emph{component database}
-    records typechecked components.
-    \item  In Backpack, it may not be possible to \emph{compile} a component
-    at install time: it may depend on some (as yet) unspecified holes.
-    A component that is compiled to a specific instantiation is called a
-    \emph{unit}.  Thus, we maintain a second \emph{installed unit database}
-    which records compiled units; the \emph{component database} contains
-    typechecked-only components.  (In practice, these two database are
-    stored together, as components with no holes live both in the component
-    database and the installed unit database.)
-\end{enumerate}
-%
-Thus, there are four closely related types of identifier to be aware of:
-
-\begin{description}
-\item[Component IDs]  A component ID uniquely represents a component
-in a Cabal package, including the name and version of the containing package,
-the transitive dependencies of the component, and even the build information
-for the component.  This ID is opaque to GHC and selected by Cabal
-(although GHC may take a component ID and suffix it with a unit name to
-derive a new component ID.)  Component IDs identity entries in the
-\textbf{component database}, which contains the results of typechecking
-a component, but no actual object code.  However, it does contain the
-elaborated source, so that it can be built into actual code when
-the requirement is filled.
-
-\item[Unit ID]  A unit ID is a component ID augmented with a
-\I{HoleMap}, which says how the requirements of the component are
-instantiated.  Every component ID induces a unit ID, where each
-requirement is filled with a fictitious unit \verb|hole|: when we
-typecheck a component for the component database, it is as if we are
-``compiling'' it instantiated with holes.  Units instantiated with holes
-are never installed; they are strictly for type-checking (although we
-could generate code for them, which could be linked if the \verb|hole|
-symbols are rewritten to their true destinations).
-
-\item[Installed unit IDs]  An installed unit ID is a unit ID which has
-no \verb|hole|s; it identifies a unit that can be compiled.  The
-\textbf{installed unit database} caches the compilation results of these
-units, so that if a unit is compiled multiple times with the same
-instantiation, this code can be reused. (This database most closely
-resembles the existing installed package database with GHC today.)
-\end{description}
-
-\subsection{The unit renamer}
-
-The unit renamer is responsible for transforming component names in a
-Backpack file into \I{ComponentId}s, so that they can be uniquely
-identified in the component database.
-Given a base \I{ComponentId} of the library component we are compiling (\I{ThisComponentId})
-and a mapping from $p$ to \I{ComponentId} (\I{ComponentNameMap}), we rename
-as follows:
-
-\begin{itemize}
-    \item Every unit declaration $\verb|unit|\; p$ is renamed to $\I{ThisComponentId}\, \verb|-|\, p$.
-    \item Every unit include $\verb|include|\; p$ is renamed to $\I{ThisComponentId}\, \verb|-|\, p$ if $p$ was declared in the Backpack file; otherwise it is renamed according to \I{ComponentNameMap}.
-\end{itemize}
-
-The \I{ComponentNameMap} is entirely user specified, so there is a great deal
-of flexibility on how it can be created, but the convention we expect to
-be used by Cabal is that a component name $p$ corresponds to the same-named
-unit in a \emph{package} named $p$.  Packages that don't use Backpack
-only have one component, the library component, which has the same name as package.
-
-\paragraph{Notational conventions}
-In the rest of this document, when it is unambiguous, we will use $p$, $q$ and $r$
-interchangeably with \I{ComponentId}, as after unit renaming, there
-are no occurrences of component names.
-
-\newpage
-\section{Dependency solver}
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-  \tilde{d} & ::= & \verb|module|\;    Module \; [exports]\; \verb|where|\; \I{body} \\
-    & |   & \verb|signature|\; \I{Module} \; [exports]\; \verb|where|\; \I{body} \\
-    & |   & \verb|merge|\; \I{Module} \\
-    & |   & \verb|include|\; \I{UnitId} \\
-  \I{ComponentRecord}^{\mathsf{dep}} & ::= & \verb|provides:|\; m\; \verb|->|\; \I{Module}\verb|,|\, \ldots\\
-    & & \verb|requires:|\; m\verb|,|\, \ldots
-\end{array}
-$$
-\caption{Resolved declarations} \label{fig:resolved}
-\end{figure}
-
-The dependency solver computes the unfilled requirements of a component, a
-dependency DAG on the modules/signatures in the component, and a dependency
-DAG on the includes in the component.  We assume every referenced $p$ in the
-component must be recorded in the component database, such that we can
-look up $\I{ComponentRecord}^{\mathsf{dep}}$.
-
-\paragraph{Computing unfilled requirements}  The unfilled requirements are $R-P$, where $R$ and $P$ are sets of module names computed from the declarations in the following manner:
-
-\begin{itemize}
-    \item $\verb|include|\; p$: union the (domain of the) provisions with $P$ and the requirements with $R$.
-    \item $\verb|module|\; m$: add $m$ to $P$.
-    \item $\verb|signature|\; m$: add $m$ to $R$.
-\end{itemize}
-
-\paragraph{Declaration dependency graph}
-We define a graph where the nodes are as described in Figure~\ref{fig:resolved}:
-there is a node per
-for each module and signature, as well as an extra ``merge'' node for
-every unfilled requirement, which merges the interfaces of a local signature and
-any requirements brought in from includes.
-%
-Each node is identified by the tuple $\left(\I{Module}, \I{IsSource?}\right)$, where
-the \I{Module} of a declaration $m$ in component $p$ is \verb|p(H):m|, where $H$ maps
-each unfilled requirement $n$ to \verb|hole:n|, and \I{IsSource?} is true only for signatures.
-
-The edges of the directed graph signify a ``depends on'' relation, and are
-defined as follows:
-
-\begin{itemize}
-    \item A module/signature $m$ depends on a module/signature merge $n$ if $m$ imports $n$.
-    \item A module/signature $m$ depends on a signature $n$ if $m$ \verb|{-# SOURCE #-}| imports $n$.
-    \item A module/signature merge $m$ depends on a local signature $m$ (if it exists).
-\end{itemize}
-%
-If the resulting graph has a cycle, this is an error.
-
-\paragraph{Include dependency graph}  We define an dependency graph
-between includes, where an $\verb|include|\; p$ depends on
-$\verb|include|\; q$ if, for some module name $m$, $p$ requires $m$ and
-$q$ provides $m$.  If there is a cyclic, then there is cross-component
-mutual recursion: for now, this is an error.
-
-Assuming an acyclic graph, we can compute the \I{UnitId} of each
-key as follows.  Initialize $\Gamma$, a substitution from holes to \I{Module},
-to the identity substitution. For each $\verb|include|\; p$ in topological
-order, define its \I{UnitId} to be $p$ with the mapping $\Gamma$ with its
-domain restricted to the requirements of $p$.  Then, for each provision
-$m\; \verb|->|\; \I{Module}$, update $\Gamma$ so that
-$\Gamma(m) = \operatorname{subst} (\Gamma, \I{Module})$
-(where $\operatorname{subst}$ recursively applies the substitution $\Gamma$ in \I{Module}).
-
-During compilation, the include dependency graph is useful for
-determining a compilation order for included units.
-
-\newpage
-\section{Requirement calculation}
-
-\Red{to write}
-
-\newpage
-\section{Shaping pass}
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-\I{Shape} & ::= & \verb|provides:|\; m \; \verb|->|\; \I{Module}\; \I{ModShape} \verb|;|\; \ldots \\
-      &     & \verb|requires:| \; m \; \verb|->|\; \textcolor{white}{\I{Module}}\; \I{ModShape}  \verb|;|\; \ldots \\
-\I{ModShape} & ::= & \I{AvailInfo}_0 \verb|,|\, \ldots \verb|,|\, \I{AvailInfo}_n \\
-\I{AvailInfo} & ::= & \I{Name} & \mbox{Plain identifiers} \\
-          & |   & \I{Name} \, \verb|{| \, \I{Name}_0\verb|,| \, \ldots\verb|,| \, \I{Name}_n \, \verb|}| & \mbox{Type constructors} \\
-\I{Name}   & ::= & \I{Module} \verb|.| \I{OccName} \\
-\I{OccName} & & \mbox{Unqualified name in a namespace} \\
-\I{ComponentRecord}^{\mathsf{shape}} & ::= & \I{Shape}
-\end{array}
-$$
-\caption{Shaping} \label{fig:shaping}
-\end{figure}
-
-The shaping pass computes the export \I{AvailInfo}s for each node in
-the dependency graph; collectively, these form the \I{Shape} of
-the unit described in Figure~\ref{fig:shaping}.  Equivalently,
-the \I{Shape} of unit specifies what a unit requires and provides
-at the Haskell declaration level.
-
-An \I{AvailInfo} names a Haskell declaration that may be exported.
-It may be a plain identifier \I{Name}, or it may be a type constructor,
-in which case it has children \I{Name}s representing the names of the
-data constructors, record selectors, etc.  This level of hierarchy
-makes it possible to use ellipses in an import list, e.g. \verb|TyCon(..)|,
-to selectively import just the logical children of a type constructor.
-Children names have the invariant that they have the same \I{Module} as the parent name.
-In a \I{ModShape}/export list,
-the \I{OccName}s of the plain identifier \I{AvailInfo}s and the \emph{children}
-of type constructor are unique
-(although the top-level \I{Name}s may not have unique \I{OccName}s).
-
-The compilation of every node is associated with a ``shape context'',
-which represents the modules which are transitively depended upon. Let the
-environment shape context is the merge of the shapes of all includes; to
-shape a node:
-
-\begin{enumerate}
-    \item Merge the environment shape contexts with the shape contexts
-    of all direct dependencies, resulting in the initial shape context.
-    \item Rename the module/signature according to the initial shape context,
-    getting a \I{ModShape}.  Importantly, when renaming the signature \verb|M|,
-    any declarations defined in the signature are assigned a \I{Name}s with the \I{Module} \verb|hole:M| (rather than a \I{Module} based on the current unit $p$).
-    \item Merge this \I{ModShape} into the initial shape context
-    (modules go in provisions while signatures go in provisions), the
-    result defining the shape context of this node.
-\end{enumerate}
-
-We now elaborate on these steps in more detail.
-
-\subsection{Shapes of includes}
-Given an \verb|include p (X) requires (Y)|, we can look up the shape
-for $p$ from the indefinite package database.  However, an include can
-also rename provisions and requires (where $X$, $Y$ are partial maps
-from module name to module name), which requires transforms the shape
-in the following way:
-
-\begin{itemize}
-    \item For each original provision $m\; \verb|->|\; \ldots$, provide
-          $X (m)\; \verb|->|\; \ldots$ if $X (m)$ is defined.
-    \item For each original requirement $m\; \verb|->|\; \ldots$, require
-          $Y (m)\; \verb|->|\; \ldots$ if $Y (m)$ is defined, and $m$ if it is not.
-          (Non-mentioned requirements are always passed through).
-    \item For each requirement renaming from \verb|M| to \verb|N| in $Y$, substitute
-          all occurrences of \verb|hole:M| to \verb|hole:N| in the \I{ModShape}
-          of all provisions and requirements.
-\end{itemize}
-
-\subsection{Shape merging}
-Before specifying the how to merge shapes algorithm, we must define some subprocedures
-for unifying and merging lower-level entities such as \I{AvailInfo}s and \I{Name}s,
-which produce \I{Name} substitution that are applied to shapes.
-
-\begin{description}
-    \item[Unify two \textit{Name}s]
-    (produces a \I{Name} and a \I{Name} substitution) \\
-    Error if the names do not have matching \I{OccName}s.  Error if neither name
-    is a hole name.  Otherwise, without loss of generality let $m$ be the hole name
-    and $n$ the other name, return $n$ and the substitution of $m$ to $n$.
-    \item[Merge two sets of \textit{Name}s]
-    (produces a set of \I{Name}s and a \I{Name} substitution) \\
-    Let two \I{Name}s be related if they have the same \I{OccName}.
-    Union the two sets, unifying related names.
-    \item[Unify two \textit{AvailInfo}s]
-    (produces an \I{AvailInfo} and a \I{Name} substitution) \\
-    If both \I{AvailInfo}s are simply
-    a \I{Name}, unify the two \I{Name}s.  If both \I{AvailInfo}s are
-    $\I{Name}\, \verb|{|\, \I{Name}_0\verb|,|\, \ldots\verb|,|\, \I{Name}_n\, \verb|}|$,
-    unify the top-level \I{Name}, apply the substitution to both \I{AvailInfo}s,
-    and return the unified \I{Name} with the union of the child names of the
-    substituted \I{AvailInfo}s.
-    Otherwise, error.
-    \item[Merge two sets of \textit{AvailInfo}s]
-    (produces a set of \I{AvailInfo}s and a \I{Name} substitution) \\
-    Let two \I{AvailInfo}s be related if they both are of the form
-    \I{Name} and have matching \I{OccName}s, or if they both are of
-    the form
-    $\I{Name}\, \verb|{|\, \I{Name}_0\verb|,|\, \ldots\verb|,|\, \I{Name}_n\, \verb|}|$
-    and there exists a child name in each which have matching \I{OccName}s.
-    Union the two sets, unifying related \I{AvailInfo}s.
-    \item[Apply a name substitution on an \textit{AvailInfo}] (produces an \I{AvailInfo}) \\
-    Substitute the top-level \I{Name}, which induces a substitution from
-    \I{Module} to $\I{Module}'$.  Apply this module substitution to each child
-    \I{Name} in the \I{AvailInfo}.
-
-\end{description}
-%
-Shape merging takes two units with inputs (requirements) and outputs
-(provisions) and ``wires'' them up so that outputs feed into inputs. To
-merge the shape of $p$ with the shape of $q$:
-
-\begin{enumerate}
-    \item \emph{Fill every requirement of $q$ with provided modules from
-        $p$.} For each requirement $M$ of $q$ that is provided by $p$,
-        substitute each \I{Module} occurrence of \verb|hole:M| with the
-        provided $p\verb|(|M\verb|)|$ (however, do \textbf{NOT} substitute the
-        top-level \I{Module} in a \I{Name}s), merge the \I{AvailInfo}s and apply
-        the resulting \I{Name} substitution, and
-        remove the requirement from $q$.  If the \I{AvailInfo}s of the
-        provision are not a superset of the required \I{AvailInfo}s,
-        error.
-    \item If mutual recursion is supported, \emph{fill every requirement
-        of $p$ with provided modules from $q$.}
-    \item \emph{Merge leftover requirements.}  For each requirement $M$
-        of $q$ that is not provided by $p$ but required by $p$, and let
-        the new requirement be the merge of
-        \I{AvailInfo}s, applying the resulting \I{Name} substitution.
-    \item \emph{Add provisions of $q$.} Union the provisions of $p$ and $q$, (lazily) erroring
-        if there is a duplicate that doesn't have the same \I{Module}.
-\end{enumerate}
-
-\newpage
-\section{Indefinite type checker}
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-\I{ComponentRecord} & ::= & \I{ModIface}_0 \verb|;|\, \ldots\verb|;|\, \I{ModIface}_n \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Module interface}} \\
-\I{ModIface} & ::= & \verb|module| \; \I{Module} \; \verb|(| \I{mi\_exports} \verb|)| \; \verb|where| \\
-& & \qquad \I{mi\_decls} \\
-& & \qquad \I{mi\_insts} \\
-& & \qquad \I{dep\_orphs} \\
-\I{mi\_exports} & ::= & \I{AvailInfo}_0 \verb|,|\, \ldots \verb|,|\, \I{AvailInfo}_n & \mbox{Export list} \\
-\I{mi\_decls} & ::= & \I{IfaceDecl}_0 \verb|;|\, \ldots \verb|;|\, \I{IfaceDecl}_n & \mbox{Defined declarations} \\
-\I{mi\_insts} & ::= & \I{IfaceClsInst}_0 \verb|;|\, \ldots \verb|;|\, \I{IfaceClsInst}_n & \mbox{Defined instances} \\
-\I{dep\_orphs} & ::= & \I{Module}_0 \verb|;|\, \ldots \verb|;|\, \I{Module}_n & \mbox{Transitive orphan dependencies} \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Interface declarations}} \\
-\I{IfaceDecl} & ::= & \I{OccName} \; \verb|::| \; \I{IfaceId} \\
-              & |   & \verb|data| \; \I{OccName} \; \verb|=| \;\ \I{IfaceData} \\
-              & |   & \ldots \\
-\I{IfaceClsInst} & & \mbox{A type-class instance} \\
-\I{IfaceId} & & \mbox{Interface of top-level binder} \\
-\I{IfaceData} & & \mbox{Interface of type constructor} \\
-\end{array}
-$$
-\caption{Module interfaces in GHC} \label{fig:typecheck}
-\end{figure}
-
-\Red{This needs updating.}
-
-In general terms,
-type checking an indefinite unit (a unit with holes) involves
-calculating, for every module, a \I{ModIface} representing the
-type/interface of the module in question (which is serialized
-to disk).  The general form of these
-interface files are described in Figure~\ref{fig:typecheck}; notably,
-the interfaces \I{IfaceId}, \I{IfaceData}, etc. contain \I{Name} references,
-which must be resolved by
-looking up a \I{ModIface} corresponding to the \I{Module} associated
-with the \I{Name}. (We will say more about this lookup process shortly.)
-For example, given:
-
-\begin{verbatim}
-    unit p where
-        signature H where
-            data T
-        module A(S, T) where
-            import H
-            data S = S T
-\end{verbatim}
-%
-the \I{PkgType} is:
-
-\begin{verbatim}
-    module hole:H (hole:H.T) where
-        data T -- abstract type constructor
-    module THIS:A (THIS:A.S, hole:H.T) where
-        data S = S hole:H.T
-    -- where THIS = p(H -> hole:H)
-\end{verbatim}
-%
-However, while it is true that the \I{ModIface} is the final result
-of type checking, we actually are conflating two distinct concepts: the user-visible
-notion of a \I{ModuleName}, which, when imported, brings some \I{Name}s
-into scope (or could trigger a deprecation warning, or pull in some
-orphan instances\ldots), versus the actual declarations, which, while recorded
-in the \I{ModIface}, have an independent existence: even if a declaration
-is not visible for an import, we may internally refer to its \I{Name}, and
-need to look it up to find out type information.  (A simple case when
-this can occur is if a module exports a function with type \verb|T -> T|,
-but doesn't export \verb|T|).
-
-\begin{figure}[htpb]
-$$
-\begin{array}{rcll}
-\I{ModDetails} & ::= & \langle\I{md\_types} \verb|;|\; \I{md\_insts}\rangle \\
-\I{md\_types}  & ::= & \I{TyThing}_0 \verb|,|\, \ldots\verb|,|\, \I{TyThing}_n \\
-\I{md\_insts}  & ::= & \I{ClsInst}_0 \verb|,|\, \ldots\verb|,|\, \I{ClsInst}_n \\[1em]
-\multicolumn{3}{l}{\mbox{\bf Type-checked declarations}} \\
-\I{TyThing}    &     & \mbox{Type-checked thing with a \I{Name}} \\
-\I{ClsInst}    &     & \mbox{Type-checked type class instance} \\
-\end{array}
-$$
-\caption{Semantic objects in GHC} \label{fig:typecheck-more}
-\end{figure}
-
-Thus, a \I{ModIface} can be type-checked into a \I{ModDetails}, described in
-Figure~\ref{fig:typecheck-more}.  Notice that a \I{ModDetails} is just
-a bag of type-checkable entities which GHC knows about.  We
-define the \emph{external package state (EPT)} to
-simply be the union of the \I{ModDetails}
-of all external modules.
-
-Type checking is a delicate balancing act between module
-interfaces and our semantic objects.  A \I{ModIface} may get
-type-checked multiple times with different hole instantiations
-to provide multiple \I{ModDetails}.
-Furthermore complicating matters
-is that GHC does this resolution \emph{lazily}: a \I{ModIface}
-is only converted to a \I{ModDetails} when we are looking up
-the type of a \I{Name} that is described by the interface;
-thus, unlike usual theoretical treatments of type checking, we can't
-eagerly go ahead and perform substitutions on \I{ModIface}s when
-they get included.
-
-In a separate compiler like GHC, there are two primary functions we must provide:
-
-\paragraph{\textit{ModuleName} to \textit{ModIface}}  Given a \I{ModuleName} which
-was explicitly imported by a user, we must produce a \I{ModIface}
-that, among other things, specifies what \I{Name}s are brought
-into scope.  This is used by the renamer to resolve plain references
-to identifiers to real \I{Name}s.  (By the way, if shaping produced
-renamed trees, it would not be necessary to do this step!)
-
-\paragraph{\textit{Module} to \textit{ModDetails}/EPT}  Given a \I{Module} which may be
-a part of a \I{Name}, we must be able to type check it into
-a \I{ModDetails} (usually by reading and typechecking the \I{ModIface}
-associated with the \I{Module}, but this process is involved).  This
-is used by the type checker to find out type information on things. \\
-
-There are two points in the type checker where these capabilities are exercised:
-
-\paragraph{Source-level imports}  When a user explicitly imports a
-module, the \textit{ModuleName} is mapped to a \textit{ModIface}
-to find out what exports are brought into scope (\I{mi\_exports})
-and what orphan instances must be loaded (\I{dep\_orphs}).  Additionally,
-the \textit{Module} is loaded to the EPT to bring instances from
-the module into scope.
-
-\paragraph{Internal name lookup}  During type checking, we may have
-a \I{Name} for which we need type information (\I{TyThing}).  If it's not already in the
-EPT, we type check and load
-into the EPT the \I{ModDetails} of the \I{Module} in the \I{Name},
-and then check the EPT again. (\verb|importDecl|)
-
-\subsection{\textit{ModuleName} to \textit{ModIface}}
-
-In all cases, the \I{mi\_exports} can be calculated directly from the
-shaping process, which specifies exactly for each \I{ModuleName} in scope
-what will be brought into scope.
-
-\paragraph{Modules} Modules are straightforward, as for any
-\I{Module} there is only one possibly \I{ModIface} associated
-with it (the \I{ModIface} for when we type-checked the (unique) \verb|module|
-declaration.)
-
-\paragraph{Signatures} For signatures, there may be multiple \I{ModIface}s
-associated with a \I{ModuleName} in scope, e.g. in this situation:
-
-\begin{verbatim}
-    unit p where
-        signature S where
-            data A
-    unit q where
-        include p
-        signature S where
-            data B
-        module M where
-            import S
-\end{verbatim}
-%
-Each literal \verb|signature| has a \I{ModIface} associated with it; and
-the import of \verb|S| in \verb|M|, we want to see the \emph{merged}
-\I{ModIface}s.  We can determine the \I{mi\_exports} from the shape,
-but we also need to pull in orphan instances for each signature, and
-produce a warning for each deprecated signature.
-
-\begin{aside}
-\textbf{Does hiding a signature hide its orphans.} Suppose that we have
-extended Backpack to allow hiding signatures from import.
-
-\begin{verbatim}
-    unit p requires (H) where -- H is hidden from import
-        module A where
-            instance Eq (a -> b) where -- orphan
-        signature H {-# DEPRECATED "Don't use me" #-} where
-            import A
-
-    unit q where
-        include p
-        signature H where
-            data T
-        module M where
-            import H                -- warn deprecated?
-            instance Eq (a -> b)    -- overlap?
-\end{verbatim}
-
-It is probably the most consistent to not pull in orphan instances
-and not give the deprecated warning: this corresponds to merging
-visible \I{ModIface}s, and ignoring invisible ones.
-\end{aside}
-
-\subsection{\textit{Module} to \textit{ModDetails}}
-
-\paragraph{Modules}  For modules, we have a \I{Module} of
-the form $\I{p}\verb|(|m\; \verb|->|\; \I{Module}\verb|,|\, \ldots\verb|)|$,
-and we also have a unique \I{ModIface}, where each hole instantiation
-is $\verb|hole:|m$.
-
-To generate the \I{ModDetails} associated with the specific instantiation,
-we have to type-check the \I{ModIface} with the following adjustments:
-
-\begin{enumerate}
-    \item Perform a \I{Module} substitution according to the instantiation
-          of the \I{ModIface}'s \I{Module}. (NB: we \emph{do}
-          substitute \verb|hole:A.x| to \verb|hole:B.x| if we instantiated
-          \verb|A -> hole:B|, \emph{unlike} the disjoint
-          substitutions applied by shaping.)
-    \item Perform a \I{Name} substitution as follows: for any name
-          with a unit key that is a $\verb|hole|$,
-          substitute with the recorded \I{Name} in the requirements of the shape.
-          Otherwise, look up the (unique) \I{ModIface} for the \I{Module},
-          and substitute with the corresponding \I{Name} in the \I{mi\_exports}.
-\end{enumerate}
-
-\paragraph{Signatures}  For signatures, we have a \I{Module} of the form
-$\verb|hole:|m$.  Unlike modules, there are multiple \I{ModIface}s associated with a hole.
-We distinguish each separate \I{ModIface} by considering the full \I{UnitId}
-it was defined in, e.g. \verb|p(A -> hole:C, B -> q():B)|; call this
-the hole's \emph{defining unit key}; the set of \I{ModIface}s for a hole
-and their defining unit keys can easily be calculated during shaping.
-
-To generate the \I{ModDetails} associated with a hole, we type-check each
-\I{ModIface}, with the following adjustments:
-
-\begin{enumerate}
-    \item Perform a \I{Module} substitution according to the instantiation
-        of the defining unit key.  (NB: This may rename the hole itself!)
-    \item Perform a \I{Name} substitution as follows, in the same manner
-        as would be done in the case of modules.
-    \item When these \I{ModDetails} are merged into the EPT, some merging
-        of duplicate types may occur; a type
-        may be defined multiple times, in which case we check that each
-        definition is compatible with the previous ones.  A concrete
-        type is always compatible with an abstract type.
-\end{enumerate}
-
-\paragraph{Invariants} When we perform \I{Name} substitutions, we must be
-sure that we can always find out the correct \I{Name} to substitute to.
-This isn't obviously true, consider:
-
-\begin{verbatim}
-    unit p where
-        signature S(foo) where
-            data T
-            foo :: T
-        module M(bar) where
-            import S
-            bar = foo
-    unit q where
-        module A(T(..)) where
-            data T = T
-            foo = T
-        module S(foo) where
-            import A
-        include p
-        module A where
-            import M
-            ... bar ...
-\end{verbatim}
-%
-When we type check \verb|p|, we get the \I{ModIface}s:
-
-\begin{verbatim}
-    module hole:S(hole:S.foo) where
-        data T
-        foo :: hole:S.T
-    module THIS:M(THIS:M.bar) where
-        bar :: hole:S.T
-\end{verbatim}
-%
-Now, when we type check \verb|A|, we pull on the \I{Name} \verb|p(S -> q():S):M.bar|,
-which means we have to type check the \I{ModIface} for \verb|p(S -> q():S):M|.
-The un-substituted type of \verb|bar| has a reference to \verb|hole:S.T|;
-this should be substituted to \verb|q():S.T|.  But how do we discover this?
-We know that \verb|hole:S| was instantiated to \verb|q():S|, so we might try
-and look for \verb|q():S.T|.  However, this \I{Name} does not exist because
-the \verb|module S| reexports the selector from \verb|A|!  Nor can we consult
-the (unique) \I{ModIface} for the module, as it doesn't reexport the relevant
-type.
-
-The conclusion, then, is that a module written this way should be disallowed.
-Specifically, the correctness condition for a signature is this: \emph{Any \I{Name}
-mentioned in the \I{ModIface} of a signature must either be from an external module, or be
-exported by the signature}.
-
-\newpage
-\section{Installation}
-
-This section defines the syntax for the file-system format of the \I{ComponentDb}.
-Like entries in the installed unit database, an entry is a sequence of fields
-with values.
-
-Indefinite unit entries share some entries in common with entries in the installed
-unit database:
-
-\begin{description}
-    \item[\texttt{component-id:}] \I{ComponentId} \newline
-        The unique identifier of an installed package.  This combined
-        with \texttt{unit-name} uniquely identifies an entry in the
-        installed unit database.
-    \item[\texttt{exposed:}] \verb|True| or \verb|False| \newline
-        Whether or not this unit is exposed, i.e. it is available for
-        \verb|include| under its \verb|unit-name| (this is used to compute
-        the default \I{ComponentNameMap} when GHC is called by itself).
-    \item[\texttt{import-dirs:}] \I{FilePath} \newline
-        Where interface files for this unit can be found. (NB: these
-        interface files are templates, which contain references to holes
-        which we can substitute.)  (There's exactly one.)
-    \item[\texttt{exposed-modules:}] \I{ModuleName} or \I{ModuleName} \texttt{from} \I{Module} $\ldots$ \newline
-        The set of exposed modules from this unit, including reexports from
-        other units.
-    \item[\texttt{other-modules:}] \I{ModuleName} $\ldots$ \newline
-        Non-exposed modules; there is an interface for each of these
-        in the import-dirs. (Redundant, but useful for error reporting.)
-\end{description}
-%
-As well as all non-essential, Cabal-specific metadata; e.g. \texttt{name}, \texttt{version}, \ldots (\texttt{data-dir} and \texttt{haddock} probably)
-Here are new entries for indefinite units:
-
-\begin{description}
-    \item[\texttt{requires:}] \I{ModuleName} \ldots \newline
-        The set of module names which are requirements of this unit.
-        (Installed units instead record \texttt{instantiated-with}, which
-        specifies how each requirement was instantiated.)  Every
-        requirement has an interface in the import-dirs.
-    \item[\texttt{source-dir:}] \I{FilePath} \newline
-        The path to the original source of the package.
-    \item[\texttt{setup-executable:}] \I{FilePath} \newline
-        The path to the \texttt{Setup} executable as described by the Cabal
-        specification which is capable of building and installing the package
-        using \texttt{./Setup instantiate} (this is a new command which lets
-        us program how the requirements of the indefinite unit should be filled),
-        \texttt{./Setup build}, \texttt{./Setup copy} and
-        \texttt{./Setup register}.
-    \item[\texttt{package-config:}] \I{FilePath} \newline
-        The path to the package configuration saved when the indefinite
-        unit was installed.  This should contain all of the relevant configuration
-        information necessary to build a package, except how its requirements
-        are instantiated.
-\end{description}
-%
-The string representation of \I{Module} is worth remarking upon.  In
-this specification, \I{Module} is a recursive data structure.  For
-installed packages, it is acceptable to flatten \I{Module} into a
-hash representing the \I{UnitId} and the \I{ModuleName}, as the \I{UnitId}
-is an \I{InstalledUnitId} which has an entry in the database.  However,
-this is unacceptable for indefinite units, because we don't have an
-entry per \I{UnitId}.  So, for \I{UnitId}s in the indefinite unit database,
-the full tree is written out, subject to this syntax:
-
-\begin{verbatim}
-Module ::= UnitId ":" ModuleName
-UnitId ::= InstalledPackageId
-          [ "/" UnitName "(" HoleMap ")" ]
-          | "hole"
-HoleMap ::= ModuleName "->" Module "," ...
-\end{verbatim}
-
-\section{Appendix: Shaping}
-
-This section clarifies some subtle aspects about shaping.
-
-\subsection{\textit{OccName} is implied by \textit{Name}}
-In Haskell, the following is not valid syntax:
-
-\begin{verbatim}
-    import A (foobar as baz)
-\end{verbatim}
-In particular, a \I{Name} which is in scope will always have the same
-\I{OccName} (even if it may be qualified.)  You might imagine relaxing
-this restriction so that declarations can be used under different \I{OccName}s;
-in such a world, we need a different definition of shape:
-
-\begin{verbatim}
-    Shape ::=
-        provided: ModuleName -> Module { OccName -> Name }
-        required: ModuleName ->        { OccName -> Name }
-\end{verbatim}
-Presently, however, such an \I{OccName} annotation would be redundant: it can be inferred from the \I{Name}.
-
-\subsection{Holes of a unit are a mapping, not a set.}
-
-Why can't the \I{UnitId} just record a
-set of \I{Module}s, e.g. $\I{UnitId}\;::= \; p \; \verb|{| \; \I{Module} \; \verb|}|$?  Consider:
-
-\begin{verbatim}
-    unit p (A) requires (H1, H2) where
-        signature H1(T) where
-            data T
-        signature H2(T) where
-            data T
-        module A(A(..)) where
-            import qualified H1
-            import qualified H2
-            data A = A H1.T H2.T
-
-    unit q (A12, A21) where
-        module I1(T) where
-            data T = T Int
-        module I2(T) where
-            data T = T Bool
-        include p (A as A12) requires (H1 as I1, H2 as I2)
-        include p (A as A21) requires (H1 as I2, H2 as I1)
-\end{verbatim}
-With a mapping, the first instance of \verb|p| has key \verb|p(H1 -> q():I1, H2 -> q():I2)|
-while the second instance has key \verb|p(H1 -> q():I2, H2 -> q():I1)|; with
-a set, both would have the key \verb|p{q():I1, q():I2}| and be
-indistinguishable.
-
-\subsection{Signatures can require a specific entity.}
-With requirements like \verb|A -> { hole:A.T, hole:A.foo }|,
-why not specify it as \verb|A -> { T, foo }|,
-e.g., \verb|required: { ModuleName -> { OccName } }|?  Consider:
-
-\begin{verbatim}
-    unit p () requires (A, B) where
-        signature A(T) where
-            data T
-        signature B(T) where
-            import T
-\end{verbatim}
-The requirements of this unit specify that \verb|A.T| $=$ \verb|B.T|; this
-can be expressed with \I{Name}s as
-
-\begin{verbatim}
-    A -> { hole:A.T }
-    B -> { hole:A.T }
-\end{verbatim}
-But, without \I{Name}s, the sharing constraint is impossible:  \verb|A -> { T }; B -> { T }|. (NB: \verb|A| and \verb|B| could be filled with different modules, they just have
-to both export the same \verb|T|.)
-
-\subsection{The \textit{Name} of a value is used to avoid
-ambiguous identifier errors.}
-We state that two types
-are equal when their \I{Name}s are the same; however,
-for values, it is less clear why we care.  But consider this example:
-
-\begin{verbatim}
-    unit p (A) requires (H1, H2) where
-        signature H1(x) where
-            x :: Int
-        signature H2(x) where
-            import H1(x)
-        module A(y) where
-            import H1
-            import H2
-            y = x
-\end{verbatim}
-The reference to \verb|x| in \verb|A| is unambiguous, because it is known
-that \verb|x| from \verb|H1| and \verb|x| from \verb|H2| are the same (have
-the same \I{Name}.)  If they were not the same, it would be ambiguous and
-should cause an error.  Knowing the \I{Name} of a value distinguishes
-between these two cases.
-
-\subsection{Holes are linear}
-Requirements do not record what \I{Module} represents
-the identity of a requirement, which means that it's not possible to assert
-that hole \verb|A| and hole \verb|B| should be implemented with the same module,
-as might occur with aliasing:
-
-\begin{verbatim}
-    signature A where
-    signature B where
-    alias A = B
-\end{verbatim}
-%
-The benefit of this restriction is that when a requirement is filled,
-it is obvious that this is the only requirement that is filled: you won't
-magically cause some other requirements to be filled.  The downside is
-it's not possible to write a unit which looks for an interface it is
-looking for in one of $n$ names, accepting any name as an acceptable linkage.
-If aliasing was allowed, we'd need a separate physical shaping context,
-to make sure multiple mentions of the same hole were consistent.
-
-\subsection{A unit does not ``provide'' its signatures}
-We enforce the invariant that
-a provision is always (syntactically) a \verb|module| and a requirement
-is always a \verb|signature|.  This means that if you have a requirement
-and a provision of the same name, the requirement can \emph{always} be filled
-with the provision.
-
-The alternate design, where a unit both requires and provides
-its signatures, makes it unclear if a provision
-will actually fill a signature.  Consider this example, where
-a signature is required and exposed:
-
-\begin{verbatim}
-    unit a-sigs (A) requires (A) where -- ***
-        signature A where
-            data T
-
-    unit a-user (B) requires (A) where
-        signature A where
-            data T
-            x :: T
-        module B where
-            ...
-
-    unit p where
-        include a-sigs
-        include a-user
-\end{verbatim}
-%
-When we consider merging in the shape of \verb|a-user|, does the
-\verb|A| provided by \verb|a-sigs| fill in the \verb|A| requirement
-in \verb|a-user|?  It \emph{should not}, since \verb|a-sigs| does not
-actually provide enough declarations to satisfy \verb|a-user|'s
-requirement: the intended semantics \emph{merges} the requirements
-of \verb|a-sigs| and \verb|a-user|.
-
-What about this example?
-
-\begin{verbatim}
-    unit a-sigs (M as A) requires (H as A) where
-        signature H(T) where
-            data T
-        module M(T) where
-            import H(T)
-\end{verbatim}
-%
-We rightly should error, since the provision is a module. And in this situation:
-
-\begin{verbatim}
-    unit a-sigs (H as A) requires (H) where
-        signature H(T) where
-            data T
-\end{verbatim}
-%
-The requirements should be merged, but should the merged requirement
-be under the name \verb|H| or \verb|A|?
-
-It may still be possible to use the \verb|(A) requires (A)| syntax to
-indicate exposed signatures, but this would be a mere syntactic
-alternative to \verb|() requires (exposed A)|.
-
-\subsection{Signature visibility, and defaulting}
-The simplest formulation of requirements is to have them always be
-importable.  One proposed enhancement, however, is to allow some
-requirements to be ``non-importable''; that is, they are not visible
-to people who include packages.
-
-One simple way of modeling this is to associate each required module
-with a flag indicating whether or not it is importable or not.  Then, we
-might imagine that an explicit export list could be used to toggle
-whether or not a requirement is visible or not.
-
-However, when an export list is absent, we have to pick a default
-visibility for a signature.  If we use the same behavior as with
-modules, a strange situation can occur:
-
-\begin{verbatim}
-    unit p where -- S is visible
-        signature S where
-            x :: True
-
-    unit q where -- use defaulting
-        include p
-        signature S where
-            y :: True
-        module M where
-            import S
-            z = x && y      -- OK
-
-    unit r where
-        include q
-        module N where
-            import S
-            z = y           -- OK
-            z = x           -- ???
-\end{verbatim}
-%
-Absent the second signature declaration in \verb|q|, \verb|S.x| clearly
-should not be visible in \verb|N|.  However, what ought to occur when this signature
-declaration is added?  One interpretation is to say that only some
-(but not all) declarations are provided (\verb|S.x| remains invisible);
-another interpretation is that adding \verb|S| is enough to treat
-the signature as ``in-line'', and all declarations are now provided
-(\verb|S.x| is visible).
-
-The latter interpretation avoids having to keep track of providedness
-per declarations, and means that you can always express defaulting
-behavior by writing an explicit provides declaration on the unit.
-However, it has the odd behavior of making empty signatures semantically
-meaningful:
-
-\begin{verbatim}
-unit q where
-    include p
-    signature S where
-\end{verbatim}
-%
-%   SPJ: This would be too complicated (if there's yet a third way)
-
-This is pretty complicated, so signature visibility is not currently
-planned to be implemented.
-
-\subsection{Tricky \textit{AvailInfo} merging scenarios}
-
-\paragraph{Merging when type constructors are not in scope}
-
-\begin{verbatim}
-    signature A1(foo) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    signature A2(bar) where
-        data A = A { foo :: Int, bar :: Bool }
-\end{verbatim}
-%
-If we merge \verb|A1| and \verb|A2|, are we supposed to conclude that
-the types \verb|A1.A| and \verb|A2.A| (not in scope!) are the same?
-The answer is no!  Consider these implementations:
-
-\begin{verbatim}
-    module A1(A(..)) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    module A2(A(..)) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    module A(foo, bar) where
-        import A1(foo)
-        import A2(bar)
-\end{verbatim}
-
-Here, \verb|module A1| implements \verb|signature A1|, \verb|module A2| implements \verb|signature A2|,
-and \verb|module A| implements \verb|signature A1| and \verb|signature A2| individually
-and should certainly implement their merge.  This is why we cannot simply
-merge type constructors based on the \I{OccName} of their top-level type;
-merging only occurs between in-scope identifiers.
-
-\paragraph{Does merging a selector merge the type constructor?}
-
-\begin{verbatim}
-    signature A1(A(..)) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    signature A2(A(..)) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    signature A2(foo) where
-        import A1(foo)
-\end{verbatim}
-%
-Does the last signature, which is written in the style of a sharing constraint on \verb|foo|,
-also cause \verb|bar| and the type and constructor \verb|A| to be unified?
-Because a merge of a child name results in a substitution on the parent name,
-the answer is yes.
-
-\paragraph{Incomplete data declarations}
-
-\begin{verbatim}
-    signature A1(A(foo)) where
-        data A = A { foo :: Int }
-
-    signature A2(A(bar)) where
-        data A = A { bar :: Bool }
-\end{verbatim}
-%
-Should \verb|A1| and \verb|A2| merge?  If yes, this would imply
-that data definitions in signatures could only be \emph{partial}
-specifications of their true data types.  This seems complicated,
-which suggests this should not be supported; however, in fact,
-this sort of definition, while disallowed during type checking,
-should be \emph{allowed} during shaping. The reason that the
-shape we abscribe to the signatures \verb|A1| and \verb|A2| are
-equivalent to the shapes for these which should merge:
-
-\begin{verbatim}
-    signature A1(A(foo)) where
-        data A = A { foo :: Int, bar :: Bool }
-
-    signature A2(A(bar)) where
-        data A = A { foo :: Int, bar :: Bool }
-\end{verbatim}
-
-\subsection{Subtyping record selectors as functions}
-
-\begin{verbatim}
-    signature H(A, foo) where
-        data A
-        foo :: A -> Int
-
-    module M(A, foo) where
-        data A = A { foo :: Int, bar :: Bool }
-\end{verbatim}
-%
-Does \verb|M| successfully fill \verb|H|?  If so, it means that anywhere
-a signature requests a function \verb|foo|, we can instead validly
-provide a record selector.  This capability seems quite attractive,
-although in practice record selectors rarely seem to be abstracted this
-way: one reason is that \verb|M.foo| still \emph{is} a record selector,
-and can be used to modify a record.  (Many library authors find this
-surprising!)
-
-Nor does this seem to be an insurmountable instance of the avoidance
-problem:
-as a workaround, \verb|H| can equivalently be written as:
-
-\begin{verbatim}
-    signature H(foo) where
-        data A = A { foo :: Int, bar :: Bool }
-\end{verbatim}
-%
-However, you might not like this, as the otherwise irrelevant \verb|bar| must be mentioned
-in the definition.
-
-In any case, actually implementing this `subtyping' is quite complicated, because we can no
-longer assume that every child name is associated with a parent name.
-The technical difficulty is that we now need to unify a plain identifier
-\I{AvailInfo} (from the signature) with a type constructor \I{AvailInfo}
-(from a module.)  It is not clear what this should mean.
-Consider this situation:
-
-\begin{verbatim}
-    unit p where
-        signature H(A, foo, bar) where
-            data A
-            foo :: A -> Int
-            bar :: A -> Bool
-        module X(A, foo) where
-            import H
-    unit q where
-        include p
-        signature H(bar) where
-            data A = A { foo :: Int, bar :: Bool }
-        module Y where
-            import X(A(..)) -- ???
-\end{verbatim}
-
-Should the wildcard import on \verb|X| be allowed?
-This question is equivalent to whether or not shaping discovers
-whether or not a function is a record selector and propagates this
-information elsewhere.
-If the wildcard is not allowed, here is another situation:
-
-\begin{verbatim}
-    unit p where
-        -- define without record selectors
-        signature X1(A, foo) where
-            data A
-            foo :: A -> Int
-        module M1(A, foo) where
-            import X1
-
-    unit q where
-        -- define with record selectors (X1s unify)
-        signature X1(A(..)) where
-            data A = A { foo :: Int, bar :: Bool }
-        signature X2(A(..)) where
-            data A = A { foo :: Int, bar :: Bool }
-
-        -- export some record selectors
-        signature Y1(bar) where
-            import X1
-        signature Y2(bar) where
-            import X2
-
-    unit r where
-        include p
-        include q
-
-        -- sharing constraint
-        signature Y2(bar) where
-            import Y1(bar)
-
-        -- the payload
-        module Test where
-            import M1(foo)
-            import X2(foo)
-            ... foo ... -- conflict?
-\end{verbatim}
-
-Without the sharing constraint, the \verb|foo|s from \verb|M1| and \verb|X2|
-should conflict.  With it, however, we should conclude that the \verb|foo|s
-are the same, even though the \verb|foo| from \verb|M1| is \emph{not}
-considered a child of \verb|A|, and even though in the sharing constraint
-we \emph{only} unified \verb|bar| (and its parent \verb|A|).  To know that
-\verb|foo| from \verb|M1| should also be unified, we have to know a bit
-more about \verb|A| when the sharing constraint performs unification;
-however, the \I{AvailInfo} will only tell us about what is in-scope, which
-is \emph{not} enough information.
-
-\subsection{Some examples}
-
-\subsubsection{A simple example}
-
-In the following set of units:
-
-\begin{verbatim}
-    unit p(M) requires (A) where
-        signature A(T) where
-            data T
-        module M(T, S) where
-            import A(T)
-            data S = S T
-
-    unit q where
-        module A where
-            data T = T
-        include p
-\end{verbatim}
-
-When we \verb|include p|, we need to merge the partial shape
-of \verb|q| (with just provides \verb|A|) with the shape
-of \verb|p|.  Here is each step of the merging process:
-
-\begin{verbatim}
-          shape 1                       shape 2
-          --------------------------------------------------------------------------------
-(initial shapes)
-provides: A -> THIS:A { q():A.T }       M -> p(A -> hole:A) { hole:A.T, p(A -> hole:A).S }
-requires: (nothing)                     A ->                { hole:A.T }
-
-(after filling requirements)
-provides: A -> THIS:A { q():A.T }       M -> p(A -> THIS:A) { q():A.T, p(A -> THIS:A).S }
-requires: (nothing)                     (nothing)
-
-(after adding provides)
-provides: A -> THIS:A         { q():A.T }
-          M -> p(A -> THIS:A) { q():A.T, p(A -> THIS:A).S }
-requires: (nothing)
-\end{verbatim}
-
-Notice that we substituted \verb|hole:A| with \verb|THIS:A|, but \verb|hole:A.T| with \verb|q():A.T|.
-
-\subsubsection{Requirements merging can affect provisions}
-
-When a merge results in a substitution, we substitute over both
-requirements and provisions:
-
-\begin{verbatim}
-    signature H(T) where
-        data T
-    module A(T) where
-        import H(T)
-    module B(T) where
-        data T = T
-
-    -- provides: A -> THIS:A { hole:H.T }
-    --           B -> THIS:B { THIS:B.T }
-    -- requires: H ->        { hole:H.T }
-
-    signature H(T, f) where
-        import B(T)
-        f :: a -> a
-
-    -- provides: A -> THIS:A { THIS:B.T }           -- UPDATED
-    --           B -> THIS:B { THIS:B.T }
-    -- requires: H ->        { THIS:B.T, hole:H.f } -- UPDATED
-\end{verbatim}
-
-\subsubsection{Sharing constraints}
-
-Suppose you have two signature which both independently define a type,
-and you would like to assert that these two types are the same.  In the
-ML world, such a constraint is known as a sharing constraint.  Sharing
-constraints can be encoded in Backpacks via clever use of reexports;
-they are also an instructive example for signature merging.
-
-\begin{verbatim}
-    signature A(T) where
-        data T
-    signature B(T) where
-        data T
-
-    -- requires: A -> { hole:A.T }
-                 B -> { hole:B.T }
-
-    -- the sharing constraint!
-    signature A(T) where
-        import B(T)
-    -- (shape to merge)
-    -- requires: A -> { hole:B.T }
-
-    -- (after merge)
-    -- requires: A -> { hole:A.T }
-    --           B -> { hole:A.T }
-\end{verbatim}
-%
-\Red{I'm pretty sure any choice of \textit{Name} is OK, since the
-subsequent substitution will make it alpha-equivalent.}
-
-\subsection{Export declarations}
-
-If an explicit export declaration is given, the final shape is the
-computed shape, minus any provisions not mentioned in the list, with the
-appropriate renaming applied to provisions and requirements.  (Requirements
-are implicitly passed through if they are not named.)
-If no explicit export declaration is given, the final shape is
-the computed shape, including only provisions which were defined
-in the declarations of the unit.
-
-
-\section{Cabal}
-
-
-%  \I{InstalledUnitId} & ::= & \I{ComponentId} \verb|(| \, m \; \verb|->| \; \I{Module} \verb|,|\, \ldots\, \verb|)| & \mbox{Also known as \I{UnitId}} \\
-%  \I{Module} & ::= & \I{InstalledUnitId} \verb|:| m \\
-
-\paragraph{Indefinite versus installed units}
-The purpose of an \I{ComponentId} is to uniquely identify the results of \textbf{typechecking}
-an indefinite unit; whereas an \I{InstalledUnitId} uniquely identifies
-the results of \textbf{compiling} a unit with all its holes
-filled.  Thus, an \I{InstalledUnitId} also records a \emph{hole mapping}
-which specifies how each hole was filled.  If an \I{InstalledUnitId}
-is only partially filled, we may refer to it as a \I{UnitId} (as these
-are never installed.)
-
-\paragraph{Units versus packages}
-
-Cabal packages are:
-
-\begin{itemize}
-    \item The unit of distribution
-    \item The unit that Hackage handles
-    \item The unit of versioning
-    \item The unit of ownership (who maintains it etc) 
-\end{itemize}
-
-Backpack units are the building blocks of modular development;
-there may be multiple units per a Cabal package.  While in theory
-Cabal could do sophisticated things with multiple units in a
-package, we expect Cabal
-to pick a distinguished unit (with the same unit name $p$ as
-the package) which serves as the publically visible unit.
-
-
-%\newpage
-
-\end{document} % chktex 16
diff --git a/docs/backpack/arch.png b/docs/backpack/arch.png
deleted file mode 100644
index d8b8fd21f9..0000000000
--- a/docs/backpack/arch.png
+++ /dev/null
diff --git a/docs/backpack/backpack-impl.bib b/docs/backpack/backpack-impl.bib
deleted file mode 100644
index 6bda35a8ea..0000000000
--- a/docs/backpack/backpack-impl.bib
+++ /dev/null
@@ -1,17 +0,0 @@
-@inproceedings{Kilpatrick:2014:BRH:2535838.2535884,
- author = {Kilpatrick, Scott and Dreyer, Derek and Peyton Jones, Simon and Marlow, Simon},
- title = {Backpack: Retrofitting Haskell with Interfaces},
- booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
- series = {POPL '14},
- year = {2014},
- isbn = {978-1-4503-2544-8},
- location = {San Diego, California, USA},
- pages = {19--31},
- numpages = {13},
- url = {http://doi.acm.org/10.1145/2535838.2535884},
- doi = {10.1145/2535838.2535884},
- acmid = {2535884},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {applicative instantiation, haskell modules, mixin modules, module systems, packages, recursive modules, separate modular development, type systems},
-} 
diff --git a/docs/backpack/backpack-impl.tex b/docs/backpack/backpack-impl.tex
deleted file mode 100644
index 10f199bac4..0000000000
--- a/docs/backpack/backpack-impl.tex
+++ /dev/null
@@ -1,2519 +0,0 @@
-\documentclass{article}
-
-\usepackage{pifont}
-\usepackage{graphicx} %[pdftex] OR [dvips]
-\usepackage{fullpage}
-\usepackage{wrapfig}
-\usepackage{float}
-\usepackage{titling}
-\usepackage{hyperref}
-\usepackage{tikz}
-\usepackage{color}
-\usepackage{footnote}
-\usepackage{float}
-\usepackage{algorithm}
-\usepackage{algpseudocode}
-\usetikzlibrary{arrows}
-\usetikzlibrary{positioning}
-\setlength{\droptitle}{-6em}
-
-\input{commands-new-new.tex}
-
-\newcommand{\nuAA}{\nu_\mathit{AA}}
-\newcommand{\nuAB}{\nu_\mathit{AB}}
-\newcommand{\nuGA}{\nu_\mathit{GA}}
-\newcommand{\nuGB}{\nu_\mathit{GB}}
-\newcommand{\betaPL}{\beta_\mathit{PL}}
-\newcommand{\betaAA}{\beta_\mathit{AA}}
-\newcommand{\betaAS}{\beta_\mathit{AS}}
-\newcommand{\thinandalso}{\hspace{.45cm}}
-\newcommand{\thinnerandalso}{\hspace{.38cm}}
-
-\input{commands-rebindings.tex}
-
-\newcommand{\var}[1]{\textsf{#1}}
-
-\newcommand{\ghcfile}[1]{\textsl{#1}}
-
-\title{Implementing Backpack}
-
-\begin{document}
-
-\maketitle
-
-The purpose of this document is to describe an implementation path
-for Backpack in GHC\@.
-
-\tableofcontents
-
-\section{What we are trying to solve}
-
-While the current ecosystem has proved itself serviceable for many years,
-there are a number of major problems which causes significant headaches
-for many users.  Here are some of them:
-
-\subsection{Package reinstalls are destructive}\label{sec:destructive}
-
-When attempting to install a new package, you might get an error like
-this:
-
-\begin{verbatim}
-$ cabal install hakyll
-cabal: The following packages are likely to be broken by the reinstalls:
-pandoc-1.9.4.5
-Graphalyze-0.14.0.0
-Use --force-reinstalls if you want to install anyway.
-\end{verbatim}
-
-While this error message is understandable if you're really trying to
-reinstall a package, it is quite surprising that it can occur even if
-you didn't ask for any reinstalls!
-
-The underlying cause of this problem is related to an invariant Cabal
-currently enforces on a package database: there can only be one instance
-of a package for any given package name and version.  This means that it
-is not possible to install a package multiple times, compiled against
-different dependencies.  However, sometimes, reinstalling a package with
-different dependencies is the only way to fulfill version bounds of a
-package!  For example: say we have three packages \pname{a}, \pname{b}
-and \pname{c}.  \pname{b-1.0} is the only version of \pname{b}
-available, and it has been installed and compiled against \pname{c-1.0}.
-Later, the user installs an updated version \pname{c-1.1} and then
-attempts to install \pname{a}, which depends on the specific versions
-\pname{c-1.1} and \pname{b-1.0}.  We \emph{cannot} use the already
-installed version of \pname{b-1.0}, which depends on the wrong version
-of \pname{c}, so our only choice is to reinstall \pname{b-1.0} compiled
-against \pname{c-1.1}.  This will break any packages, e.g. \pname{d},
-which were built against the old version of \pname{b-1.0}.
-
-Our solution to this problem is to \emph{abolish} destructive package
-installs, and allow a package to be installed multiple times with the same
-package name and version.  However, allowing this poses some interesting
-user interface problems, since package IDs are now no longer unambiguous
-identifiers.
-
-\subsection{Version bounds are often over/under-constrained}
-
-When attempting to install a new package, Cabal might fail in this way:
-
-\begin{verbatim}
-$ cabal install hledger-0.18
-Resolving dependencies...
-cabal: Could not resolve dependencies:
-# pile of output
-\end{verbatim}
-
-There are a number of possible reasons why this could occur, but usually
-it's because some of the packages involved have over-constrained version
-bounds, which are resulting in an unsatisfiable set of constraints (or,
-at least, Cabal gave up backtracking before it found a solution.)  To
-add insult to injury, most of the time the bound is nonsense and removing
-it would result in a working compilation.  In fact, this situation is
-so common that Cabal has a flag \verb|--allow-newer| which lets you
-override the package upper bounds.
-
-However, the flip-side is when Cabal finds a satisfying set, but your
-compilation fails with a type error.  Here, you had an under-constrained
-set of version bounds which didn't actually reflect the compatible
-versions of a package, and Cabal picked a version of the package which
-was incompatible.
-
-Our solution to this problem is to use signatures instead of version
-numbers as the primary mechanism by which compatibility is determined:
-e.g., if it typechecks, it's a valid choice.  Version numbers can still
-be used to reflect semantic changes not seen in the types (in
-particular, ruling out buggy versions of a package is a useful
-operation), but these bounds are empirical observations and can be
-collected after-the-fact.
-
-\subsection{It is difficult to support multiple implementations of a type}
-
-This problem is perhaps best described by referring to a particular
-instance of it Haskell's ecosystem: the \texttt{String} data type.  Haskell,
-by default, implements strings as linked lists of integers (representing
-characters).  Many libraries use \texttt{String}, because it's very
-convenient to program against.  However, this representation is also
-very \emph{slow}, so there are alternative implementations such as
-\texttt{Text} which implement efficient, UTF-8 encoded packed byte
-arrays.
-
-Now, suppose you are writing a library and you don't care if the user of
-your library is using \texttt{String} or \texttt{Text}.  However, you
-don't want to rewrite your library twice to support both data types:
-rather, you'd like to rely on some \emph{common interface} between the
-two types, and let the user instantiate the implementation.  The only
-way to do this in today's Haskell is using type classes; however, this
-necessitates rewriting all type signatures from a nice \texttt{String ->
-String} to \texttt{StringLike s => s -> s}.  The result is less readable,
-required a large number of trivial edits to type signatures, and might
-even be less efficient, if GHC does not appropriately specialize your code
-written in this style.
-
-Our solution to this problem is to introduce a new mechanism of
-pluggability: module holes, which let us use types and functions from a
-module \texttt{Data.String} as before, but defer choosing \emph{what}
-module should be used in the implementation to some later point (or
-instantiate the code multiple times with different choices.)
-
-\subsection{Fast moving APIs are difficult to develop/develop against}
-
-Most packages that are uploaded to Hackage have package authors which pay
-some amount of attention to backwards compatibility and avoid making egregious
-breaking changes.  However, a package like the \verb|ghc-api| follows a
-very different model: the library is a treated by its developers as an
-internal component of an application (GHC), and is frequently refactored
-in a way that changes its outwards facing interface.
-
-Arguably, an application like GHC should design a stable API and
-maintain backwards compatibility against it.  However, this is a lot of
-work (including refactoring) which is only being done slowly, and in the
-meantime, the dump of all the modules gives users the functionality they
-want (even if it keeps breaking every version.)
-
-One could say that the core problem is there is no way for users to
-easily communicate to GHC authors what parts of the API they rely on.  A
-developer of GHC who is refactoring an interface will often rely on the
-typechecker to let them know which parts of the codebase they need to
-follow and update, and often could say precisely how to update code to
-use the new interface.  User applications, which live out of tree, don't
-receive this level of attention.
-
-Our solution is to make it possible to typecheck the GHC API against a
-signature.  Important consumers can publish what subsets of the GHC API
-they rely against, and developers of GHC, as part of their normal build
-process, type-check against these signatures.  If the signature breaks,
-a developer can either do the refactoring differently to avoid the
-compatibility-break, or document how to update code to use the new API\@.
-
-\section{Backpack in a nutshell}
-
-For a more in-depth tutorial about Backpack's features, check out Section 2
-of the original Backpack paper.  In this section, we briefly review the
-most important points of Backpack's design.
-
-\paragraph{Thinning and renaming at the module level}
-A user can specify a build dependency which only exposes a subset of
-modules (possibly under different names.)  By itself, it's a way for the
-user to resolve ambiguous module imports at the package level, without
-having to use the \texttt{PackageImports} syntax extension.
-
-\paragraph{Holes (abstract module definitions)}  The core
-component of Backpack's support for \emph{separate modular development}
-is the ability to specify abstract module bindings, or holes, which give
-users of the module an obligation to provide an implementation which
-fulfills the signature of the hole.  In this example:
-
-\begin{verbatim}
-package p where
-    A :: [ ... ]
-    B = [ import A; ... ]
-\end{verbatim}
-
-\verb|p| is an \emph{indefinite package}, which cannot be compiled until
-an implementation of \m{A} is provided.  However, we can still type check
-\m{B} without any implementation of \m{A}, by type checking it against
-the signature.  Holes can be put into signature packages and included
-(depended upon) by other packages to reuse definitions of signatures.
-
-\paragraph{Filling in holes with an implementation}
-A hole in an indefinite package can be instantiated in a \emph{mix-in}
-style: namely, if a signature and an implementation have the same name,
-they are linked together:
-
-\begin{verbatim}
-package q where
-    A = [ ... ]
-    include p -- has signature A
-\end{verbatim}
-
-Renaming is often useful to rename a module (or a hole) so that a signature
-and implementation have the same name and are linked together.
-An indefinite package can be instantiated multiple times with different
-implementations: the \emph{applicativity} of Backpack means that if
-a package is instantiated separately with the same module, the results
-are type equal:
-
-\begin{verbatim}
-package q' where
-    A = [ ... ]
-    include p (A, B as B1)
-    include p (A, B as B2)
-    -- B1 and B2 are equivalent
-\end{verbatim}
-
-\paragraph{Combining signatures together}
-Unlike implementations, it's valid for a multiple signatures with the
-same name to be in scope.
-
-\begin{verbatim}
-package a-sig where
-    A :: [ ... ]
-package a-sig2 where
-    A :: [ ... ]
-package q where
-    include a-sig
-    include a-sig2
-    B = [ import A; ... ]
-\end{verbatim}
-
-These signatures \emph{merge} together, providing the union of the
-functionality (assuming the types of individual entities are
-compatible.)  Backpack has a very simple merging algorithm: types must
-match exactly to be compatible (\emph{width} subtyping).
-
-\clearpage
-
-\section{Module and package identity}
-
-\begin{figure}[H]
-\begin{tabular}{p{0.45\textwidth} p{0.45\textwidth}}
-\begin{verbatim}
-package p where
-    A :: [ data X ]
-    P = [ import A; data Y = Y X ]
-package q where
-    A1 = [ data X = X1 ]
-    A2 = [ data X = X2 ]
-    include p (A as A1, P as P1)
-    include p (A as A2, P as P2)
-\end{verbatim}
-&
-\begin{verbatim}
-package p where
-    A :: [ data X ]
-    P = [ data T = T ] -- no A import!
-package q where
-    A1 = [ data X = X1 ]
-    A2 = [ data X = X2 ]
-    include p (A as A1, P as P1)
-    include p (A as A2, P as P2)
-\end{verbatim}
-\\
-(a) Type equality must consider holes\ldots &
-(b) \ldots but how do we track dependencies? \\
-\end{tabular}
-\caption{Two similar examples}\label{fig:simple-ex}
-\end{figure}
-
-One of the central questions one encounters when type checking Haskell
-code is: \emph{when are two types equal}?  In ordinary Haskell, the
-answer is simple: ``They are equal if their \emph{original names} (i.e.,
-where they were originally defined) are the same.''  However, in
-Backpack, the situation is murkier due to the presence of \emph{holes}.
-Consider the pair of examples in Figure~\ref{fig:simple-ex}.
-In Figure~\ref{fig:simple-ex}a,  the types \m{B1}.\verb|Y| and \m{B2}.\verb|Y| should not be
-considered equal, even though na\"\i vely their original names are
-\pname{p}:\m{B}.\verb|Y|, since their arguments are different \verb|X|'s!
-On the other hand, if we instantiated \pname{p} twice with the same \m{A}
-(e.g., change the second include to \texttt{include p (A as A1, P as P2)}),
-we might consider the two resulting \verb|Y|'s
-equal, an \emph{applicative} semantics of identity instantiation.  In
-Figure~\ref{fig:simple-ex}b, we see that even though \m{A} was instantiated differently,
-we might reasonably wonder if \texttt{T} should still be considered the same,
-since it has no dependence on the actual choice of \m{A}.
-
-In fact, there are quite a few different choices that can be made here.
-Figures~\ref{fig:applicativity}~and~\ref{fig:granularity} summarize the various
-choices on two axes: the granularity of applicativity (under what circumstances
-do we consider two types equal) and the granularity of dependency (what circumstances
-do we consider two types not equal)?  A \ding{52} means the design we have chosen
-answers the question affirmatively---\ding{54}, negatively---but all of these choices
-are valid points on the design space.
-
-\subsection{The granularity of applicativity}
-
-An applicative semantics of package instantiation states that if a package is
-instantiated with the ``same arguments'', then the resulting entities it defines
-should also be considered equal.  Because Backpack uses \emph{mix-in modules},
-it is very natural to consider the arguments of a package instantiation as the
-modules, as shown in Figure~\ref{fig:applicativity}b: the same module \m{A} is
-linked for both instantiations, so \m{P1} and \m{P2} are considered equal.
-
-However, we consider the situation at a finer granularity, we might say, ``Well,
-for a declaration \texttt{data Y = Y X}, only the definition of type \verb|X| matters.
-If they are the same, then \verb|Y| is the same.''  In that case, we might accept
-that in Figure~\ref{fig:applicativity}a, even though \pname{p} is instantiated
-with different modules, at the end of the day, the important component \verb|X| is
-the same in both cases, so \verb|Y| should also be the same.  This is a sort of
-``extreme'' view of modular development, where every declaration is desugared
-into a separate module.  In our design, we will be a bit more conservative, and
-continue with module level applicativity, in the same manner as Paper Backpack.
-
-\paragraph{Implementation considerations}
-Compiling Figure~\ref{fig:applicativity}b to dynamic libraries poses an
-interesting challenge, if every package compiles to a dynamic library.
-When we compile package \pname{q}, the libraries we end up producing are \pname{q}
-and an instance of \pname{p} (instantiated with \pname{q}:\m{A}).  Furthermore,
-\pname{q} refers to code in \pname{p} (the import in \m{Q}), and vice versa (the usage
-of the instantiated hole \m{A}).  When building static libraries, this circular
-dependency doesn't matter: when we link the executable, we can resolve all
-of the symbols in one go.  However, when the libraries in question are
-dynamic libraries \verb|libHSq.so| and \verb|libHSp(q:A).so|, we now have
-a \emph{circular dependency} between the two dynamic libraries, and most dynamic
-linkers will not be able to load either of these libraries.
-
-To break the circularity in Figure~\ref{fig:applicativity}b, we have to \emph{inline}
-the entire module \m{A} into the instance of \pname{p}.  Since the code is exactly
-the same, we can still consider the instance of \m{A} in \pname{q} and in \pname{p}
-type equal.  However, in Figure~\ref{fig:applicativity}c, applicativity has been
-done at a coarser level: although we are using Backpack's module mixin syntax,
-morally, this example is filling in the holes with the \emph{package} \pname{a}
-(rather than a module).  In this case, we can achieve code sharing, since
-\pname{p} can refer directly to \pname{a}, breaking the circularity.
-
-\newcolumntype{C}{>{\centering\arraybackslash}p{0.3\textwidth}}
-    \begin{savenotes}
-\begin{figure}
-    \begin{tabular}{C C C}
-\begin{verbatim}
-package q where
-  A = [ data X = X ]
-  A1 = [ import A; x = 0 ]
-  A2 = [ import A; x = 1 ]
-  include p (A as A1, P as P1)
-  include p (A as A2, P as P2)
-  Q = [ import P1; ... ]
-\end{verbatim}
-&
-\begin{verbatim}
-package q where
-  A = [ data X = X ]
-
-
-  include p (A, P as P1)
-  include p (A, P as P2)
-  Q = [ import P1; ... ]
-\end{verbatim}
-&
-\begin{verbatim}
-package a where
-  A = [ data X = X ]
-package q where
-  include a
-  include p (A, P as P1)
-  include p (A, P as P2)
-  Q = [ import P1; ... ]
-\end{verbatim}
-  \\
-  (a) Declaration applicativity \ding{54} &
-  (b) Module applicativity \ding{52} &
-  (c) Package applicativity \ding{52} \\
-\end{tabular}
-\caption{Choices of granularity of applicativity on \pname{p}: given \texttt{data Y = Y X},  is \m{P1}.\texttt{Y} equal to \m{P2}.\texttt{Y}?}\label{fig:applicativity}
-\end{figure}
-\end{savenotes}
-
-\subsection{The granularity of dependency}
-
-\begin{savenotes}
-\newcolumntype{C}{>{\centering\arraybackslash}p{0.3\textwidth}}
-\begin{figure}
-    \begin{tabular}{C C C}
-\begin{verbatim}
-package p(A,P) where
-  A :: [ data X ]
-  P = [
-    import A
-    data T = T
-    data Y = Y X
-  ]
-\end{verbatim}
-&
-\begin{verbatim}
-package p(A,P) where
-  A :: [ data X ]
-  B = [ data T = T ]
-  C = [
-    import A
-    data Y = Y X
-  ]
-  P = [
-    import B
-    import C
-  ]
-\end{verbatim}
-&
-\begin{verbatim}
-package b where
-  B = [ data T = T ]
-package c where
-  A :: [ data X ]
-  C = [
-    import A
-    data Y = Y X
-  ]
-package p(A,P) where
-  include b; include c
-  P = [ import B; import C ]
-\end{verbatim}
-  \\
-  (a) Declaration granularity \ding{54} &
-  (b) Module granularity \ding{54} &
-  (c) Package granularity \ding{52} \\
-\end{tabular}
-\caption{Choices of granularity for dependency: is the identity of \texttt{T} independent of how \m{A} is instantiated?}\label{fig:granularity}
-\end{figure}
-
-\end{savenotes}
-
-In the previous section, we considered \emph{what} entities may be considered for
-computing dependency; in this section we consider \emph{which} entities are actually
-considered as part of the dependencies for the declaration/module/package we're writing.
-Figure~\ref{fig:granularity} contains a series of examples which exemplify the choice
-of whether or not to collect dependencies on a per-declaration, per-module or per-package basis:
-
-\begin{itemize}
-    \item Package-level granularity states that the modules in a package are
-considered to depend on \emph{all} of the holes in the package, even if
-the hole is never imported.  Figure~\ref{fig:granularity}c is factored so that
-\verb|T| is defined in a distinct package \pname{b} with no holes, so no matter
-the choice of \m{A}, \m{B}.\verb|T| will be the same.  On the other hand, in
-Figure~\ref{fig:granularity}b, there is a hole in the package defining \m{B},
-so the identity of \verb|T| will depend on the choice of \m{A}.
-
-\item Module-level granularity states that each module has its own dependency,
-computed by looking at its import statements.  In this setting, \verb|T| in Figure~\ref{fig:granularity}b
-is independent of \m{A}, since the hole is never imported in \m{B}.  But once again, in
-Figure~\ref{fig:granularity}a, there is an import in the module defining \verb|T|,
-so the identity of \verb|T| once again depends on the choice of \m{A}.
-
-\item Finally, at the finest level of granularity, one could chop up \pname{p} in
-Figure~\ref{fig:granularity}a, looking at the type declaration-level dependency
-to suss out whether or not \verb|T| depends on \m{A}.  It doesn't refer to
-anything in \m{A}, so it is always considered the same.
-\end{itemize}
-
-It is well worth noting that the system described by Paper Backpack tracks dependencies per module;
-however, we have decided that we will implement tracking per package instead:
-a coarser grained granularity which accepts less programs.
-
-Is a finer form of granularity \emph{better?} Not necessarily!  For
-one, we can always split packages into further subpackages (as was done
-in Figure~\ref{fig:granularity}c) which better reflect the internal hole
-dependencies, so it is always possible to rewrite a program to make it
-typecheck---just with more packages.  Additionally, the finer the
-granularity of dependency, the more work I have to do to understand what
-the identities of entities in a module are.  In Paper Backpack, I have
-to understand the imports of all modules in a package; with
-declaration-granularity, I have to understand the entire code.  This is
-a lot of work for the developer to think about; a more granular model is
-easier to remember and reason about.  Finally, package-level granularity
-is much easier to implement, as it preserves the previous compilation
-model, \emph{one library per package}.  At a fine level of granularity, we
-may end up repeatedly compiling a module which actually should be considered
-``the same'' as any other instance of it.
-
-Nevertheless, finer granularity can be desirable from an end-user perspective.
-Usually, these circumstances arise when library-writers are forced to split their
-components into many separate packages, when they would much rather have written
-a single package.  For example, if I define a data type in my library, and would
-like to define a \verb|Lens| instance for it, I would create a new package just
-for the instance, in order to avoid saddling users who aren't interested in lenses
-with an extra dependency.  Another example is test suites, which have dependencies
-on various test frameworks that a user won't care about if they are not planning
-on testing the code. (Cabal has a special case for this, allowing the user
-to write effectively multiple packages in a single Cabal file.)
-
-\subsection{Summary}
-
-We can summarize all of the various schemes by describing the internal data
-types that would be defined by GHC under each regime.  First, we have
-the shared data structures, which correspond closely to what users are
-used to seeing:
-
-\begin{verbatim}
-<pkg-name>   ::= containers, ...
-<pkg-version ::= 1.0, ...
-<pkg-id>     ::= <pkg-name>-<pkg-version>
-<mod-name>   ::= Data.Set, ...
-<occ>        ::= empty, ...
-\end{verbatim}
-
-Changing the \textbf{granularity of applicativity} modifies how we represent the
-list of dependencies associated with an entity.  With module applicativity,
-we list module identities (not yet defined); with declaration applicativity
-we actually list the original names (i.e., ids).
-
-\begin{verbatim}
-<deps>       ::= <id>, ...      # Declaration applicativity
-<deps>       ::= <module>, ...  # Module applicativity
-\end{verbatim}
-
-Changing the \textbf{granularity of dependency} affects how we compute
-the lists of dependencies, and what entities are well defined:
-
-\begin{verbatim}
-# Package-level granularity
-<pkg-key>    ::= hash(<pkg-id> + <deps for pkg>)
-<module>     ::= <pkg-key> : <mod-name>
-<id>         ::= <module> . <occ>
-
-# Module-level granularity
-<pkg-key>    not defined
-<module>     ::= hash(<pkg-id> : <mod-name> + <deps for mod>)
-<id>         ::= <module-key> . <occ>
-
-# Declaration-level granularity
-<pkg-key>    not defined
-<module>     not defined
-<id>         ::= hash(<pkg-id> : <mod-name> . <occ> + <deps for decl>)
-\end{verbatim}
-
-Notice that as we increase the granularity, the notion of a ``package'' and a ``module''
-become undefined.  This is because, for example, with module-level granularity, a single
-``package'' may result in several modules, each of which have different sets of
-dependencies.  It doesn't make much sense to refer to the package as a monolithic entity,
-because the point of splitting up the dependencies was so that if a user relies only
-on a single module, it has a correspondingly restricted set of dependencies.
-\subsection{The new scheme, formally}
-
-\begin{wrapfigure}{R}{0.5\textwidth}
-\begin{myfig}
-\[
-\begin{array}{@{}lr@{\;}c@{\;}l@{}}
-    \text{Package Names (\texttt{PkgName})} & P &\in& \mathit{PkgNames} \\
-    \text{Module Path Names (\texttt{ModName})} & p &\in& \mathit{ModPaths} \\
-    \text{Module Identity Vars} & \alpha,\beta &\in& \mathit{IdentVars} \\
-    \text{Package Key (\texttt{PackageKey})} & \K &::=& P(\vec{p\mapsto\nu}) \\
-    \text{Module Identities (\texttt{Module})} & \nu &::=&
-      \alpha ~|~
-      \K\colon\! p \\
-    \text{Module Identity Substs} & \phi,\theta &::=&
-      \{\vec{\alpha \coloneqq \nu}\} \\
-\end{array}
-\]
-\caption{Module Identities}
-\label{fig:mod-idents}
-\end{myfig}
-\end{wrapfigure}
-
-In this section, we give a formal treatment of our choice in the design space, in the
-same style as the Backpack paper, but omitting mutual recursion, as it follows straightforwardly.
-Physical module
-identities $\nu$, the \texttt{Module} component of \emph{original names} in GHC, are either (1) \emph{variables} $\alpha$, which are
-used to represent holes\footnote{In practice, these will just be fresh paths in a special package key for variables.} or (2) a concrete module $p$ defined in package
-$P$, with holes instantiated with other module identities (might be
-empty)\footnote{In Paper Backpack, we would refer to just $P$:$p$ as the identity
-constructor.  However, we've written the subterms specifically next to $P$ to highlight the semantic difference of these terms.}.
-
-As in traditional Haskell, every package contains a number of module
-files at some module path $p$; within a package these paths are
-guaranteed to be unique.\footnote{In Paper Backpack, the module expressions themselves are used to refer to globally unique identifiers for each literal.  This makes the metatheory simpler, but for implementation purposes it is convenient to conflate the \emph{original} module path that a module is defined at with its physical identity.}  When we write inline module definitions, we assume
-that they are immediately assigned to a module path $p$ which is incorporated
-into their identity.  A module identity $\nu$ simply augments this
-with subterms $\vec{p\mapsto\nu}$ representing how \emph{all} holes in the package $P$
-were instantiated.\footnote{In Paper Backpack, we do not distinguish between holes/non-holes, and we consider all imports of the \emph{module}, not the package.}  This naming is stable because the current Backpack surface syntax does not allow a logical path in a package
-to be undefined.  A package key is $P(\vec{p\mapsto\nu})$.
-
-Here is the very first example from
-Section 2 of the original Backpack paper, \pname{ab-1}:
-
-\begin{example}
-\Pdef{ab-1}{
-    \Pmod{A}{x = True}
-    \Pmod{B}{\Mimp{A}; y = not x}
-    % \Pmodd{C}{\mname{A}}
-}
-\end{example}
-
-The identities of \m{A} and \m{B} are
-\pname{ab-1}:\mname{A} and \pname{ab-1}:\mname{B}, respectively.\footnote{In Paper Backpack, the identity for \mname{B} records its import of \mname{A}, but since it is definite, this is strictly redundant.} In a package with holes, each
-hole (within the package definition) gets a fresh variable as its
-identity, and all of the holes associated with package $P$ are recorded. Consider \pname{abcd-holes-1}:
-
-\begin{example}
-\Pdef{abcd-holes-1}{
-    \Psig{A}{x :: Bool} % chktex 26
-    \Psig{B}{y :: Bool} % chktex 26
-    \Pmod{C}{x = False}
-    \Pmodbig{D}{
-        \Mimpq{A}\\
-        \Mimpq{C}\\
-        % \Mexp{\m{A}.x, z}\\
-        z = \m{A}.x \&\& \m{C}.x
-    }
-}
-\end{example}
-
-The identities of the four modules
-are, in order, $\alpha_a$, $\alpha_b$, $\pname{abcd-holes-1}(\alpha_a,\alpha_b)$:\mname{C}, and
-$\pname{abcd-holes-1}(\alpha_a,\alpha_b)$:\mname{D}.\footnote{In Paper Backpack, the granularity is at the module level, so the subterms of \mname{C} and \mname{D} can differ.}  We include both $\alpha_a$ and $\alpha_b$ in both \mname{C} and \mname{D}, regardless of the imports.  When we link the package against an implementation of the hole, these variables are replaced with the identities of the modules we linked against.
-
-Shaping proceeds in the same way as in Paper Backpack, except that the
-shaping judgment must also accept the package key
-$P(\vec{p\mapsto\alpha})$ so we can create identifiers with
-\textsf{mkident}.  This implies we must know ahead of time what the holes
-of a package are.
-
-\paragraph{A full Backpack comparison}
-If you're curious about how the rest of the Backpack examples translate,
-look no further than this section.
-
-First, consider the module identities in the \m{Graph} instantiations in
-\pname{multinst}, shown in Figure 2 of the original Backpack paper.
-In the definition of \pname{structures}, assume that the variables for
-\m{Prelude} and \m{Array} are $\alpha_P$ and $\alpha_A$ respectively.
-The identity of \m{Graph} is $\pname{structures}(\alpha_P, \alpha_A)$:\m{Graph}. Similarly, the identities of the two array implementations
-are $\nu_{AA} = \pname{arrays-a}(\alpha_P)$:\m{Array} and
-$\nu_{AB} = \pname{arrays-b}(\alpha_P)$:\m{Array}.\footnote{Notice that the subterms coincide with Paper Backpack!  A sign that module level granularity is not necessary for many use-cases.}
-
-The package \pname{graph-a} is more interesting because it
-\emph{links} the packages \pname{arrays-a} and \pname{structures}
-together, with the implementation of \m{Array} from \pname{arrays-a}
-\emph{instantiating} the hole \m{Array} from \pname{structures}.  This
-linking is reflected in the identity of the \m{Graph} module in
-\pname{graph-a}: whereas in \pname{structures} it was $\nu_G =
-\pname{structures}(\alpha_P, \alpha_A)$:\m{Graph}, in \pname{graph-a} it is
-$\nu_{GA} = \nu_G[\nu_{AA}/\alpha_A] = \pname{structures}(\alpha_P, \nu_{AA})$:\m{Graph}.  Similarly, the identity of \m{Graph} in
-\pname{graph-b} is $\nu_{GB} = \nu_G[\nu_{AB}/\alpha_A] =
-\pname{structures}(\alpha_P, \nu_{AB})$:\m{Graph}.  Thus, linking consists
-of substituting the variable identity of a hole by the concrete
-identity of the module filling that hole.
-
-Lastly, \pname{multinst} makes use of both of these \m{Graph}
-modules, under the aliases \m{GA} and \m{GB}, respectively.
-Consequently, in the \m{Client} module, \code{\m{GA}.G} and
-\code{\m{GB}.G} will be correctly viewed as distinct types since they
-originate in modules with distinct identities.
-
-As \pname{multinst} illustrates, module identities effectively encode
-dependency graphs at the package level.\footnote{In Paper Backpack, module identities
-encode dependency graphs at the module level.  In both cases, however, what is being
-depended on is always a module.}  Like in Paper Backpack, we have an \emph{applicative}
-semantics of instantiation, and the applicativity example in Figure 3 of the
-Backpack paper still type checks.  However, because we are operating at a coarser
-granularity, modules may have spurious dependencies on holes that they don't
-actually depend on, which means less type equalities may hold.
-
-
-\subsection{Cabal dependency resolution}
-
-Currently, when we compile a Cabal
-package, Cabal goes ahead and resolves \verb|build-depends| entries with actual
-implementations, which we compile against.  The package key,
-independently of Backpack, records the transitive dependency tree selected
-during this dependency resolution process, so that we can install \pname{libfoo-1.0}
-twice compiled against different versions of its dependencies.
-What is the relationship to this transitive dependency tree of \emph{packages},
-with the subterms of our package identities which are \emph{modules}?  Does one
-subsume the other?  In fact, these are separate mechanisms---two levels of indirections,
-so to speak.
-
-To illustrate, suppose I write a Cabal file with \verb|build-depends: foobar|.  A reasonable assumption is that this translates into a
-Backpack package which has \verb|include foobar|.  However, this is not
-actually a Paper Backpack package: Cabal's dependency solver has to
-rewrite all of these package references into versioned references
-\verb|include foobar-0.1|.  For example, this is a pre-package:
-
-\begin{verbatim}
-package foo where
-    include bar
-\end{verbatim}
-
-and this is a Paper Backpack package:
-
-\begin{verbatim}
-package foo-0.3[bar-0.1[baz-0.2]] where
-    include bar-0.1[baz-0.2]
-\end{verbatim}
-
-This tree is very similar to the one tracking dependencies for holes,
-but we must record this tree \emph{even} when our package has no holes.
-%   As a final example, the full module
-%   identity of \m{B1} in Figure~\ref{fig:granularity} may actually be $\pname{p-0.9(q-1.0[p-0.9]:A1)}$:\m{B}.
-
-\paragraph{Linker symbols} As we increase the amount of information in
-PackageId, it's important to be careful about the length of these IDs,
-as they are used for exported linker symbols (e.g.
-\verb|base_TextziReadziLex_zdwvalDig_info|).  Very long symbol names
-hurt compile and link time, object file sizes, GHCi startup time,
-dynamic linking, and make gdb hard to use.
-As such, we've done away with full package names and versions; instead,
-there is simply a base-62 encoded hash, with the first five characters of the package
-name for user-friendliness.
-
-\subsection{Package selection}
-
-When I fire up \texttt{ghci} with no arguments, GHC somehow creates
-out of thin air some consistent set of packages, whose modules I can
-load using \texttt{:m}.  This functionality is extremely handy for
-exploratory work, but actually GHC has to work quite hard in order
-to generate this set of packages, the contents of which are all
-dumped into a global namespace.  For example, GHC doesn't have access
-to Cabal's dependency solver, nor does it know \emph{which} packages
-the user is going to ask for, so it can't just run a constraint solver,
-get a set of consistent packages to offer and provide them to the user.\footnote{Some might
-argue that depending on a global environment in this fashion is wrong, because
-when you perform a build in this way, you have absolutely no ideas what
-dependencies you actually ended up using.  But the fact remains that for
-end users, this functionality is very useful.}
-
-To make matters worse, while in the current design of the package database,
-a package is uniquely identified by its package name and version, in
-the Backpack design, it is \emph{mandatory} that we support multiple
-packages installed in the database with the same package name and version,
-and this can result in complications in the user model.  This further
-complicates GHC's default package selection algorithm.
-
-In this section, we describe how the current algorithm operates (including
-what invariants it tries to uphold and where it goes wrong), and how
-to replace the algorithm to handle generalization to
-multiple instances in the package database.  We'll also try to tease
-apart the relationship between package keys and installed package IDs in
-the database.
-
-\paragraph{The current algorithm} Abstractly, GHC's current package
-selection algorithm operates as follows.  For every package name, select
-the package with the latest version (recall that this is unique) which
-is also \emph{valid}.  A package is valid if:
-
-\begin{itemize}
-    \item It exists in the package database,
-    \item All of its dependencies are valid,
-    \item It is not shadowed by a package with the same package ID\footnote{Recall that currently, a package ID uniquely identifies a package in the package database} in
-        another package database (unless it is in the transitive closure
-        of a package named by \texttt{-package-id}), and
-    \item It is not ignored with \texttt{-ignore-package}.
-\end{itemize}
-
-Package validity is probably the minimal criterion for to GHC to ensure
-that it can actually \emph{use} a package.  If the package is missing,
-GHC can't find the interface files or object code associated with the
-package.  Ignoring packages is a way of pretending that a package is
-missing from the database.
-
-Package validity is also a very weak criterion.  Another criterion we
-might hope holds is \emph{consistency}: when we consider the transitive
-closure of all selected packages, for any given package name, there
-should only be one instance providing that package.  It is trivially
-easy to break this property: suppose that I have packages \pname{a-1.0},
-\pname{b-1.0} compiled against \pname{a-1.0}, and \pname{a-1.1}.  GHC
-will happily load \pname{b-1.0} and \pname{a-1.1} together in the same
-interactive session (they are both valid and the latest versions), even
-though \pname{b-1.0}'s dependency is inconsistent with another package
-that was loaded.  The user will notice if they attempt to treat entities
-from \pname{a} reexported by \pname{b-1.0} and entities from
-\pname{a-1.1} as type equal.  Here is one user who had this problem:
-\url{http://stackoverflow.com/questions/12576817/}.  In some cases, the
-problem is easy to work around (there is only one offending package
-which just needs to be hidden), but if the divergence is deep in two
-separate dependency hierarchies, it is often easier to just blow away
-the package database and try again.
-
-Perversely, destructive reinstallation helps prevent these sorts of
-inconsistent databases.  While inconsistencies can arise when multiple
-versions of a package are installed, multiple versions will frequently
-lead to the necessity of reinstalls.  In the previous example, if a user
-attempts to Cabal install a package which depends on \pname{a-1.1} and
-\pname{b-1.0}, Cabal's dependency solver will propose reinstalling
-\pname{b-1.0} compiled against \pname{a-1.1}, in order to get a
-consistent set of dependencies.  If this reinstall is accepted, we
-invalidate all packages in the database which were previously installed
-against \pname{b-1.0} and \pname{a-1.0}, excluding them from GHC's
-selection process and making it more likely that the user will see a
-consistent view of the database.
-
-\paragraph{Enforcing consistent dependencies}  From the user's
-perspective, it would be desirable if GHC never loaded a set of packages
-whose dependencies were inconsistent.
-There are two ways we can go
-about doing this.  First, we can improve GHC's logic so that it doesn't
-pick an inconsistent set.  However, as a point of design, we'd like to
-keep whatever resolution GHC does as simple as possible (in an ideal
-world, we'd skip the validity checks entirely, but they ended up being
-necessary to prevent broken database from stopping GHC from starting up
-at all). In particular, GHC should \emph{not} learn how to do
-backtracking constraint solving: that's in the domain of Cabal.  Second,
-we can modify the logic of Cabal to enforce that the package database is
-always kept in a consistent state, similar to the consistency check
-Cabal applies to sandboxes, where it refuses to install a package to a
-sandbox if the resulting dependencies would not be consistent.
-
-The second alternative is a appealing, but Cabal sandboxes are currently
-designed for small, self-contained single projects, as opposed to the
-global ``universe'' that a default environment is intended to provide.
-For example, with a Cabal sandbox environment, it's impossible to
-upgrade a dependency to a new version without blowing away the sandbox
-and starting again.  To support upgrades, Cabal needs to do some work:
-when a new version is put in the default set, all of the
-reverse-dependencies of the old version are now inconsistent.  Cabal
-should offer to hide these packages or reinstall them compiled against
-the latest version.  Furthermore, because we in general may not have write
-access to all visible package databases, this visibility information
-must be independent of the package databases themselves.
-
-As a nice bonus, Cabal should also be able to snapshot the older
-environment which captures the state of the universe prior to the
-installation, in case the user wants to revert back.
-
-\paragraph{Modifying the default environment}  Currently, after GHC
-calculates the default package environment, a user may further modify
-the environment by passing package flags to GHC, which can be used to
-explicitly hide or expose packages.  How do these flags interact with
-our Cabal-managed environments?  Hiding packages is simple enough,
-but exposing packages is a bit dicier.  If a user asks for a different
-version of a package than in the default set, it will probably be
-inconsistent with the rest of the dependencies.  Cabal would have to
-be consulted to figure out a maximal set of consistent packages with
-the constraints given.  Alternatively, we could just supply the package
-with no claims of consistency.
-
-However, this use-case is rare.  Usually, it's not because they want a
-specific version: the package is hidden simply because we're not
-interested in loading it by default (\pname{ghc-api} is the canonical
-example, since it dumps a lot of modules in the top level namespace).
-If we distinguish packages which are consistent but hidden, their
-loads can be handled appropriately.
-
-\paragraph{Consistency in Backpack} We have stated as an implicit
-assumption that if we have both \pname{foo-1.0} and \pname{foo-1.1}
-available, only one should be loaded at a time.  What are the
-consequences if both of these packages are loaded at the same time?  An
-import of \m{Data.Foo} provided by both packages would be ambiguous and
-the user might find some type equalities they expect to hold would not.
-However, the result is not \emph{unsound}: indeed, we might imagine a
-user purposely wanting two different versions of a library in the same
-program, renaming the modules they provided so that they could be
-referred to unambiguously.  As another example, suppose that we have an
-indefinite package with a hole that is instantiated multiple times.  In
-this case, a user absolutely may want to refer to both instantiations,
-once again renaming modules so that they have unique names.
-
-There are two consequences of this.  First, while the default package
-set may enforce consistency, a user should still be able to explicitly
-ask for a package instance, renamed so that its modules don't conflict,
-and then use it in their program.  Second, instantiated indefinite packages
-should \emph{never} be placed in the default set, since it's impossible
-to know which instantiation is the one the user prefers.  A definite package
-can reexport an instantiated module under an unambiguous name if the user
-so pleases.
-
-\paragraph{Shadowing, installed package IDs, ABI hashes and package
-keys} Shadowing plays an important role for maintaining the soundness of
-compilation; call this the \emph{compatibility} of the package set.  The
-problem it addresses is when there are two distinct implementations of a
-module, but because their package ID (or package key, in the new world
-order) are the same, they are considered type equal.  It is absolutely
-wrong for a single program to include both implementations
-simultaneously (the symbols would conflict and GHC would incorrectly
-conclude things were type equal when they're not), so \emph{shadowing}'s
-job is to ensure that only one instance is picked, and all the other
-instances considered invalid (and their reverse-dependencies, etc.)
-Recall that in current GHC, within a package database, a package
-instance is uniquely identified by its package ID\@; thus, shadowing
-only needs to take place between package databases.  An interesting
-corner case is when the same package ID occurs in both databases, but
-the installed package IDs are the \emph{same}.  Because the installed
-package ID is currently simply an ABI hash, we skip shadowing, because
-the packages are---in principle---interchangeable.
-
-There are currently a number of proposed changes to this state of affairs:
-
-\begin{itemize}
-    \item Change installed package IDs to not be based on ABI hashes.
-        ABI hashes have a number of disadvantages as identifiers for
-        packages in the database.  First, they cannot be computed until
-        after compilation, which gave the multi-instance GSoC project a
-        few years some headaches.  Second, it's not really true that
-        programs with identical ABI hashes are interchangeable: a new
-        package may be ABI compatible but have different semantics.
-        Thus, installed package IDs are a poor unique identifier for
-        packages in the package database.  However, because GHC does not
-        give ABI stability guarantees, it would not be possible to
-        assume from here that packages with the same installed package
-        ID are ABI compatible.
-
-    \item Relaxing the uniqueness constraint on package IDs.  There are
-        actually two things that could be done here.  First, since we
-        have augmented package IDs with dependency resolution
-        information to form package keys, we could simply state that
-        package keys uniquely identify a package in a database.
-        Shadowing rules can be implemented in the same way as before, by
-        preferring the instance topmost on the stack.  Second, we could
-        also allow \emph{same-database} shadowing: that is, not even
-        package keys are guaranteed to be unique in a database: instead,
-        installed package IDs are the sole unique identifier of a
-        package.  This architecture is Nix inspired, as the intent is
-        to keep all package information in a centralized database.
-\end{itemize}
-
-Without mandatory package environments, same-database shadowing is a bad
-idea, because GHC now has no idea how to resolve shadowing.  Conflicting
-installed package IDs can be simulated by placing them in multiple
-package databases (in principle, the databases can be concatenated together
-and treated as a single monolitic database.)
-
-\section{Shapeless Backpack}\label{sec:simplifying-backpack}
-
-Backpack as currently defined always requires a \emph{shaping} pass,
-which calculates the shapes of all modules defined in a package.
-The shaping pass is critical to the solution of the double-vision problem
-in recursive module linking, but it also presents a number of unpalatable
-implementation problems:
-
-\begin{itemize}
-
-    \item \emph{Shaping is a lot of work.} A module shape specifies the
-        providence of all data types and identifiers defined by a
-        module. To calculate this, we must preprocess and parse all
-        modules, even before we do the type-checking pass.  (Fortunately,
-        shaping doesn't require a full parse of a module, only enough
-        to get identifiers.  However, it does have to understand import
-        statements at the same level of detail as GHC's renamer.)
-
-    \item \emph{Shaping must be done upfront.} In the current Backpack
-        design, all shapes must be computed before any typechecking can
-        occur.  While performing the shaping pass upfront is necessary
-        in order to solve the double vision problem (where a module
-        identity may be influenced by later definitions), it means
-        that GHC must first do a shaping pass, and then revisit every module and
-        compile them proper.  Nor is it (easily) possible to skip the
-        shaping pass when it is unnecessary, as one might expect to be
-        the case in the absence of mutual recursion.  Shaping is not
-        a ``pay as you go'' language feature.
-
-    \item \emph{GHC can't compile all programs shaping accepts.}  Shaping
-        accepts programs that GHC, with its current hs-boot mechanism, cannot
-        compile.  In particular, GHC requires that any data type or function
-        in a signature actually be \emph{defined} in the module corresponding
-        to that file (i.e., an original name can be assigned to these entities
-        immediately.)  Shaping permits unrestricted exports to implement
-        modules; this shows up in the formalism as $\beta$ module variables.
-
-    \item \emph{Shaping encourages inefficient program organization.}
-        Shaping is designed to enable mutually recursive modules, but as
-        currently implemented, mutual recursion is less efficient than
-        code without recursive dependencies. Programmers should avoid
-        this code organization, except when it is absolutely necessary.
-
-    \item \emph{GHC is architecturally ill-suited for directly
-        implementing shaping.}  Shaping implies that GHC's internal
-        concept of an ``original name'' be extended to accommodate
-        module variables.  This is an extremely invasive change to all
-        aspects of GHC, since the original names assumption is baked
-        quite deeply into the compiler.  Plausible implementations of
-        shaping requires all these variables to be skolemized outside
-        of GHC\@.
-
-\end{itemize}
-
-To be clear, the shaping pass is fundamentally necessary for some
-Backpack packages.  Here is the example which convinced Simon:
-
-\begin{verbatim}
-package p where
-    A :: [data T; f :: T -> T]
-    B = [export T(MkT), h; import A(f); data T = MkT; h x = f MkT]
-    A = [export T(MkT), f, h; import B; f MkT = MkT]
-\end{verbatim}
-
-The key to this example is that B \emph{may or may not typecheck} depending
-on the definition of A. Because A reexports B's definition T, B will
-typecheck; but if A defined T on its own, B would not typecheck.  Thus,
-we \emph{cannot} typecheck B until we have done some analysis of A (the
-shaping analysis!)
-
-Thus, it is beneficial (from an optimization point of view) to
-consider a subset of Backpack for which shaping is not necessary.
-Here is a programming discipline which does just that, which we will call the \textbf{linking restriction}: \emph{Module implementations must be declared before
-signatures.}  Formally, this restriction modifies the rule for merging
-polarized module shapes ($\widetilde{\tau}_1^{m_1} \oplus \widetilde{\tau}_2^{m_2}$) so that
-$\widetilde{\tau}_1^- \oplus \widetilde{\tau}_2^+$ is always undefined.\footnote{This seemed to be the crispest way of defining the restriction, although this means an error happens a bit later than I'd like it to: I'd prefer if we errored while merging logical contexts, but we don't know what is a hole at that point.}
-
-Here is an example of the linking restriction. Consider these two packages:
-
-\begin{verbatim}
-package random where
-    System.Random = [ ... ].hs
-
-package monte-carlo where
-    System.Random :: ...
-    System.MonteCarlo = [ ... ].hs
-\end{verbatim}
-
-Here, random is a definite package which may have been compiled ahead
-of time; monte-carlo is an indefinite package with a dependency
-on any package which provides \verb|System.Random|.
-
-Now, to link these two applications together, only one ordering
-is permissible:
-
-\begin{verbatim}
-package myapp where
-    include random
-    include monte-carlo
-\end{verbatim}
-
-If myapp wants to provide its own random implementation, it can do so:
-
-\begin{verbatim}
-package myapp2 where
-    System.Random = [ ... ].hs
-    include monte-carlo
-\end{verbatim}
-
-In both cases, all of \verb|monte-carlo|'s holes have been filled in by the time
-it is included.  The alternate ordering is not allowed.
-
-Why does this discipline prevent mutually recursive modules?  Intuitively,
-a hole is the mechanism by which we can refer to an implementation
-before it is defined; otherwise, we can only refer to definitions which
-preceed our definition. If there are never any holes \emph{which get filled},
-implementation links can only go backwards, ruling out circularity.
-
-It's easy to see how mutual recursion can occur if we break this discipline:
-
-\begin{verbatim}
-package myapp2 where
-    include monte-carlo
-    System.Random = [ import System.MonteCarlo ].hs
-\end{verbatim}
-
-\subsection{Typechecking of definite modules without shaping}
-
-If we are not carrying out a shaping pass, we need to be able to calculate
-$\widetilde{\Xi}_{\mathsf{pkg}}$ on the fly.  In the case that we are
-compiling a package---there will be no holes in the final package---we
-can show that shaping is unnecessary quite easily, since with the
-linking restriction, everything is definite from the get-go.
-
-Observe the following invariant: at any given step of the module
-bindings, the physical context $\widetilde{\Phi}$ contains no
-holes.  We can thus conclude that there are no module variables in any
-type shapes.  As the only time a previously calculated package shape can
-change is due to unification, the incrementally computed shape is in
-fact the true one.
-
-As far as the implementation is concerned, we never have to worry
-about handling module variables; we only need to do extra typechecks
-against (renamed) interface files.
-
-\subsection{Compiling definite packages}\label{sec:compiling}
-
-% New definitions
-\algnewcommand\algorithmicswitch{\textbf{switch}}
-\algnewcommand\algorithmiccase{\textbf{case}}
-\algnewcommand\algorithmicassert{\texttt{assert}}
-% New "environments"
-\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
-\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ ``#1''}{\algorithmicend\ \algorithmiccase}%
-\algtext*{EndSwitch}%
-\algtext*{EndCase}%
-
-\begin{algorithm}
-    \caption{Compilation of definite packages (assume \texttt{-hide-all-packages} on all \texttt{ghc} invocations)}\label{alg:compile}
-\begin{algorithmic}
-    \Procedure{Compile}{\textbf{package} $P$ \textbf{where} $\vec{B}$, $H$, $db$}\Comment{}$H$ maps hole module names to identities
-    \State$flags\gets \nil$
-    \State$\mathcal{K}$ $\gets$ \Call{Hash}{$P + H$}
-    \State%
-    In-place register the package $\mathcal{K}$ in $db$
-    \For{$B$ \textbf{in} $\vec{B}$}
-        \Case{$p = p\texttt{.hs}$}
-        \State\Call{Exec}{\texttt{ghc -c} $p$\texttt{.hs} \texttt{-package-db} $db$ \texttt{-this-package-key} $\mathcal{K}$ $flags$}
-        \EndCase%
-        \Case{$p$ $\cc$ $p$\texttt{.hsig}}
-            \State\Call{Exec}{\texttt{ghc -c} $p$\texttt{.hsig} \texttt{-package-db} $db$ \texttt{-sig-of} $H(p)$ $flags$}
-        \EndCase%
-        \Case{$p = p'$}
-            \State$flags\gets flags$ \texttt{-alias} $p$ $p'$
-        \EndCase%
-        \Case{\Cinc{$P'$} $\langle\vec{p_H\mapsto p_H'}, \vec{p\mapsto p'} \rangle$}
-            \State\textbf{let} $H'(p_H) = $ \Call{ResolveModule}{$p_H'$}
-            \State$\mathcal{K}'\gets$ \Call{Compile}{$P'$, $H'$, $db$}\Comment{}Nota bene: not $flags$
-            \State$flags\gets flags$ \texttt{-package} $\mathcal{K}'$ $\langle\vec{p\mapsto p'}\rangle$
-        \EndCase%
-    \EndFor%
-    \State%
-    Remove $\mathcal{K}$ from $db$
-    \State%
-    Install the complete package $\mathcal{K}$ to the global database
-    \State\Return$\mathcal{K}$
-    \EndProcedure%
-\end{algorithmic}
-\end{algorithm}
-
-The full recursive procedure for compiling a Backpack package using
-one-shot compilation is given in Figure~\ref{alg:compile}.  We
-recursively walk through Backpack descriptions, processing each line by
-invoking GHC and/or modifying our package state.  Here is a more
-in-depth description of the algorithm, line-by-line:
-
-\paragraph{The parameters} To compile a package description for package
-$P$, we need to know $H$, the mapping of holes $p_H$ in package $P$ to
-physical module identities $\nu$ which are implementing them; this
-mapping is used to calculate the package key $\mathcal{K}$ for the
-package in question.  Furthermore, we have an inplace package database
-$db$ in which we will register intermediate build results, including
-partially compiled parent packages which may provide implementations
-of holes for packages they include.
-
-\subsection{Compiling implementations}
-
-We compile modules in the same way we do today, but with some extra
-package visibility $flags$, which let GHC know how to resolve imports
-and look up original names.  We'll describe what the new flags are
-and also discuss some subtleties with module lookup.
-
-\paragraph{In-place registration}  Perhaps surprisingly, we start
-compilation by registering the (uncompiled) package in the in-place
-package database.  This registration does not expose packages, and is
-purely intended to inform the compilation of subpackages where to
-find modules that are provided by the parent (in-progress) package,
-as well as provide auxiliary information, e.g., such as the package name
-and version for error reporting.  The pre-registration trick is an old
-one used by the GHC build system; the key invariant to look out for
-is that we shouldn't reference original names in modules that haven't
-been built yet.  This is enforced by our manual tracking of holes in
-$H$: a module can't occur in $H$ unless it's already been compiled!
-
-\paragraph{New package resolution algorithm}  Currently, invocations
-of \texttt{-package} and similar flags have the result of \emph{hiding}
-other exposed packages with the same name.  However, this is not going
-to work for Backpack: an indefinite package may get loaded multiple times
-with different instantiations, and it might even make sense to load multiple
-versions of the same package simultaneously, as long as their modules
-are renamed to not conflict.
-
-Thus, we impose the following behavior change: when
-\texttt{-hide-all-packages} is specified, we do \emph{not} automatically
-hide packages with the same name as a package specified by
-\texttt{-package} (or a similar flag): they are all included, even if
-there are conflicts.  To deal with conflicts, we augment the syntax of
-\texttt{-package} to also accept a list of thinnings and renamings, e.g.
-\texttt{-package} \pname{containers} $\langle\m{Data.Set},
-\m{Data.Map}\mapsto \m{Map}\rangle$ says to make visible for import
-\m{Data.Set} and \m{Map} (which is \m{Data.Map} renamed.)  This means
-that
-\texttt{-package} \pname{containers-0.9} $\langle\m{Data.Set}\mapsto
-\m{Set09}\rangle$ \texttt{-package} \pname{containers-0.8}
-$\langle\m{Data.Set}\mapsto \m{Set08}\rangle$ now uses both packages
-concurrently (previously, GHC would hide one of them.)
-
-Additionally, it's important to note that two packages exporting the
-same module do not \emph{necessarily} cause a conflict; the modules
-may be linkable.  For example, \texttt{-package} \pname{containers} $\langle\m{Data.Set}\rangle$
-\texttt{-package} \pname{containers} $\langle\m{Data.Set}\rangle$ is fine, because
-precisely the same implementation of \m{Data.Set} is loaded in both cases.
-A similar situation can occur with signatures:
-
-\begin{verbatim}
-package p where
-    A :: [ x :: Int ]
-package q
-    include p
-    A :: [ y :: Int ]
-    B = [ import A; z = x + y ] -- *
-package r where
-    A = [ x = 0; y = 0 ]
-    include q
-\end{verbatim}
-
-Here, both \pname{p} and \pname{q} are visible when compiling the starred
-module, which compiles with the flags \texttt{-package} \pname{p}, but there
-are two interface files available: one available locally, and one from \pname{p}.
-Both of these interface files are \emph{forwarding} to the original implementation
-\pname{r} (more on this in the ``Compiling signatures'' file), so rather than
-reporting an ambiguous import, we instead have to merge the two interface files
-together. This is done by simulating multiple imports: one to each interface
-file. This works because GHC does not consider symbols with equal original names
-as conflicting.
-
-Note that we do not need to merge signatures with an implementation, in such
-cases, we should just use the implementation interface.  E.g.
-
-\begin{verbatim}
-package p where
-    A :: ...
-package q where
-    A = ...
-    include p
-    B = [ import A ]    -- *
-\end{verbatim}
-
-Here, \m{A} is available both from \pname{p} and \pname{q}, but the use in the
-starred module should be done with respect to the full implementation.
-
-\paragraph{The \texttt{-alias} flag}  We introduce a new flag
-\texttt{-alias} for aliasing modules.  Aliasing is analogous to
-the merging that can occur when we include packages, but it also applies
-to modules which are locally defined.  When we alias a module $p$ with
-$p'$, we require that $p'$ exists in the current module mapping, and then
-we attempt to add an entry for it at entry $p$.  If there is no mapping for
-$p$, this succeeds; otherwise, we apply the same conflict resolution algorithm.
-
-\subsection{Compiling signatures}
-
-Signature compilation is triggered when we compile a signature file.
-This mode similar to how we process \verb|hs-boot| files, except
-we pass an extra flag \verb|-sig-of| which specifies what the
-identity of the actual implementation of the signature is (according to our $H$
-mapping).  This is guaranteed to exist, due to the linking
-restriction, although it may be in a partially registered package
-in $db$.  If the module is \emph{not} currently available under the same name of the
-\texttt{hsig} file, we output an \texttt{hi} file which, for all declarations the
-signature exposes, forwards their definitions to the original
-implementation file.  The intent is that any code in the current package
-which compiles against this signature will use this signature \texttt{hi} file,
-not the original one \texttt{hi} file.
-For example, the \texttt{hi} file produced when compiling the starred interface
-points to the implementation in package \pname{q}.
-
-\begin{verbatim}
-package p where
-    A :: ...    -- *
-    B = [ import A; ... ]
-package q where
-    A = [ ... ]
-    include p
-\end{verbatim}
-
-\paragraph{Sometimes \texttt{hi} is unnecessary}
-In the following package:
-
-\begin{verbatim}
-package p where
-    P = ...
-    P :: ...
-\end{verbatim}
-
-Paper Backpack specifies that we check the signature \m{P} against implementation
-\m{P}, but otherwise no changes are made (i.e., the signature does not narrow
-the implementation.) In this case, it is not necessary to generate an \texttt{hi} file;
-the original interface file suffices.
-
-\paragraph{Multiple signatures}  As a simplification, we assume that there
-is only one signature per logical name in a package.  (This prevents
-us from expressing mutual recursion in signatures, but let's not worry
-about it for now.)
-
-\paragraph{Restricted recursive modules ala hs-boot}\label{sec:hs-boot-restrict}
-When we compile an \texttt{hsig} file without any \texttt{-sig-of} flag (because
-no implementation is known), we fall back to old-style GHC mutual recursion.
-Na\"\i vely, a shaping pass would be necessary;
-so we adopt an existing constraint that
-already applies to hs-boot files: \emph{at the time we define a signature,
-we must know what the original name for all data types is}.  In practice,
-GHC enforces this by stating that: (1) an hs-boot file must be
-accompanied with an implementation, and (2) the implementation must
-in fact define (and not reexport) all of the declarations in the signature.
-We can discover if a signature is intended to break a recursive module loop
-when we discover that $p\notin flags_H$; in this case, we fallback to the
-old hs-boot behavior. (Alternatively, the user can explicitly ask for it.)
-
-Why does this not require a shaping pass? The reason is that the
-signature is not really polymorphic: we require that the $\alpha$ module
-variable be resolved to a concrete module later in the same package, and
-that all the $\beta$ module variables be unified with $\alpha$. Thus, we
-know ahead of time the original names and don't need to deal with any
-renaming.\footnote{This strategy doesn't completely resolve the problem
-of cross-package mutual recursion, because we need to first compile a
-bit of the first package (signatures), then the second package, and then
-the rest of the first package.}
-
-Compiling packages in this way gives the tantalizing possibility
-of true separate compilation: the only thing we don't know is what the actual
-package name of an indefinite package will be, and what the correct references
-to have are.  This is a very minor change to the assembly, so one could conceive
-of dynamically rewriting these references at the linking stage.  But
-separate compilation achieved in this fashion would not be able to take
-advantage of cross-module optimizations.
-
-\subsection{Compiling includes}
-
-Includes are the most interesting part of the compilation process, as we have
-calculate how the holes of the subpackage we are filling in are compiled $H'$
-and modify our flags to make the exports of the include visible to subsequently
-compiled modules.  We consider the case with renaming, since includes with
-no renaming are straightforward.
-
-First, we assume that we know \emph{a priori} what the holes of a
-package $p_H$ are (either by some sort of pre-pass, or explicit
-declaration.)  For each of their \emph{renamed targets} $p'_H$, we determine
-what the original module associated with the $p'_H$ is, based off of
-the package database that we have been manipulating.
-For example:
-
-\begin{verbatim}
-package p where
-    A :: ...
-    ...
-package q where
-    A = [ ... ]
-    B = [ ... ]
-    include p (A as B)
-\end{verbatim}
-
-When computing the entry $H(\pname{A})$, we determine what the original
-module for \pname{B} is.
-
-Next, we recursively call \textsc{Compile} with the computed $H'$.
-Note that the entries in $H$ may refer to modules which would not be
-picked up by $flags$, but they will be registered in the inplace
-package database $db$.
-For example, in this situation:
-
-\begin{verbatim}
-package p where
-    B :: ...
-    C = [ import B; ... ]
-package q where
-    A = [ ... ]
-    B = [ import A; ... ]
-    include p
-    D = [ import C; ... ]
-\end{verbatim}
-
-When we recursively process package \pname{p}, $H$ will refer to
-\pname{q}:\m{B}, and we need to know where to find it (\pname{q} is only
-partially processed and so is in the inplace package database.)
-Furthermore, the interface file for \m{B} may refer to \pname{q}:\m{A},
-and thus we likewise need to know how to find its interface file.
-
-Note that the inplace package database is not expected to expose intermediate
-packages. Otherwise, this example would improperly compile:
-
-\begin{verbatim}
-package p where
-    B = [ import A; ... ]
-package q where
-    A = ...
-    include p
-\end{verbatim}
-
-\pname{p} does not compile on its own, so it should not compile if it is
-recursively invoked from \pname{q}.  However, if we exposed the modules
-of the partially registered package \pname{q}, \m{A} is now suddenly
-resolvable.
-
-Finally, once the subpackage is compiled, we can add it to our $flags$ so later
-modules we compile see its (appropriately thinned and renamed) modules, and like
-aliasing.
-
-\paragraph{Absence of an \texttt{hi} file}
-It is important that when we resolve a module, we look up the \emph{implementor}
-of a module, and not just a signature which is providing it at some name.
-Sometimes, it can be a bit indirect, for example:
-
-\begin{verbatim}
-package p where
-    A :: [ y :: Int ]
-package q where
-    A :: [ x :: Int ]
-    include p -- *
-package r where
-    A = [ x = 0; y = 1 ]
-    include q
-\end{verbatim}
-
-When computing $H'$ for the starred include, our $flags$ only include
-\texttt{-package-dir} \pname{r} $cwd_r$ $\langle\rangle$: with a thinning
-that excludes all modules!  The only interface file we can pick up with these
-$flags$ is the local definition of \m{A}.  However, we \emph{absolutely}
-should set $H'(\m{A})=\pname{q}:\m{A}$; if we do so, then we will incorrectly
-conclude when compiling the signature in \pname{p} that the implementation
-doesn't export enough identifiers to fulfill the signature (\texttt{y} is not
-available from just the signature in \pname{q}).  Instead, we have to look
-up the original implementor of \m{A} in \pname{r}, and use that in $H'$.
-If you maintain the invariant that you always know what the original implementor
-is of all modules in scope, it's easy enough to figure this out.
-
-\subsection{Commentary}
-
-\paragraph{Just because it compiled, doesn't mean the individual packages type check}
-The compilation mechanism described is slightly more permissive than vanilla Backpack.
-Here is a simple example:
-
-\begin{verbatim}
-package p where
-    A :: [ data T = T ]
-    B :: [ data T = T ]
-    C = [
-        import A
-        import B
-        x = A.T :: B.T
-    ]
-package q where
-    A = [ data T = T ]
-    B = A
-    include p
-\end{verbatim}
-
-Here, we incorrectly decide \m{A}\verb|.T| and \m{B}\verb|.T| are type
-equal when typechecking \m{C}, because the \verb|hisig| files we
-generate for them all point to the same original implementation.  However,
-\pname{p} should not typecheck.
-
-The problem here is that type checking asks ``does it compile with respect
-to all possible instantiations of the holes'', whereas compilation asks
-``does it compile with respect to this particular instantiation of holes.''
-In the absence of a shaping pass, this problem is unavoidable.
-
-\section{Shaped Backpack}
-
-Despite the simplicity of shapeless Backpack with the linking
-restriction in the absence of holes, we will find that when we have
-holes, it will be very difficult to do type-checking without
-some form of shaping.  This section is very much a work in progress,
-but the ability to typecheck against holes, even with the linking restriction,
-is a very important part of modular separate development, so we will need
-to support it at some point.
-
-\subsection{Efficient shaping}
-
-(These are Edward's opinion, he hasn't convinced other folks that this is
-the right way to do it.)
-
-In this section, I want to argue that, although shaping constitutes
-a pre-pass which must be run before compilation in earnest, it is only
-about as bad as the dependency resolution analysis that GHC already does
-in \verb|ghc -M| or \verb|ghc --make|.
-
-In Paper Backpack, what information does shaping compute? It looks at
-exports, imports, data declarations and value declarations (but not the
-actual expressions associated with these values.)  As a matter of fact,
-GHC already must look at the imports associated with a package in order
-to determine the dependency graph, so that it can have some order to compile
-modules in.  There is a specialized parser which just parses these statements,
-and then ignores the rest of the file.
-
-A bit of background: the \emph{renamer} is responsible for resolving
-imports and figuring out where all of these entities actually come from.
-SPJ would really like to avoid having to run the renamer in order to perform
-a shaping pass.
-
-\paragraph{Is it necessary to run the Renamer to do shaping?}
-Edward and Scott believe the answer is no, well, partially.
-Shaping needs to know the original names of all entities exposed by a
-module/signature. Then it needs to know (a) which entities a module/signature
-defines/declares locally and (b) which entities that module/signature exports.
-The former, (a), can be determined by a straightforward inspection of a parse
-tree of the source file.\footnote{Note that no expression or type parsing
-is necessary. We only need names of local values, data types, and data
-constructors.} The latter, (b), is a bit trickier. Right now it's the Renamer
-that interprets imports and exports into original names, so we would still
-rely on that implementation. However, the Renamer does other, harder things
-that we don't need, so ideally we could factor out the import/export
-resolution from the Renamer for use in shaping.
-
-Unfortunately the Renamer's import resolution analyzes \verb|.hi| files, but for
-local modules, which haven't yet been typechecked, we don't have those.
-Instead, we could use a new file format, \verb|.hsi| files, to store the shape of
-a locally defined module. (Defined packages are bundled with their shapes,
-so included modules have \verb|.hsi| files as well.) (What about the logical
-vs.~physical distinction in file names?) If we refactor the import/export
-resolution code, could we rewrite it to generically operate on both
-\verb|.hi| files and \verb|.hsi| files?
-
-Alternatively, rather than storing shapes on a per-source basis, we could
-store (in memory) the entire package shape. Similarly, included packages
-could have a single shape file for the entire package. Although this approach
-would make shaping non-incremental, since an entire package's shape would
-be recomputed any time a constituent module's shape changes, we do not expect
-shaping to be all that expensive.
-
-\subsection{Typechecking of indefinite modules}\label{sec:typechecking-indefinite}
-
-Recall in our argument in the definite case, where we showed there are
-no holes in the physical context.  With indefinite modules, this is no
-longer true. While (with the linking restriction) these holes will never
-be linked against a physical implementation, they may be linked against
-other signatures.  (Note: while disallowing signature linking would
-solve our problem, it would disallow a wide array of useful instances of
-signature reuse, for example, a package mylib that implements both
-mylib-1x-sig and mylib-2x-sig.)
-
-With holes, we must handle module variables, and we sometimes must unify them:
-
-\begin{verbatim}
-package p where
-    A :: [ data A ]
-package q where
-    A :: [ data A ]
-package r where
-    include p
-    include q
-\end{verbatim}
-
-In this package, it is not possible to a priori assign original names to
-module A in p and q, because in package r, they should have the same
-original name.  When signature linking occurs, unification may occur,
-which means we have to rename all relevant original names. (A similar
-situation occurs when a module is typechecked against a signature.)
-
-An invariant which would be nice to have is this: when typechecking a
-signature or including a package, we may apply renaming to the entities
-being brought into context.  But once we've picked an original name for
-our entities, no further renaming should be necessary. (Formally, in the
-unification for semantic object shapes, apply the unifier to the second
-shape, but not the first one.)
-
-However, there are plenty of counterexamples here:
-
-\begin{verbatim}
-package p where
-    A :: [ data A ]
-    B :: [ data A ]
-    M = ...
-    A = B
-\end{verbatim}
-
-In this package, does module M know that A.A and B.A are type equal?  In
-fact, the shaping pass will have assigned equal module identities to A
-and B, so M \emph{equates these types}, despite the aliasing occurring
-after the fact.
-
-We can make this example more sophisticated, by having a later
-subpackage which causes the aliasing; now, the decision is not even a
-local one (on the other hand, the equality should be evident by inspection
-of the package interface associated with q):
-
-\begin{verbatim}
-package p where
-    A :: [ data A ]
-    B :: [ data A ]
-package q where
-    A :: [ data A ]
-    B = A
-package r where
-    include p
-    include q
-\end{verbatim}
-
-Another possibility is that it might be acceptable to do a mini-shaping
-pass, without parsing modules or signatures, \emph{simply} looking at
-names and aliases.  But logical names are not the only mechanism by
-which unification may occur:
-
-\begin{verbatim}
-package p where
-    C :: [ data A ]
-    A = [ data A = A ]
-    B :: [ import A(A) ]
-    C = B
-\end{verbatim}
-
-It is easy to conclude that the original names of C and B are the same.  But
-more importantly, C.A must be given the original name of p:A.A.  This can only
-be discovered by looking at the signature definition for B. In any case, it
-is worth noting that this situation parallels the situation with hs-boot
-files (although there is no mutual recursion here).
-
-The conclusion is that you will probably, in fact, have to do real
-shaping in order to typecheck all of these examples.
-
-\paragraph{Hey, these signature imports are kind of tricky\ldots}
-
-When signatures and modules are interleaved, the interaction can be
-complex.  Here is an example:
-
-\begin{verbatim}
-package p where
-    C :: [ data A ]
-    M = [ import C; ... ]
-    A = [ import M; data A = A ]
-    C :: [ import A(A) ]
-\end{verbatim}
-
-Here, the second signature for C refers to a module implementation A
-(this is permissible: it simply means that the original name for p:C.A
-is p:A.A).  But wait! A relies on M, and M relies on C. Circularity?
-Fortunately not: a client of package p will find it impossible to have
-the hole C implemented in advance, since they will need to get their hands on module
-A\ldots but it will not be defined prior to package p.
-
-In any case, however, it would be good to emit a warning if a package
-cannot be compiled without mutual recursion.
-
-\subsection{Rename on entry}
-
-Consider the following example:
-
-\begin{verbatim}
-package p where
-    A :: [ data T = T ]
-    B = [ import A; x = T ]
-package q where
-    C :: ...
-    A = [ data T = T ]
-    include p
-    D = [
-        import qualified A
-        import qualified B
-        import C
-        x = B.T :: A.T
-    ]
-\end{verbatim}
-
-We are interested in type-checking \pname{q}, which is an indefinite package
-on account of the uninstantiated hole \m{C}.  Furthermore, let's suppose that
-\pname{p} has already been independently typechecked, and its interface files
-installed in some global location with $\alpha_A$ used as the module identity
-of \m{A}. (To simplify this example, we'll assume $\beta_{AT}=\alpha_A$.)
-
-The first three lines of \pname{q} type check in the normal way, but \m{D}
-now poses a problem: if we load the interface file for \m{B} the normal way,
-we will get a reference to type \texttt{T} with the original name $\alpha_A$.\texttt{T},
-whereas from \m{A} we have an original name \pname{q}:\m{A}.\texttt{T}.
-
-Let's suppose that we already have the result of a shaping pass, which
-maps our identity variables to their true identities.
-Let's consider the possible options here:
-
-\begin{itemize}
-    \item We could re-typecheck \pname{p}, feeding it the correct instantiations
-        for its variables.  However, this seems wasteful: we typechecked the
-        package already, and up-to-renaming, the interface files are exactly
-        what we need to type check our application.
-    \item We could make copies of all the interface files, renamed to have the
-        right original names.  This also seems wasteful: why should we have to
-        create a new copy of every interface file in a library we depend on?
-    \item When \emph{reading in} the interface file to GHC, we could apply the
-        renaming according to the shaping pass and store that in memory.
-\end{itemize}
-
-That last solution is pretty appealing, however, there are still circumstances
-we need to create new interface files; these exactly mirror the cases described
-in Section~\ref{sec:compiling}.
-
-\subsection{Incremental typechecking}
-We want to typecheck modules incrementally, i.e., when something changes in
-a package, we only want to re-typecheck the modules that care about that
-change. GHC already does this today.%
-\footnote{\url{https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/RecompilationAvoidance}}
-Is the same mechanism sufficient for Backpack? Edward and Scott think that it
-is, mostly. Our conjecture is that a module should be re-typechecked if the
-existing mechanism says it should \emph{or} if the logical shape
-context (which maps logical names to physical names) has changed. The latter
-condition is due to aliases that affect typechecking of modules.
-
-Let's look again at an example from before:
-\begin{verbatim}
-package p where
-    A :: [ data A ]
-    B :: [ data A ]
-    M = [ import A; import B; ... ]
-\end{verbatim}
-Let's say that \verb|M| is typechecked successfully. Now we add an alias binding
-at the end of the package, \verb|A = B|. Does \verb|M| need to be
-re-typechecked? Yes! (Well, it seems so, but let's just assert ``yes'' for now.
-Certainly in the reverse case---if we remove the alias and then ask---this
-is true, since \verb|M| might have depended on the two \verb|A| types
-being the same.)
-The logical shape context changed to say that \verb|A| and
-\verb|B| now map to the same physical module identity. But does the existing
-recompilation avoidance mechanism say that \verb|M| should be re-typechecked?
-It's unclear. The \verb|.hi| file for \verb|M| records that it imported \verb|A| and
-\verb|B| with particular ABIs, but does it also know about the physical module
-identities (or rather, original module names) of these modules?
-
-Scott thinks this highlights the need for us to get our story straight about
-the connection between logical names, physical module identities, and file
-names!
-
-
-\subsection{Installing indefinite packages}\label{sec:installing-indefinite}
-
-If an indefinite package contains no code at all, we only need
-to install the interface file for the signatures.  However, if
-they include code, we must provide all of the
-ingredients necessary to compile them when the holes are linked against
-actual implementations.  (Figure~\ref{fig:pkgdb})
-
-\paragraph{Source tarball or preprocessed source?}  What is the representation of the source that is saved is.  There
-are a number of possible choices:
-
-\begin{itemize}
-    \item The original tarballs downloaded from Hackage,
-    \item Preprocessed source files,
-    \item Some sort of internal, type-checked representation of Haskell code (maybe the output of the desugarer).
-\end{itemize}
-
-Storing the tarballs is the simplest and most straightforward mechanism,
-but we will have to be very certain that we can recompile the module
-later in precisely the same we compiled it originally, to ensure the hi
-files match up (fortunately, it should be simple to perform an optional
-sanity check before proceeding.) The appeal of saving preprocessed
-source, or even the IRs, is that this is conceptually this is exactly
-what an indefinite package is: we have paused the compilation process
-partway, intending to finish it later.  However, our compilation strategy
-for definite packages requires us to run this step using a \emph{different}
-choice of original names, so it's unclear how much work could actually be reused.
-
-\paragraph{Sources in sandboxes}  Another nice way to implement indefinite
-packages is to register them as source packages in a Cabal sandbox, and then
-teach Cabal how to build them multiple times in the compile process.  Perhaps
-the global package database should be extended with a directory of source
-packages in order to support indefinite packages.
-
-\section{Surface syntax}
-
-In the Backpack paper, a brand new module language is presented, with
-syntax for inline modules and signatures.  This syntax is probably worth implementing,
-because it makes it easy to specify compatibility packages, whose module
-definitions in general may be very short:
-
-\begin{verbatim}
-package ishake-0.12-shake-0.13 where
-    include shake-0.13
-    Development.Shake.Sys = Development.Shake.Cmd
-    Development.Shake = [ (**>) = (&>) ; (*>>) = (|*>)]
-    Development.Shake.Rule = [ defaultPriority = rule . priority 0.5 ]
-    include ishake-0.12
-\end{verbatim}
-
-However, there are a few things that are less than ideal about the
-surface syntax proposed by Paper Backpack:
-
-\begin{itemize}
-    \item It's completely different from the current method users
-        specify packages. There's nothing wrong with this per se
-        (one simply needs to support both formats) but the smaller
-        the delta, the easier the new packaging format is to explain
-        and implement.
-
-    \item Sometimes order matters (relative ordering of signatures and
-        module implementations), and other times it does not (aliases).
-        This can be confusing for users.
-
-    \item Users have to order module definitions topologically,
-        whereas in current Cabal modules can be listed in any order, and
-        GHC figures out an appropriate order to compile them.
-\end{itemize}
-
-Here is an alternative proposal, closely based on Cabal syntax.  Given
-the following Backpack definition:
-
-\begin{verbatim}
-package libfoo(A, B, C, Foo) where
-    include base
-    -- renaming and thinning
-    include libfoo (Foo, Bar as Baz)
-    -- holes
-    A :: [ a :: Bool ].hsig
-    A2 :: [ b :: Bool ].hsig
-    -- normal module
-    B = [
-        import {-# SOURCE #-} A
-        import Foo
-        import Baz
-        ...
-    ].hs
-    -- recursively linked pair of modules, one is private
-    C :: [ data C ].hsig
-    D = [ import {-# SOURCE #-} C; data D = D C ].hs
-    C = [ import D; data C = C D ].hs
-    -- alias
-    A = A2
-\end{verbatim}
-
-We can write the following Cabal-like syntax instead (where
-all of the signatures and modules are placed in appropriately
-named files):
-
-\begin{verbatim}
-package: libfoo
-...
-build-depends: base, libfoo (Foo, Bar as Baz)
-required-signatures: A A2 -- deferred for now
-exposed-modules: Foo B C
-aliases: A = A2
-other-modules: D
-\end{verbatim}
-
-Notably, all of these lists are \emph{insensitive} to ordering!
-The key idea is use of the \verb|{-# SOURCE #-}| pragma, which
-is enough to solve the important ordering constraint between
-signatures and modules.
-
-Here is how the elaboration works.  For simplicity, in this algorithm
-description, we assume all packages being compiled have no holes
-(including \verb|build-depends| packages). Later, we'll discuss how to
-extend the algorithm to handle holes in both subpackages and the main
-package itself.
-
-\begin{enumerate}
-
-    \item At the top-level with \verb|package| $p$ and
-        \verb|exposed-modules| $ms$, record \verb|package p (ms) where|
-
-    \item For each package $p$ with thinning/renaming $ms$ in
-        \verb|build-depends|, record a \verb|include p (ms)| in the
-        Backpack package.  The ordering of these includes does not
-        matter, since none of these packages have holes.
-
-    \item Take all modules $m$ in \verb|other-modules| and
-        \verb|exposed-modules| which were not exported by build
-        dependencies, and create a directed graph where hs and hs-boot
-        files are nodes and imports are edges (the target of an edge is
-        an hs file if it is a normal import, and an hs-boot file if it
-        is a SOURCE import).  Topologically sort this graph, erroring if
-        this graph contains cycles (even with recursive modules, the
-        cycle should have been broken by an hs-boot file).  For each
-        node, in this order, record \verb|M = [ ... ]| or \verb|M :: [ ... ]|
-        depending on whether or not it is an hs or hs-boot.  If possible,
-        sort signatures before implementations when there is no constraint
-        otherwise.
-
-\end{enumerate}
-
-Here is a simple example which shows how SOURCE can be used to disambiguate
-between two important cases. Suppose we have these modules:
-
-\begin{verbatim}
--- A1.hs
-import {-# SOURCE #-} B
-
--- A2.hs
-import B
-
--- B.hs
-x = True
-
--- B.hs-boot
-x :: Bool
-\end{verbatim}
-
-Then we translate the following packages as follows:
-
-\begin{verbatim}
-exposed-modules: A1 B
--- translates to
-B :: [ x :: Bool ]
-A1 = [ import B ]
-B = [ x = True ]
-\end{verbatim}
-
-but
-
-\begin{verbatim}
-exposed-modules: A2 B
--- translates to
-B = [ x = True ]
-B :: [ x :: Bool ]
-A2 = [ import B ]
-\end{verbatim}
-
-The import controls placement between signature and module, and in A1 it
-forces B's signature to be sorted before B's implementation (whereas in
-the second section, there is no constraint so we preferentially place
-the B's implementation first)
-
-\paragraph{Holes in the database} In the presence of holes,
-\verb|build-depends| resolution becomes more complicated.  First,
-let's consider the case where the package we are building is
-definite, but the package database contains indefinite packages with holes.
-In order to maintain the linking restriction, we now have to order packages
-from step (2) of the previous elaboration.  We can do this by creating
-a directed graph, where nodes are packages and edges are from holes to the
-package which implements them.  If there is a cycle, this indicates a mutually
-recursive package.  In the absence of cycles, a topological sorting of this
-graph preserves the linking invariant.
-
-One subtlety to consider is the fact that an entry in \verb|build-depends|
-can affect how a hole is instantiated by another entry.  This might be a
-bit weird to users, who might like to explicitly say how holes are
-filled when instantiating a package.  Food for thought, surface syntax wise.
-
-\paragraph{Holes in the package} Actually, this is quite simple: the
-ordering of includes goes as before, but some indefinite packages in the
-database are less constrained as they're ``dependencies'' are fulfilled
-by the holes at the top-level of this package.  It's also worth noting
-that some dependencies will go unresolved, since the following package
-is valid:
-
-\begin{verbatim}
-package a where
-    A :: ...
-package b where
-    include a
-\end{verbatim}
-
-\paragraph{Multiple signatures}  In Backpack syntax, it's possible to
-define a signature multiple times, which is necessary for mutually
-recursive signatures:
-
-\begin{verbatim}
-package a where
-    A :: [ data A ]
-    B :: [ import A; data B = B A ]
-    A :: [ import B; data A = A B ]
-\end{verbatim}
-
-Critically, notice that we can see the constructors for both module B and A
-after the signatures are linked together.  This is not possible in GHC
-today, but could be possible by permitting multiple hs-boot files.  Now
-the SOURCE pragma indicating an import must \emph{disambiguate} which
-hs-boot file it intends to include.  This might be one way of doing it:
-
-\begin{verbatim}
--- A.hs-boot2
-data A
-
--- B.hs-boot
-import {-# SOURCE hs-boot2 #-} A
-
--- A.hs-boot
-import {-# SOURCE hs-boot #-} B
-\end{verbatim}
-
-\paragraph{Explicit or implicit reexports}  One annoying property of
-this proposal is that, looking at the \verb|exposed-modules| list, it is
-not immediately clear what source files one would expect to find in the
-current package.  It's not obvious what the proper way to go about doing
-this is.
-
-\paragraph{Better syntax for SOURCE}  If we enshrine the SOURCE import
-as a way of solving Backpack ordering problems, it would be nice to have
-some better syntax for it. One possibility is:
-
-\begin{verbatim}
-abstract import Data.Foo
-\end{verbatim}
-
-which makes it clear that this module is pluggable, typechecking against
-a signature.  Note that this only indicates how type checking should be
-done: when actually compiling the module we will compile against the
-interface file for the true implementation of the module.
-
-It's worth noting that the SOURCE annotation was originally made a
-pragma because, in principle, it should have been possible to compile
-some recursive modules without needing the hs-boot file at all. But if
-we're moving towards boot files as signatures, this concern is less
-relevant.
-
-\section{Type classes and type families}
-
-\subsection{Background}
-
-Before we talk about how to support type classes in Backpack, it's first
-worth talking about what we are trying to achieve in the design.  Most
-would agree that \emph{type safety} is the cardinal law that should be
-preserved (in the sense that segfaults should not be possible), but
-there are many instances of ``bad behavior'' (top level mutable state,
-weakening of abstraction guarantees, ambiguous instance resolution, etc)
-which various Haskellers may disagree on the necessity of ruling out.
-
-With this in mind, it is worth summarizing what kind of guarantees are
-presently given by GHC with regards to type classes and type families,
-as well as characterizing the \emph{cultural} expectations of the
-Haskell community.
-
-\paragraph{Type classes}  When discussing type class systems, there are
-several properties that one may talk about.
-A set of instances is \emph{confluent} if, no matter what order
-constraint solving is performed, GHC will terminate with a canonical set
-of constraints that must be satisfied for any given use of a type class.
-In other words, confluence says that we won't conclude that a program
-doesn't type check just because we swapped in a different constraint
-solving algorithm.
-
-Confluence's closely related twin is \emph{coherence} (defined in ``Type
-classes: exploring the design space''). This property states that
-``every different valid typing derivation of a program leads to a
-resulting program that has the same dynamic semantics.''  Why could
-differing typing derivations result in different dynamic semantics?  The
-answer is that context reduction, which picks out type class instances,
-elaborates into concrete choices of dictionaries in the generated code.
-Confluence is a prerequisite for coherence, since one
-can hardly talk about the dynamic semantics of a program that doesn't
-type check.
-
-In the vernacular, confluence and coherence are often incorrectly used
-to refer to another related property: \emph{global uniqueness of instances},
-which states that in a fully compiled program, for any type, there is at most one
-instance resolution for a given type class.  Languages with local type
-class instances such as Scala generally do not have this property, and
-this assumption is frequently used for abstraction.
-
-So, what properties does GHC enforce, in practice?
-In the absence of any type system extensions, GHC's employs a set of
-rules (described in ``Exploring the design space'') to ensure that type
-class resolution is confluent and coherent.  Intuitively, it achieves
-this by having a very simple constraint solving algorithm (generate
-wanted constraints and solve wanted constraints) and then requiring the
-set of instances to be \emph{nonoverlapping}, ensuring there is only
-ever one way to solve a wanted constraint.  Overlap is a
-more stringent restriction than either confluence or coherence, and
-via the \verb|OverlappingInstances| and \verb|IncoherentInstances|, GHC
-allows a user to relax this restriction ``if they know what they're doing.''
-
-Surprisingly, however, GHC does \emph{not} enforce global uniqueness of
-instances.  Imported instances are not checked for overlap until we
-attempt to use them for instance resolution.  Consider the following program:
-
-\begin{verbatim}
--- T.hs
-data T = T
--- A.hs
-import T
-instance Eq T where
--- B.hs
-import T
-instance Eq T where
--- C.hs
-import A
-import B
-\end{verbatim}
-
-When compiled with one-shot compilation, \verb|C| will not report
-overlapping instances unless we actually attempt to use the \verb|Eq|
-instance in C.\footnote{When using batch compilation, GHC reuses the
-    instance database and is actually able to detect the duplicated
-    instance when compiling B.  But if you run it again, recompilation
-avoidance skips A, and it finishes compiling!  See this bug:
-\url{https://ghc.haskell.org/trac/ghc/ticket/5316}}  This is by
-design\footnote{\url{https://ghc.haskell.org/trac/ghc/ticket/2356}}:
-ensuring that there are no overlapping instances eagerly requires
-eagerly reading all the interface files a module may depend on.
-
-We might summarize these three properties in the following manner.
-Culturally, the Haskell community expects \emph{global uniqueness of instances}
-to hold: the implicit global database of instances should be
-confluent and coherent.  GHC, however, does not enforce uniqueness of
-instances: instead, it merely guarantees that the \emph{subset} of the
-instance database it uses when it compiles any given module is confluent and coherent.  GHC does do some
-tests when an instance is declared to see if it would result in overlap
-with visible instances, but the check is by no means
-perfect\footnote{\url{https://ghc.haskell.org/trac/ghc/ticket/9288}};
-truly, \emph{type-class constraint resolution} has the final word.  One
-mitigating factor is that in the absence of \emph{orphan instances}, GHC is
-guaranteed to eagerly notice when the instance database has overlap.\footnote{Assuming that the instance declaration checks actually worked\ldots}
-
-Clearly, the fact that GHC's lazy behavior is surprising to most
-Haskellers means that the lazy check is mostly good enough: a user
-is likely to discover overlapping instances one way or another.
-However, it is relatively simple to construct example programs which
-violate global uniqueness of instances in an observable way:
-
-\begin{verbatim}
--- A.hs
-module A where
-data U = X | Y deriving (Eq, Show)
-
--- B.hs
-module B where
-import Data.Set
-import A
-
-instance Ord U where
-compare X X = EQ
-compare X Y = LT
-compare Y X = GT
-compare Y Y = EQ
-
-ins :: U -> Set U -> Set U
-ins = insert
-
--- C.hs
-module C where
-import Data.Set
-import A
-
-instance Ord U where
-compare X X = EQ
-compare X Y = GT
-compare Y X = LT
-compare Y Y = EQ
-
-ins' :: U -> Set U -> Set U
-ins' = insert
-
--- D.hs
-module Main where
-import Data.Set
-import A
-import B
-import C
-
-test :: Set U
-test = ins' X $ ins X $ ins Y $ empty
-
-main :: IO ()
-main = print test
-
--- OUTPUT
-$ ghc -Wall -XSafe -fforce-recomp --make D.hs
-[1 of 4] Compiling A ( A.hs, A.o )
-[2 of 4] Compiling B ( B.hs, B.o )
-
-B.hs:5:10: Warning: Orphan instance: instance [safe] Ord U
-[3 of 4] Compiling C ( C.hs, C.o )
-
-C.hs:5:10: Warning: Orphan instance: instance [safe] Ord U
-[4 of 4] Compiling Main ( D.hs, D.o )
-Linking D ...
-$ ./D
-fromList [X,Y,X]
-\end{verbatim}
-
-Locally, all type class resolution was coherent: in the subset of
-instances each module had visible, type class resolution could be done
-unambiguously.  Furthermore, the types of \verb|ins| and \verb|ins'|
-discharge type class resolution, so that in \verb|D| when the database
-is now overlapping, no resolution occurs, so the error is never found.
-
-It is easy to dismiss this example as an implementation wart in GHC, and
-continue pretending that global uniqueness of instances holds.  However,
-the problem with \emph{global uniqueness of instances} is that they are
-inherently nonmodular: you might find yourself unable to compose two
-components because they accidentally defined the same type class
-instance, even though these instances are plumbed deep in the
-implementation details of the components.
-
-As it turns out, there is already another feature in Haskell which
-must enforce global uniqueness, to prevent segfaults.
-We now turn to type classes' close cousin: type families.
-
-\paragraph{Type families}  With type families, confluence is the primary
-property of interest.  (Coherence is not of much interest because type
-families are elaborated into coercions, which don't have any
-computational content.)  Rather than considering what the set of
-constraints we reduce to, confluence for type families considers the
-reduction of type families.  The overlap checks for type families
-can be quite sophisticated, especially in the case of closed type
-families.
-
-Unlike type classes, however, GHC \emph{does} check the non-overlap
-of type families eagerly.  The analogous program does \emph{not} type check:
-
-\begin{verbatim}
--- F.hs
-type family F a :: *
--- A.hs
-import F
-type instance F Bool = Int
--- B.hs
-import F
-type instance F Bool = Bool
--- C.hs
-import A
-import B
-\end{verbatim}
-
-The reason is that it is \emph{unsound} to ever allow any overlap
-(unlike in the case of type classes where it just leads to incoherence.)
-Thus, whereas one might imagine dropping the global uniqueness of instances
-invariant for type classes, it is absolutely necessary to perform global
-enforcement here.  There's no way around it!
-
-\subsection{Local type classes}
-
-Here, we say \textbf{NO} to global uniqueness.
-
-This design is perhaps best discussed in relation to modular type
-classes, which shares many similar properties.  Instances are now
-treated as first class objects (in MTCs, they are simply modules)---we
-may explicitly hide or include instances for type class resolution (in
-MTCs, this is done via the \verb|using| top-level declaration).  This is
-essentially what was sketched in Section 5 of the original Backpack
-paper.  As a simple example:
-
-\begin{verbatim}
-package p where
-    A :: [ data T = T ]
-    B = [ import A; instance Eq T where ... ]
-
-package q where
-    A = [ data T = T; instance Eq T where ... ]
-    include p
-\end{verbatim}
-
-Here, \verb|B| does not see the extra instance declared by \verb|A|,
-because it was thinned from its signature of \verb|A| (and thus never
-declared canonical.)  To declare an instance without making it
-canonical, it must placed in a separate (unimported) module.
-
-Like modular type classes, Backpack does not give rise to incoherence,
-because instance visibility can only be changed at the top level module
-language, where it is already considered best practice to provide
-explicit signatures.  Here is the example used in the Modular Type
-Classes paper to demonstrate the problem:
-
-\begin{verbatim}
-structure A = using EqInt1 in
-    struct ...fun f x = eq(x,x)... end
-structure B = using EqInt2 in
-    struct ...val y = A.f(3)... end
-\end{verbatim}
-
-Is the type of f \verb|int -> bool|, or does it have a type-class
-constraint?  Because type checking proceeds over the entire program, ML
-could hypothetically pick either.  However, ported to Haskell, the
-example looks like this:
-
-\begin{verbatim}
-EqInt1 :: [ instance Eq Int ]
-EqInt2 :: [ instance Eq Int ]
-A = [
-    import EqInt1
-    f x = x == x
-]
-B = [
-    import EqInt2
-    import A hiding (instance Eq Int)
-    y = f 3
-]
-\end{verbatim}
-
-There may be ambiguity, yes, but it can be easily resolved by the
-addition of a top-level type signature to \verb|f|, which is considered
-best-practice anyway.  Additionally, Haskell users are trained to expect
-a particular inference for \verb|f| in any case (the polymorphic one).
-
-Here is another example which might be considered surprising:
-
-\begin{verbatim}
-package p where
-    A :: [ data T = T ]
-    B :: [ data T = T ]
-    C = [
-        import qualified A
-        import qualified B
-        instance Show A.T where show T = "A"
-        instance Show B.T where show T = "B"
-        x :: String
-        x = show A.T ++ show B.T
-    ]
-\end{verbatim}
-
-In the original Backpack paper, it was implied that module \verb|C|
-should not type check if \verb|A.T = B.T| (failing at link time).
-However, if we set aside, for a moment, the issue that anyone who
-imports \verb|C| in such a context will now have overlapping instances,
-there is no reason in principle why the module itself should be
-problematic.  Here is the example in MTCs, which I have good word from
-Derek does type check.
-
-\begin{verbatim}
-signature SIG = sig
-    type t
-    val mk : t
-end
-signature SHOW = sig
-    type t
-    val show : t -> string
-end
-functor Example (A : SIG) (B : SIG) =
-    let structure ShowA : SHOW = struct
-        type t = A.t
-        fun show _ = "A"
-    end in
-    let structure ShowB : SHOW = struct
-        type t = B.t
-        fun show _ = "B"
-    end in
-    using ShowA, ShowB in
-    struct
-        val x = show A.mk ++ show B.mk
-    end : sig val x : string end
-\end{verbatim}
-
-The moral of the story is, even though in a later context the instances
-are overlapping, inside the functor, the type-class resolution is unambiguous
-and should be done (so \verb|x = "AB"|).
-
-Up until this point, we've argued why MTCs and this Backpack design are similar.
-However, there is an important sociological difference between modular type-classes
-and this proposed scheme for Backpack.  In the presentation ``Why Applicative
-Functors Matter'', Derek mentions the canonical example of defining a set:
-
-\begin{verbatim}
-signature ORD = sig type t; val cmp : t -> t -> bool end
-signature SET = sig type t; type elem;
-    val empty : t;
-    val insert : elem -> t -> t ...
-end
-functor MkSet (X : ORD) :> SET where type elem = X.t
-  = struct ... end
-\end{verbatim}
-
-This is actually very different from how sets tend to be defined in
-Haskell today.  If we directly encoded this in Backpack, it would
-look like this:
-
-\begin{verbatim}
-package mk-set where
-    X :: [
-        data T
-        cmp :: T -> T-> Bool
-    ]
-    Set :: [
-        data Set
-        empty :: Set
-        insert :: T -> Set -> Set
-    ]
-    Set = [
-        import X
-        ...
-    ]
-\end{verbatim}
-
-It's also informative to consider how MTCs would encode set as it is written
-today in Haskell:
-
-\begin{verbatim}
-signature ORD = sig type t; val cmp : t -> t -> bool end
-signature SET = sig type 'a t;
-    val empty : 'a t;
-    val insert : (X : ORD) => X.t -> X.t t -> X.t t
-end
-struct MkSet :> SET = struct ... end
-\end{verbatim}
-
-Here, it is clear to see that while functor instantiation occurs for
-implementation, it is not occuring for types.  This is a big limitation
-with the Haskell approach, and it explains why Haskellers, in practice,
-find global uniqueness of instances so desirable.
-
-Implementation-wise, this requires some subtle modifications to how we
-do type class resolution.  Type checking of indefinite modules works as
-before, but when go to actually compile them against explicit
-implementations, we need to ``forget'' that two types are equal when
-doing instance resolution.  This could probably be implemented by
-associating type class instances with the original name that was
-utilized when typechecking, so that we can resolve ambiguous matches
-against types which have the same original name now that we are
-compiling.
-
-As we've mentioned previously, this strategy is unsound for type families.
-
-\subsection{Globally unique}
-
-Here, we say \textbf{YES} to global uniqueness.
-
-When we require the global uniqueness of instances (either because
-that's the type class design we chose, or because we're considering
-the problem of type families), we will need to reject declarations like the
-one cited above when \verb|A.T = B.T|:
-
-\begin{verbatim}
-A :: [ data T ]
-B :: [ data T ]
-C :: [
-    import qualified A
-    import qualified B
-    instance Show A.T where show T = "A"
-    instance Show B.T where show T = "B"
-]
-\end{verbatim}
-
-The paper mentions that a link-time check is sufficient to prevent this
-case from arising.  While in the previous section, we've argued why this
-is actually unnecessary when local instances are allowed, the link-time
-check is a good match in the case of global instances, because any
-instance \emph{must} be declared in the signature.  The scheme proceeds
-as follows: when some instances are typechecked initially, we type check
-them as if all of variable module identities were distinct.  Then, when
-we perform linking (we \verb|include| or we unify some module
-identities), we check again if to see if we've discovered some instance
-overlap.  This linking check is akin to the eager check that is
-performed today for type families; it would need to be implemented for
-type classes as well: however, there is a twist: we are \emph{redoing}
-the overlap check now that some identities have been unified.
-
-As an implementation trick, one could deferring the check until \verb|C|
-is compiled, keeping in line with GHC's lazy ``don't check for overlap
-until the use site.''  (Once again, unsound for type families.)
-
-\paragraph{What about module inequalities?}  An older proposal was for
-signatures to contain ``module inequalities'', i.e., assertions that two
-modules are not equal.  (Technically: we need to be able to apply this
-assertion to $\beta$ module variables, since \verb|A != B| while
-\verb|A.T = B.T|).  Currently, Edward thinks that module inequalities
-are only marginal utility with local instances (i.e., not enough to
-justify the implementation cost) and not useful at all in the world of
-global instances!
-
-With local instances, module inequalities could be useful to statically
-rule out examples like \verb|show A.T ++ show B.T|.  Because such uses
-are not necessarily reflected in the signature, it would be a violation
-of separate module development to try to divine the constraint from the
-implementation itself.  I claim this is of limited utility, however, because,
-as we mentioned earlier, we can compile these ``incoherent'' modules perfectly
-coherently.  With global instances, all instances must be in the signature, so
-while it might be aesthetically displeasing to have the signature impose
-extra restrictions on linking identities, we can carry this out without
-violating the linking restriction.
-
-\subsection{Orphans}
-
-Controlling instance visibility via signature problems poses an implementation
-challenge similar to that of orphan instances.  To describe this problem,
-we first have to describe how instance resolution works for orphans and
-non-orphans in GHC today.
-
-Type information for already compiled code in other packages is cached
-on disk using interface files.  For efficiency reasons, it's desirable to
-avoid loading interface file until absolutely necessary: if we don't
-use any of the identifiers for a file, it should not be necessary to
-load the interface.  Among other things, type class instances are stored
-in interface files.
-
-Signatures and hs-boot files notwithstanding, non-orphan instance
-resolution is achieved through a (somewhat) astonishing coincidence: at
-the point when a type class is resolved, we are guaranteed to have
-loaded the interfaces for all of the names involved in the type class
-instantiation.  This means that if there is a type class, we will have
-seen it; conversely, it means that non-orphan instances are a closed
-world: if we load all these interfaces and see no non-orphan instance,
-we know there never be a non-orphan instance.
-
-Things are a bit worse for orphans: these instances are an open world,
-and so the only way to tell if an orphan instance is in scope is by consulting
-the transitive closure of module imports.
-
-\section{Bits and bobs}
-
-\subsection{Abstract type synonyms}
-
-In Paper Backpack, abstract type synonyms are not permitted, because GHC doesn't
-understand how to deal with them.  The purpose of this section is to describe
-one particularly nastiness of abstract type synonyms, by way of the occurs check:
-
-\begin{verbatim}
-A :: [ type T ]
-B :: [ import qualified A; type T = [A.T] ]
-\end{verbatim}
-
-At this point, it is illegal for \verb|A = B|, otherwise this type synonym would
-fail the occurs check.  This seems like pretty bad news, since every instance
-of the occurs check in the type-checker could constitute a module inequality.
-
-\section{Open questions}\label{sec:open-questions}
-
-Here are open problems about the implementation which still require
-hashing out.
-
-\begin{itemize}
-
-    \item In Section~\ref{sec:simplifying-backpack}, we argued that we
-        could implement Backpack without needing a shaping pass. We're
-        pretty certain that this will work for typechecking and
-        compiling fully definite packages with no recursive linking, but
-        in Section~\ref{sec:typechecking-indefinite}, we described some
-        of the prevailing difficulties of supporting signature linking.
-        Renaming is not an insurmountable problem, but backwards flow of
-        shaping information can be, and it is unclear how best to
-        accommodate this.  This is probably the most important problem
-        to overcome.
-
-    \item In Section~\ref{sec:installing-indefinite}, a few choices for how to
-        store source code were pitched, however, there is not consensus on which
-        one is best.
-
-    \item What is the impact of the multiplicity of PackageIds on
-        dependency solving in Cabal?  Old questions of what to prefer
-        when multiple package-versions are available (Cabal originally
-        only needed to solve this between different versions of the same
-        package, preferring the oldest version), but with signatures,
-        there are more choices.  Should there be a complex solver that
-        does all signature solving, or a preprocessing step that puts
-        things back into the original Cabal version.  Authors may want
-        to suggest policy for what packages should actually link against
-        signatures (so a crypto library doesn't accidentally link
-        against a null cipher package).
-
-\end{itemize}
-
-\end{document}
diff --git a/docs/backpack/backpack-manual.tex b/docs/backpack/backpack-manual.tex
deleted file mode 100644
index 658df1badc..0000000000
--- a/docs/backpack/backpack-manual.tex
+++ /dev/null
@@ -1,623 +0,0 @@
-\documentclass{article}
-
-\usepackage{color}
-\usepackage{fullpage}
-\usepackage{hyperref}
-
-\newcommand{\Red}[1]{{\color{red} #1}}
-
-\title{The Backpack Manual}
-
-\begin{document}
-
-\maketitle
-
-Backpack is a new module system for Haskell, intended to enable
-``separate modular development'', where application-writers depend on
-libraries by programming against abstract interfaces instead of specific
-implementations.  Our goal is to reduce software coupling, and let the
-type system and compiler assist developers when they are developing
-large software systems.  Backpack was originally described in a POPL'14
-paper \url{http://plv.mpi-sws.org/backpack/}, but this document is
-intended to describe the syntax of a language you might actually be able
-to \emph{write}, i.e., from the perspective of a software developer.
-
-\paragraph{Examples of Backpack ``in the large''}
-In the standard practice of large-scale software development today,
-users organize code into libraries.  Here is a very simple example of
-some Haskell code structured in this way:
-
-\begin{verbatim}
-unit p where
-    module A where
-        x = True
-        y = False
-
-unit q where
-    include p
-    module B where
-        import A
-        b = x
-\end{verbatim}
-
-\verb|p| is a reusable unit (or package/library if you like) which
-provides a single module \verb|A|.  \verb|q| depends on \verb|p| by
-directly including it, bringing all of the modules of \verb|p| into scope for
-import.
-
-There is a downside to writing code this way: without editing your
-source code, you can't actually swap out \verb|p| with another version
-(maybe \verb|p-2.0|, or perhaps even a version of \verb|p| written by someone else).
-Traditionally, this is overcome by relying on an extralinguistic mechanism,
-the \emph{package manager}, which indirects \verb|include p| so that
-it can refer to some other piece of code.
-
-Backpack offers a different, in-language way of expressing dependency
-without committing to an implementation:
-
-\begin{verbatim}
-unit q where
-    require p
-    module B where
-        import A
-        b = x
-\end{verbatim}
-
-Or, equivalently:
-
-\begin{verbatim}
-unit p-interface where
-    signature A where
-        x :: Bool
-        y :: Bool
-unit q where
-    include p-interface
-    module B where
-        import A
-        b = x
-\end{verbatim}
-
-With the \verb|require| keyword, Backpack automatically computes
-\verb|p-interface|, which expresses the abstract interface of \verb|p|.
-\verb|q| utilizes a subset of this interface (unused requirements
-don't ``count''), resulting in this final version of \verb|q|:
-
-\begin{verbatim}
-unit q where
-    signature A where
-        x :: Bool
-    module B where
-        import A
-        b = x
-\end{verbatim}
-
-The technical innovation of Backpack is that the indefinite version of \verb|q|, which
-does not depend on a specific implementation of \verb|p|, still composes
-naturally and in the \emph{same} way that the definite version of
-\verb|q|.  That is to say, you can take a hierarchy of libraries that \verb|include| one
-another (today's situation) and replace each \verb|include| with a
-\verb|require|. The result is a reusable set of components with
-explicitly defined requirements.  If the inferred requirements are not
-general enough, a signature can be written explicitly.
-
-Finally, the package manager serves a new role: it can be used to select
-a combination of components which fulfill all the requirements.  Unlike
-dependency resolution with version numbers, with interfaces the package
-manager can do this \emph{completely} precisely.
-
-\paragraph{Examples of Backpack ``in the small''}
-Although Backpack was originally designed for library-scale development,
-it can also be used for small-scale modular development,
-similar to ML modules.  Here is a simple example of writing an
-associated list implementation that is parametrized over the key:
-
-\begin{verbatim}
-    unit assoc-map where
-        signature H where
-            data T
-            eq :: T -> T -> Bool
-        module Assoc where
-            import H
-            mylookup :: T -> [(T, a)] -> Maybe a
-            mylookup x xs = fmap snd (find (eq x) xs)
-    unit main where
-        module AbsInt where
-            type T = Int
-            eq x y = abs x == abs y
-        include assoc-map (Assoc as AbsIntAssoc) requires (T as AbsInt)
-        module Main where
-            import AbsIntAssoc
-            import Prelude
-            main = print (mylookup -1 [(1,"yes"),(-2,"no")])
-\end{verbatim}
-
-For example, in Haskell there are many different kinds of ``string''-like
-data types: \verb|String| (a linked list of characters), \verb|ByteString|
-(an unstructured raw bytestring) and \verb|Text| (a UTF-8 encoded bytestring).
-Many libraries, e.g., parsers, need to work on any string-like input which
-a user might want to give them.
-
-A more full example of a Backpack version of some real library
-code can be found in Appendix~\ref{sec:tagstream-example}.
-
-
-
-\section{The Backpack file}
-
-\begin{verbatim}
-packages ::= "{" package_0 ";" ... ";" package_n "}"
-\end{verbatim}
-
-A Backpack file consists of a list of named packages.
-All packages in a Backpack file live in the global namespace.
-A package defines a collection of modules, exporting some of
-these modules so that other modules can make use of them via
-\emph{include}.  You can compile a definite package \verb|p| in a Backpack file \verb|foo.bkp|
-with \verb|ghc --backpack foo.bkp p|; you can type-check an indefinite package by
-adding \verb|-fno-code|.
-
-\Red{ToDo: How do you import an external Backpack file?}
-
-\Red{ToDo: Facility for private packages.}
-
-\begin{verbatim}
-package ::= "package" pkgname [pkgexports] "where" pkgbody
-pkgname ::= /* package name, e.g. containers (no version!) */
-pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
-\end{verbatim}
-
-A package begins with the keyword \verb|package|, its name, and an
-optional export specification (e.g., a list of modules to be exposed).
-The header is followed a list of declarations which define modules,
-signatures and include other packages.
-
-\section{Declarations}
-
-\begin{verbatim}
-pkgdecl ::= "module"    modid [exports] "where" body
-          | "signature" modid [exports] "where" body
-          | "include"   pkgname ["as" pkgname] [inclspec]
-\end{verbatim}
-
-A package is made up of package declarations, which either introduce a
-new module implementation, introduces a new module
-signature, or includes a package from the package environment.
-The declaration of modules and signatures is exactly as it is in Haskell98,
-so we don't reprise the grammar here.
-
-\Red{ToDo: Clarify whether order matters.  Both are valid designs, but I think order-less is more user-friendly.}
-
-We generally don't expect users to place their module source code
-in package files; thus we provide the following forms to refer to
-\verb|hs| and \verb|hsig| files living on the file-system:
-
-\begin{verbatim}
-pkgdecl ::= "module"    modid_0 "=" path_0 "," ... "," modid_n "=" path_n
-          | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
-          | "module"    modid_0 "," ... "," modid_n
-          | "signature" modid_0 "," ... "," modid_n
-\end{verbatim}
-
-Thus, \verb|module A = "A.hs"| defines the body of \verb|A| based
-on the contents of \verb|A.hs| in the package's source directory.
-When the assignment is omitted, we implicitly refer to the file path
-created by replacing periods with directory separators and adding
-an appropriate file extension (thus, we can also write \verb|module A|).
-
-\begin{verbatim}
-pkgdecl ::= "source" path
-\end{verbatim}
-
-The \verb|source| keyword is another construct which allows us to
-define modules by simply scanning the path in question.  For example,
-if \verb|src| contains two files, \verb|A.hs| and \verb|B.hsig|,
-then ``\verb|source "src"|'' is equivalent to
-``\verb|module A = "src/A.hs"; signature B = "src/B.hsig"|''.
-
-\Red{ToDo: Allow defining package-wide module imports, which propagate to all inline
-modules and signatures.}
-
-\Red{ToDo: Allow defining anonymous modules with bare type/expression declarations.}
-
-\section{Signatures}
-
-A signature, denoted with \verb|signature| in a Backpack file and a file
-with the \verb|hsig| extension on the file system, represents a (type) signature for a
-Haskell module. It can contain type signatures, data declarations, type
-classes, type class instances and reexports, but it cannot contain any
-value definitions.\footnote{Signatures are the backbone of the Backpack
-module system.  A signature can be used to type-check client code which
-uses a module (without the module implementation), or to verify that an
-implementation upholds some signature (without a client
-implementation.)} Signatures are essentially
-\texttt{hs-boot} modules which do not support mutual recursion but
-have no runtime efficiency cost.  Here is an example of a module signature
-representing an abstract map type:
-
-\begin{verbatim}
-module Map where
-    type role Map nominal representational
-    data Map k v
-    instance Functor (Map k)
-    empty :: Map k a
-\end{verbatim}
-
-\section{Includes and exports}
-
-\begin{verbatim}
-pkgdecl  ::= "include" pkgname ["as" pkgname] [inclspec]
-
-inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
-             [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
-
-renaming ::= modid [ "as" modid ]
-           | "package" pkgname
-\end{verbatim}
-
-% Add me later:
-%          | "hiding" "(" modid_0 "," ... "," modid_n [","] ")"
-
-An include brings the modules and signatures of a package into scope.
-If these modules/signatures have the same names as other
-modules/signatures in scope, \emph{mix-in linking} occurs.
-In particular:
-
-\begin{itemize}
-    \item Module + module = error (unless they really are the same!)
-    \item Module + signature = the signature is filled in, and is
-        no longer part of the requirements of the package.
-    \item Signature + signature = the signatures are merged together.
-\end{itemize}
-
-An include is associated with an optional \verb|inclspec|,
-which can be to thin the provided modules and rename the provided and
-required modules of an include.  In its simplest mode of use,
-an \verb|inclspec| is a list of modules to be brought into scope,
-e.g. \verb|include p (A, B)|.  Requirements cannot be hidden, but
-they can be renamed to provide an implementation (or even to just
-reexport the requirement under another name.)  If a requirement is
-not mentioned in an explicit requirements list, it is implicitly included
-(thus, \verb|requires (Hole)| has only a purely documentary effect).
-It is not valid to rename a provision to a requirement, or a requirement
-to a provision.
-
-\begin{verbatim}
-pkgexports ::= inclspec
-\end{verbatim}
-
-An export, symmetrically, specifies what modules a package will bring
-into scope if it is included without any \verb|inclspec|.  Any module
-which is omitted from an explicit export list is not exposed (however,
-like before, requirements cannot be hidden.)
-
-When an explicit export list is omitted, you can calculate the provides
-and requires of a package as follows:
-
-\begin{itemize}
-    \item A package provides any non-included modules and signatures.
-        (It only provides an included module/signature if it is explicitly
-        reexported.)
-    \item A package requires any transitively reachable signatures or
-        hole signatures which are not filled in with an implementation.
-\end{itemize}
-
-\Red{ToDo: Properly describe ``hole signatures'' in the declarations section}
-
-\subsection{Requirements}
-
-The fact that requirements are \emph{implicitly} propagated from package
-to package can result in some spooky ``action at a distance''. However,
-this implicit behavior is one of the key ingredients to making mix-in
-modular development scale: you don't want to have to explicitly link
-everything up, as you might have to do in a traditional ML module
-system.
-
-You cannot, however, import a requirement, unless it is also provided,
-which helps increase encapsulation.  If a package provides a
-module, it can be imported:
-
-\begin{verbatim}
-package p (A) requires (A) where
-    signature A where
-        x :: Bool
-package q (B) requires (A) where
-    include p
-    module B where
-        import A    -- OK
-\end{verbatim}
-
-If it does not, it cannot be imported:
-\Red{Alternately, the import is OK but doesn't result in any identifiers
-being brought into scope.}
-
-\begin{verbatim}
-package p () requires (A) where -- yes, this is kind of pointless
-    signature A where
-        x :: Bool
-package q (B) requires (A) where
-    include p
-    module B where
-        import A    -- ERROR!
-\end{verbatim}
-
-This means that it is always safe for a package to remove requirements
-or weaken holes; clients will always continue to compile.
-
-Of course, if there is a different signature for the hole in scope, the
-import is not an error; however, no declarations from \verb|p| are in scope:
-
-\begin{verbatim}
-package p () requires (A) where
-    signature A where
-        x :: Bool
-package q (B) requires (A) where
-    include p
-    signature A where
-        y :: Bool
-    module B where
-        import A
-        x' = x      -- ERROR!
-        y' = y      -- OK
-\end{verbatim}
-
-To summarize, requirements are part of the interface of a package; however,
-they provide no identifiers as far as imports are concerned.  \Red{There is
-some subtle interaction with requirements and shaping; see Shaping by example
-for more details.}
-
-\subsection{Package includes/exports}
-
-A package export is easy enough to explain by analogy of module exports
-in Haskell: a \verb|package p| in an export list explicitly reexports
-the identifiers from that package; whereas even a default, wildcard export
-list would only export locally defined identifiers/modules.
-
-For example, this module exports the modules of both \verb|base|
-and \verb|array|.
-
-\begin{verbatim}
-package combined(package base, package array) where
-    include base
-    include array
-\end{verbatim}
-
-However, in Backpack, a package may be included multiple times, making
-such declarations ambiguous.  Thus, a package can be included as a local
-package name to disambiguate:
-
-\begin{verbatim}
-package p(package q1) where         -- equivalent to B1
-    include impls (A1, A2)
-    include q as q1 (hole A as A1, B as B1)
-    include q as q2 (hole A as A2, B as B2)
-\end{verbatim}
-
-A package include, e.g. \verb|include a (package p)| is only valid if
-\verb|a| exports the package \verb|p| explicitly.\footnote{It's probably
-possible to use anonymous packages to allow easily dividing a package
-into subpackages, but this is silly and you can always just put it
-in an actual package.}
-
-\section{(Transparent) signature ascription}
-
-\begin{verbatim}
-inclspec ::= ...
-           | "::" pkgexp
-
-pkgexp ::= pkgname
-         | "package" [exports] "where" pkgbody
-\end{verbatim}
-
-Signature ascription subsumes thinning: it narrows the exports
-of modules in a package to those specified by a signature
-package. This package \verb|pkgexp| is specified with either
-a reference to a named package or an \emph{anonymous package}
-(in prior work, these have been referred to as \emph{units},
-although here the distinction is not necessary as our system
-is \emph{purely applicative}).
-
-Ascription also imposes a \emph{requirement} on the package
-being abscribed.  Suppose you have \verb|p :: psig|, then:
-
-\begin{itemize}
-    \item Everything provided \verb|psig| must also
-    be provided by \verb|p|.
-    \item Everything required by \verb|p| must also
-    be required by \verb|psig|.
-\end{itemize}
-
-\Red{Alternately, the second requirement is not necessary, and you
-calculate the new requirements by taking the requirements of \texttt{psig},
-removing the provides of \texttt{p}, and then adding the requirements of \texttt{p}.
-This makes it possible to ascribe includes for \emph{adapter} packages, which
-provide some modules given a different set of requirements.}
-
-Semantically, ascription replaces the module with a signature,
-type-checks the package against the signature, and then \emph{post
-facto} links the signature against the implementation.
-An ascribed include can be replaced with the signature
-it is ascribed with, resulting in a package which still typechecks
-but has more holes.  \Red{You have to link at the VERY END, because
-if you link immediately after processing the module with the
-ascribed include, the module identities will leak.  Of course, if
-we're compiling we just link eagerly.  But now this means that
-if you have a definite package which uses ascription, even assuming
-all packages in the environment type-check, you must still type-check
-this package twice, once indefinitely and then with the actual
-linking relationship.}
-
-For example, ascription in the export specification thins out all
-private identifiers from the package:
-
-\begin{verbatim}
-    package psig where
-        signature A where
-            public :: Bool
-    package p :: psig where
-        module A.Internal where
-            not_exported = 0
-        module A where
-            public = True
-            private = False
-\end{verbatim}
-
-and, symmetrically, ascription in an include hides identifiers:
-
-\begin{verbatim}
-    package psig where
-        signature A where
-            public :: Bool
-    package p where
-        module A where
-            public = True
-            private = False
-    package q where
-        include p :: psig
-        module B where
-            import A
-            ... public ...  -- OK
-            ... private ... -- ERROR
-\end{verbatim}
-
-\Red{Observation: thinning is subsumed by transparent signature ascription, but NOT renaming.  Thus RENAMING does not commute across signature ascription; you must do it either before or after.  Syntax for this is tricky.}
-
-\paragraph{Syntactic sugar for anonymous packages}
-
-\begin{verbatim}
-pkgexp ::= pkgbody
-         | path
-\end{verbatim}
-
-It may be useful to provide two forms of sugar for specifying anonymous packages:
-\verb|pkgbody| is equivalent to \verb|package where pkgbody|; and \verb|"path"|
-is equivalent to \verb|package where source "path"|.
-
-\appendix
-\section{Full grammar}
-
-\begin{verbatim}
-packages ::= "{" package_0 ";" ... ";" package_n "}"
-
-package ::= "package" pkgname [pkgexports] "where" pkgbody
-pkgname ::= /* package name, e.g. containers (no version!) */
-pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
-
-pkgdecl ::= "module"    modid [exports] "where" body
-          | "signature" modid [exports] "where" body
-          | "include"   pkgname ["as" pkgname] [inclspec]
-          | "module"    modid_0 "=" path_0 "," ... "," modid_n "=" path_n
-          | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
-          | "module"    modid_0 "," ... "," modid_n
-          | "signature" modid_0 "," ... "," modid_n
-          | "source" path
-
-inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
-             [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
-           | "::" pkgexp
-pkgexports ::= inclspec
-
-renaming ::= modid [ "as" modid ]
-           | "package" pkgname
-
-pkgexp ::= pkgname
-         | "package" [exports] "where" pkgbody
-         | pkgbody
-         | path
-\end{verbatim}
-
-\newpage
-\label{sec:tagstream-example}
-\section{\texttt{tagstream-conduit} example}
-
-When someone recently asked on Haskell Reddit what the ``precise problem Backpack
-addresses'' was, Chris Doner offered a nice example from the
-\verb|tagstream-conduit|.  The existing implementation, at \url{http://hackage.haskell.org/package/tagstream-conduit-0.5.5.1/docs/Text-HTML-TagStream-Entities.html}, uses a data type
-to define a ``module'' which is then used to implement two modules in the
-library, a variant for \verb|ByteString| and a variant for \verb|Text|.
-
-Here is how this would be done in Backpack:
-
-\Red{This still contains some syntax which I haven't fully explained.}
-
-\begin{verbatim}
-    -- | This is an ordinary module which defines some types
-    -- which are exported by the package.
-    module Text.HTML.TagStream.Types where
-        data Token' s = Text s
-                      | ...
-
-    -- | This provides a 'Decoder' implementation for 'ByteString's.
-    -- We define 'Str' to be 'ByteString' and implement a few
-    -- functions manually, as well as reexport existing functions
-    -- from some libraries.  We don't plan to publically export
-    -- these from the package.
-    module Decoder.ByteString (
-        module Decoder.ByteString,
-        Builder, break, drop, uncons
-    ) where
-        import Data.ByteString
-        import Data.ByteString.Builder
-        type Str = ByteString
-        toStr = toByteString
-        fromStr = fromByteString
-        decodeEntity = ...
-
-    -- | This provides a 'Decoder' implementation for 'Text', much
-    -- the same as 'Decoder.ByteString'.
-    module Decoder.Text (
-        module Decoder.Text,
-        Builder, break, drop, uncons
-    ) where
-        import Data.Text
-        import Data.Text.Lazy.Builder
-        type Str = Text
-        toStr = toText
-        fromStr = fromText
-        decodeEntity = ...
-
-    -- | This defines the "functor"; the module implementing entity
-    -- decoding, 'Entities', is parametrized by an abstract interface
-    -- 'Decoder' which describes two types, 'Str' and 'Builder', as
-    -- well as operations on them which are avaiable for the implementation.
-    unit decoder where
-        signature Decoder where
-            data Str
-            data Builder
-            toStr :: Builder -> Str
-            break :: (Char -> Bool) -> Str -> (Str, Str)
-            fromStr :: Str -> Builder
-            drop :: Int -> Str -> Str
-            decodeEntity :: Str -> Maybe Str
-            uncons :: Str -> Maybe (Char, Str)
-        module Entities where
-            import Text.HTML.TagStream.Types
-            import Data.Conduit
-            import Decoder
-            decodeEntities :: Monad m => Conduit (Token' Str) m (Token' Str)
-            decodeEntities = ...
-
-    -- | Finally, these two lines instantiate 'Entities' twice;
-    -- once with 'Decoder.ByteString', and once as 'Decoder.Text'.
-    include decoder (Entities as Text.HTML.TagStream.ByteString)
-                    requires (Decoder as Decoder.ByteString)
-    include decoder (Entities as Text.HTML.TagStream.Text)
-                    requires (Decoder as Decoder.Text)
-\end{verbatim}
-
-Without having the source-code inline, the out-of-line Backpack file
-would look something like this:
-
-\begin{verbatim}
-    module Text.HTML.TagStream.Types -- Text/HTML/TagStream/Types.hs
-    module Decoder.ByteString        -- Decoder/ByteString.hs
-    module Decoder.Text              -- Decoder/Text.hs
-    unit decoder where
-        signature Decoder -- decoder/Decoder.hsig
-        module Entities   -- decoder/Entities.hs
-    include decoder (Entities as Text.HTML.TagStream.ByteString)
-                    requires (Decoder as Decoder.ByteString)
-    include decoder (Entities as Text.HTML.TagStream.Text)
-                    requires (Decoder as Decoder.Text)
-\end{verbatim}
-
-\end{document}
diff --git a/docs/backpack/commands-new-new.tex b/docs/backpack/commands-new-new.tex
deleted file mode 100644
index 1f2466e14c..0000000000
--- a/docs/backpack/commands-new-new.tex
+++ /dev/null
@@ -1,891 +0,0 @@
-%!TEX root = paper/paper.tex
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{amsthm}
-\usepackage{xspace}
-\usepackage{color}
-\usepackage{xifthen}
-\usepackage{graphicx}
-\usepackage{amsbsy}
-\usepackage{mathtools}
-\usepackage{stmaryrd}
-\usepackage{url}
-\usepackage{alltt}
-\usepackage{varwidth}
-% \usepackage{hyperref}
-\usepackage{datetime}
-\usepackage{subfig}
-\usepackage{array}
-\usepackage{multirow}
-\usepackage{xargs}
-\usepackage{marvosym} % for MVAt
-\usepackage{bm} % for blackboard bold semicolon
-
-
-%% HYPERREF COLORS
-\definecolor{darkred}{rgb}{.7,0,0}
-\definecolor{darkgreen}{rgb}{0,.5,0}
-\definecolor{darkblue}{rgb}{0,0,.5}
-% \hypersetup{
-%   linktoc=page,
-%   colorlinks=true,
-%   linkcolor=darkred,
-%   citecolor=darkgreen,
-%   urlcolor=darkblue,
-% }
-
-% Coloring
-\definecolor{hilite}{rgb}{0.7,0,0}
-\newcommand{\hilite}[1]{\color{hilite}#1\color{black}}
-\definecolor{shade}{rgb}{0.85,0.85,0.85}
-\newcommand{\shade}[1]{\colorbox{shade}{\!\ensuremath{#1}\!}}
-
-% Misc
-\newcommand\evalto{\hookrightarrow}
-\newcommand\elabto{\rightsquigarrow}
-\newcommand\elabtox[1]{\stackrel{#1}\rightsquigarrow}
-\newcommand{\yields}{\uparrow}
-\newcommand\too{\Rightarrow}
-\newcommand{\nil}{\cdot}
-\newcommand{\eps}{\epsilon}
-\newcommand{\Ups}{\Upsilon}
-\newcommand{\avoids}{\mathrel{\#}}
-
-\renewcommand{\vec}[1]{\overline{#1}}
-\newcommand{\rname}[1]{\textsc{#1}}
-\newcommand{\infrule}[3][]{%
-  \vspace{0.5ex}
-  \frac{\begin{array}{@{}c@{}}#2\end{array}}%
-       {\mbox{\ensuremath{#3}}}%
-  \ifthenelse{\isempty{#1}}%
-             {}%
-             % {\hspace{1ex}\rlap{(\rname{#1})}}%
-             {\hspace{1ex}(\rname{#1})}%
-  \vspace{0.5ex}
-}
-\newcommand{\infax}[2][]{\infrule[#1]{}{#2}}
-\newcommand{\andalso}{\hspace{.5cm}}
-\newcommand{\suchthat}{~\mathrm{s.t.}~}
-\newenvironment{notes}%
-  {\vspace{-1.5em}\begin{itemize}\setlength\itemsep{0pt}\small}%
-  {\end{itemize}}
-\newcommand{\macrodef}{\mathbin{\overset{\mathrm{def}}{=}}}
-\newcommand{\macroiff}{\mathbin{\overset{\mathrm{def}}{\Leftrightarrow}}}
-
-
-\newcommand{\ttt}[1]{\text{\tt #1}}
-\newcommand{\ttul}{\texttt{\char 95}}
-\newcommand{\ttcc}{\texttt{:\!:}}
-\newcommand{\ttlb}{{\tt {\char '173}}}
-\newcommand{\ttrb}{{\tt {\char '175}}}
-\newcommand{\tsf}[1]{\textsf{#1}}
-
-% \newcommand{\secref}[1]{\S\ref{sec:#1}}
-% \newcommand{\figref}[1]{Figure~\ref{fig:#1}}
-\newcommand{\marginnote}[1]{\marginpar[$\ast$ {\small #1} $\ast$]%
-                                      {$\ast$ {\small #1} $\ast$}}
-\newcommand{\hschange}{\marginnote{!Haskell}}
-\newcommand{\TODO}{\emph{TODO}\marginnote{TODO}}
-\newcommand{\parheader}[1]{\textbf{#1}\quad}
-
-\newcommand{\file}{\ensuremath{\mathit{file}}}
-\newcommand{\mapnil}{~\mathord{\not\mapsto}}
-
-\newcommand{\Ckey}[1]{\textbf{\textsf{#1}}}
-\newcommand{\Cent}[1]{\texttt{#1}}
-% \newcommand{\Cmod}[1]{\texttt{[#1]}}
-% \newcommand{\Csig}[1]{\texttt{[\ttcc{}#1]}}
-\newcommand{\Cmod}[1]{=\texttt{[#1]}}
-\newcommand{\Csig}[1]{~\ttcc{}~\texttt{[#1]}}
-\newcommand{\Cpath}[1]{\ensuremath{\mathsf{#1}}}
-\newcommand{\Cvar}[1]{\ensuremath{\mathsf{#1}}}
-\newcommand{\Ccb}[1]{\text{\ttlb} {#1} \text{\ttrb}}
-\newcommand{\Cpkg}[1]{\texttt{#1}}
-\newcommand{\Cmv}[1]{\ensuremath{\langle #1 \rangle}}
-\newcommand{\Cto}[2]{#1 \mapsto #2}
-\newcommand{\Ctoo}[2]{\Cpath{#1} \mapsto \Cpath{#2}}
-\newcommand{\Crm}[1]{#1 \mapnil}
-\newcommand{\Crmm}[1]{\Cpath{#1} \mapnil}
-\newcommand{\Cthin}[1]{\ensuremath{\langle \Ckey{only}~#1 \rangle}}
-\newcommand{\Cthinn}[1]{\ensuremath{\langle \Ckey{only}~\Cpath{#1} \rangle}}
-\newcommand{\Cinc}[1]{\Ckey{include}~{#1}}
-\newcommand{\Cincc}[1]{\Ckey{include}~\Cpkg{#1}}
-\newcommand{\Cshar}[2]{~\Ckey{where}~{#1} \equiv {#2}}
-\newcommand{\Csharr}[2]{~\Ckey{where}~\Cpath{#1} \equiv \Cpath{#2}}
-\newcommand{\Ctshar}[2]{~\Ckey{where}~{#1} \equiv {#2}}
-\newcommand{\Ctsharr}[3]{~\Ckey{where}~\Cpath{#1}.\Cent{#3} \equiv \Cpath{#2}.\Cent{#3}}
-\newcommand{\Cbinds}[1]{\left\{\!\begin{array}{l} #1 \end{array}\!\right\}}
-\newcommand{\Cbindsp}[1]{\left(\!\begin{array}{l} #1 \end{array}\!\right)}
-\newcommand{\Cpkgs}[1]{\[\begin{array}{l} #1\end{array}\]}
-\newcommand{\Cpkgsl}[1]{\noindent\ensuremath{\begin{array}{@{}l} #1\end{array}}}
-\newcommand{\Ccomment}[1]{\ttt{\emph{--~#1}}}
-\newcommand{\Cimp}[1]{\Ckey{import}~\Cpkg{#1}}
-\newcommand{\Cimpas}[2]{\Ckey{import}~\Cpkg{#1}~\Ckey{as}~\Cvar{#2}}
-
-\newcommand{\Ctbinds}[1]{\left\{\!\vrule width 0.6pt \begin{array}{l} #1 \end{array} \vrule width 0.6pt \!\right\}}
-\newcommand{\Ctbindsx}{\left\{\!\vrule width 0.6pt \; \vrule width 0.6pt \!\right\}}
-\newcommand{\Ctbindsxx}{\left\{\!\vrule width 0.6pt \begin{array}{l}\!\!\!\!\\\!\!\!\!\end{array} \vrule width 0.6pt \!\right\}}
-\newcommand{\Ctbindsxxx}{\left\{\!\vrule width 0.6pt \begin{array}{l}\!\!\!\!\\\!\!\!\!\\\!\!\!\!\end{array} \vrule width 0.6pt \!\right\}}
-
-
-\newcommand{\Cpkgdef}[2]{%
-  \ensuremath{
-  \begin{array}{l}
-  \Ckey{package}~\Cpkg{#1}~\Ckey{where}\\
-  \hspace{1em}\begin{array}{l}
-              #2
-              \end{array}
-  \end{array}}}
-\newcommand{\Cpkgdefonly}[3]{%
-  \ensuremath{
-  \begin{array}{l}
-  \Ckey{package}~\Cpkg{#1}\Cvar{(#2)}~\Ckey{where}\\
-  \hspace{1em}\begin{array}{l}
-              #3
-              \end{array}
-  \end{array}}}
-\newcommand{\Ccc}{\mathbin{\ttcc{}}}
-\newcommand{\Cbinmod}[2]{\Cvar{#1} = \texttt{[#2]}}
-\newcommand{\Cbinsig}[2]{\Cvar{#1} \Ccc \texttt{[#2]}}
-\newcommand{\Cinconly}[2]{\Ckey{include}~\Cpkg{#1}\Cvar{(#2)}}
-\newcommand{\Cimponly}[2]{\Ckey{import}~\Cpkg{#1}\Cvar{(#2)}}
-\newcommand{\Cimpmv}[3]{\Ckey{import}~\Cpkg{#1}\langle\Cvar{#2}\mapsto\Cvar{#3}\rangle}
-
-
-
-
-
-\newcommand{\oxb}[1]{\llbracket #1 \rrbracket}
-\newcommand{\coxb}[1]{\{\hspace{-.5ex}| #1 |\hspace{-.5ex}\}}
-\newcommand{\coxbv}[1]{\coxb{\vec{#1}}}
-\newcommand{\angb}[1]{\ensuremath{\boldsymbol\langle #1 \boldsymbol\rangle}\xspace}
-\newcommand{\angbv}[1]{\angb{\vec{#1}}}
-\newcommand{\aoxbl}{\ensuremath{\boldsymbol\langle\hspace{-.5ex}|}}
-\newcommand{\aoxbr}{\ensuremath{|\hspace{-.5ex}\boldsymbol\rangle}\xspace}
-\newcommand{\aoxb}[1]{\ensuremath{\aoxbl{#1}\aoxbr}}
-\newcommand{\aoxbv}[1]{\aoxb{\vec{#1}}}
-\newcommand{\poxb}[1]{\ensuremath{%
-  (\hspace{-.5ex}|%
-  #1%
-  |\hspace{-.5ex})}\xspace}
-\newcommand{\stof}[1]{{#1}^{\star}}
-% \newcommand{\stof}[1]{\ensuremath{\underline{#1}}}
-\newcommand{\sh}[1]{\ensuremath{\tilde{#1}}}
-
-
-% \newenvironment{code}[1][t]%
-%   {\ignorespaces\begin{varwidth}[#1]{\textwidth}\begin{alltt}}%
-%   {\end{alltt}\end{varwidth}\ignorespacesafterend}
-% \newenvironment{codel}[1][t]%
-%   {\noindent\begin{varwidth}[#1]{\textwidth}\noindent\begin{alltt}}%
-%   {\end{alltt}\end{varwidth}\ignorespacesafterend}
-
-
-%% hack for subfloats in subfig -------------
-\makeatletter
-\newbox\sf@box
-\newenvironment{SubFloat}[2][]%
-  {\def\sf@one{#1}%
-   \def\sf@two{#2}%
-   \setbox\sf@box\hbox
-   \bgroup}%
-  {\egroup
-   \ifx\@empty\sf@two\@empty\relax
-     \def\sf@two{\@empty}
-   \fi
-   \ifx\@empty\sf@one\@empty\relax
-     \subfloat[\sf@two]{\box\sf@box}%
-   \else
-     \subfloat[\sf@one][\sf@two]{\box\sf@box}%
-   \fi}
-\makeatother
-%% ------------------------------------------
-
-%% hack for top-aligned tabular cells -------------
-\newsavebox\topalignbox
-\newcolumntype{L}{%
-  >{\begin{lrbox}\topalignbox
-    \rule{0pt}{\ht\strutbox}}
-  l
-  <{\end{lrbox}%
-    \raisebox{\dimexpr-\height+\ht\strutbox\relax}%
-      {\usebox\topalignbox}}}
-\newcolumntype{C}{%
-  >{\begin{lrbox}\topalignbox
-    \rule{0pt}{\ht\strutbox}}
-  c
-  <{\end{lrbox}%
-    \raisebox{\dimexpr-\height+\ht\strutbox\relax}%
-      {\usebox\topalignbox}}}
-\newcolumntype{R}{%
-  >{\begin{lrbox}\topalignbox
-    \rule{0pt}{\ht\strutbox}}
-  r
-  <{\end{lrbox}%
-    \raisebox{\dimexpr-\height+\ht\strutbox\relax}%
-      {\usebox\topalignbox}}}
-%% ------------------------------------------------
-
-\newcommand\syn[1]{\textsf{#1}}
-\newcommand\bsyn[1]{\textsf{\bfseries #1}}
-\newcommand\msyn[1]{\textsf{#1}}
-\newcommand{\cc}{\mathop{::}}
-
-% \newcommand{\Eimp}[1]{\bsyn{import}~{#1}}
-% \newcommand{\Eonly}[2]{#1~\bsyn{only}~{#2}}
-% \newcommand{\Ehide}[1]{~\bsyn{hide}~{#1}}
-% \newcommand{\Enew}[1]{\bsyn{new}~{#1}}
-% \newcommand{\Elocal}[2]{\bsyn{local}~{#1}~\bsyn{in}~{#2}}
-% \newcommand{\Smv}[3]{\Emv[]{#1}{#2}{#3}}
-\newcommand{\Srm}[2]{#1 \mathord{\setminus} #2}
-
-\newcommand{\cpath}{\varrho}
-\newcommand{\fpath}{\rho}
-
-\newcommand{\ie}{\emph{i.e.},\xspace}
-\newcommand{\eg}{\emph{e.g.},~}
-\newcommand{\etal}{\emph{et al.}}
-
-\renewcommand{\P}[1]{\Cpkg{#1}}
-\newcommand{\X}[1]{\Cvar{#1}}
-\newcommand{\E}{\mathcal{E}}
-\newcommand{\C}{\mathcal{C}}
-\newcommand{\M}{\mathcal{M}}
-\newcommand{\B}{\mathcal{B}}
-\newcommand{\R}{\mathcal{R}}
-\newcommand{\K}{\mathcal{K}}
-\renewcommand{\L}{\mathcal{L}}
-\newcommand{\D}{\mathcal{D}}
-
-%%%% NEW
-
-\newdateformat{numericdate}{%
-\THEYEAR.\twodigit{\THEMONTH}.\twodigit{\THEDAY}
-}
-
-% EL DEFNS
-\newcommand{\shal}[1]{\syn{shallow}(#1)}
-\newcommand{\exports}[1]{\syn{exports}(#1)}
-\newcommand{\Slocals}[1]{\syn{locals}(#1)}
-\newcommand{\Slocalsi}[2]{\syn{locals}(#1; #2)}
-\newcommand{\specs}[1]{\syn{specs}(#1)}
-\newcommand{\ELmkespc}[2]{\syn{mkespc}(#1;#2)}
-\newcommand{\Smkeenv}[1]{\syn{mkeenv}(#1)}
-\newcommand{\Smklocaleenv}[2]{\syn{mklocaleenv}(#1;#2)}
-\newcommand{\Smklocaleenvespcs}[1]{\syn{mklocaleenv}(#1)}
-\newcommand{\Smkphnms}[1]{\syn{mkphnms}(#1)}
-\newcommand{\Smkphnm}[1]{\syn{mkphnm}(#1)}
-\newcommand{\Sfilterespc}[2]{\syn{filterespc}(#1;#2)}
-\newcommand{\Sfilterespcs}[2]{\syn{filterespcs}(#1;#2)}
-\newcommand{\Simps}[1]{\syn{imps}(#1)}
-
-
-
-% IL DEFNS
-\newcommand{\dexp}{\mathit{dexp}}
-\newcommand{\fexp}{\mathit{fexp}}
-\newcommand{\tfexp}{\mathit{tfexp}}
-\newcommand{\pexp}{\mathit{pexp}}
-\newcommand{\dtyp}{\mathit{dtyp}}
-\newcommand{\ftyp}{\mathit{ftyp}}
-\newcommand{\hsmod}{\mathit{hsmod}}
-\newcommand{\fenv}{\mathit{fenv}}
-\newcommand{\ILmkmod}[6]{\syn{mkmod}(#1; #2; #3; #4; #5; #6)}
-\newcommand{\ILmkstubs}[3]{\syn{mkstubs}(#1; #2; #3)}
-\newcommand{\Smkstubs}[1]{\syn{mkstubs}(#1)}
-\newcommand{\ILentnames}[1]{\syn{entnames}(#1)}
-\newcommand{\ILmkfenv}[1]{\syn{mkfenv}(#1)}
-\newcommand{\ILmkdtyp}[1]{\syn{mkdtyp}(#1)}
-\newcommand{\ILmkknd}[1]{\syn{mkknd}(#1)}
-\newcommand{\ILmkimpdecl}[2]{\syn{mkimpdecl}(#1;#2)}
-\newcommand{\ILmkimpdecls}[2]{\syn{mkimpdecls}(#1;#2)}
-\newcommand{\ILmkimpspec}[3]{\syn{mkimpspec}(#1;#2;#3)}
-\newcommand{\ILmkentimp}[3]{\syn{mkentimp}(#1;#2;#3)}
-\newcommand{\ILmkentimpp}[1]{\syn{mkentimp}(#1)}
-\newcommand{\ILmkexp}[2]{\syn{mkexp}(#1;#2)}
-\newcommand{\ILmkexpdecl}[2]{\syn{mkexpdecl}(#1;#2)}
-\newcommand{\ILmkespc}[2]{\syn{mkespc}(#1;#2)}
-\newcommand{\ILshal}[1]{\syn{shallow}(#1)}
-\newcommand{\ILexports}[1]{\syn{exports}(#1)}
-\newcommand{\ILdefns}[1]{\syn{defns}(#1)}
-\newcommand{\ILdefnsi}[2]{\syn{defns}(#1;#2)}
-
-% CORE DEFNS
-\newcommand{\Hentref}{\mathit{eref}}
-\newcommand{\Hentimp}{\mathit{import}}
-\newcommand{\Hentexp}{\mathit{export}}
-\newcommand{\Himp}{\mathit{impdecl}}
-\newcommand{\Himpspec}{\mathit{impspec}}
-\newcommand{\Himps}{\mathit{impdecls}}
-\newcommand{\Hexps}{\mathit{expdecl}}
-\newcommand{\Hdef}{\mathit{def}}
-\newcommand{\Hdefs}{\mathit{defs}}
-\newcommand{\Hdecl}{\mathit{decl}}
-\newcommand{\Hdecls}{\mathit{decls}}
-\newcommand{\Heenv}{\mathit{eenv}}
-\newcommand{\Haenv}{\mathit{aenv}}
-% \newcommand{\HIL}[1]{{\scriptstyle\downarrow}#1}
-\newcommand{\HIL}[1]{\check{#1}}
-
-\newcommand{\Hcmp}{\sqsubseteq}
-
-\newcommand{\uexp}{\mathit{uexp}}
-\newcommand{\utyp}{\mathit{utyp}}
-\newcommand{\typ}{\mathit{typ}}
-\newcommand{\knd}{\mathit{knd}}
-\newcommand{\kndstar}{\ttt{*}}
-\newcommand{\kndarr}[2]{#1\ensuremath{\mathbin{\ttt{->}}}#2}
-\newcommand{\kenv}{\mathit{kenv}}
-\newcommand{\phnm}{\mathit{phnm}}
-\newcommand{\spc}{\mathit{dspc}}
-\newcommand{\spcs}{\mathit{dspcs}}
-\newcommand{\espc}{\mathit{espc}}
-\newcommand{\espcs}{\mathit{espcs}}
-\newcommand{\ds}{\mathit{ds}}
-
-\newcommand{\shctx}{\sh{\Xi}_{\syn{ctx}}}
-\newcommand{\shctxsigma}{\sh{\Sigma}_{\syn{ctx}}}
-
-\newcommand{\vdashsh}{\Vdash}
-
-% \newcommand{\vdashghc}{\vdash_{\!\!\mathrm{c}}^{\!\!\mathrm{\scriptscriptstyle EL}}}
-% \newcommand{\vdashghcil}{\vdash_{\!\!\mathrm{c}}^{\!\!\mathrm{\scriptscriptstyle IL}}}
-% \newcommand{\vdashshghc}{\vdashsh_{\!\!\mathrm{c}}^{\!\!\mathrm{\scriptscriptstyle EL}}}
-\newcommand{\vdashghc}{\vdash_{\!\!\mathrm{c}}}
-\newcommand{\vdashghcil}{\vdash_{\!\!\mathrm{c}}^{\!\!\mathrm{\scriptscriptstyle IL}}}
-\newcommand{\vdashshghc}{\vdashsh_{\!\!\mathrm{c}}}
-
-% CORE STUFF
-\newcommandx*{\JCModImp}[5][1=\sh\B, 2=\nu_0, usedefault=@]%
-  {#1;#2 \vdashshghc #3;#4 \elabto #5}
-\newcommandx*{\JIlCModImp}[5][1=\fenv, 2=f_0, usedefault=@]%
-  {#1;#2 \vdashghcil #3;#4 \elabto #5}
-\newcommandx*{\JCSigImp}[5][1=\sh\B, 2=\sh\tau, usedefault=@]%
-  {#1;#2 \vdashshghc #3;#4 \elabto #5}
-
-\newcommandx*{\JCImpDecl}[3][1=\sh\B, usedefault=@]%
-  {#1 \vdashshghc #2 \elabto #3}
-\newcommandx*{\JCImp}[4][1=\sh\B, 2=p, usedefault=@]%
-  {#1;#2 \vdashshghc #3 \elabto #4}
-\newcommandx*{\JIlCImpDecl}[3][1=\fenv, usedefault=@]%
-  {#1 \vdashghcil #2 \elabto #3}
-\newcommandx*{\JIlCImp}[4][1=\fenv, 2=f, usedefault=@]%
-  {#1;#2 \vdashghcil #3 \elabto #4}
-
-\newcommandx*{\JCModExp}[4][1=\nu_0, 2=\Heenv, usedefault=@]%
-  {#1;#2 \vdashshghc #3 \elabto #4}
-\newcommandx*{\JIlCModExp}[4][1=f_0, 2=\HIL\Heenv, usedefault=@]%
-  {#1;#2 \vdashghcil #3 \elabto #4}
-
-\newcommandx*{\JCModDef}[5][1=\Psi, 2=\nu_0, 3=\Heenv, usedefault=@]%
-  {#1; #2; #3 \vdashghcil #4 : #5}
-\newcommandx*{\JIlCModDef}[5][1=\fenv, 2=f_0, 3=\HIL\Heenv, usedefault=@]%
-  {#1; #2; #3 \vdashghcil #4 : #5}
-\newcommandx*{\JCSigDecl}[5][1=\Psi, 2=\sh\tau, 3=\Heenv, usedefault=@]%
-  {#1; #2; #3 \vdashghcil #4 : #5}
-
-\newcommandx*{\JCExp}[6][1=\sh\Psi, 2=\nu_0, 3=\Hdefs, 4=\Heenv, usedefault=@]%
-  {#1;#2;#3;#4 \vdashshghc #5 \elabto #6}
-\newcommandx*{\JIlCExp}[4][1=f_0, 2=\HIL\Heenv, usedefault=@]%
-  {#1;#2 \vdashghcil #3 \elabto #4}
-
-\newcommandx*{\JCRefExp}[7][1=\sh\Psi, 2=\nu_0, 3=\Hdefs, 4=\Heenv, usedefault=@]%
-  {#1;#2;#3;#4 \vdashshghc #5 \elabto #6:#7}
-\newcommandx*{\JIlCRefExp}[7][1=\fenv, 2=f_0, 3=\HIL\Hdefs, 4=\HIL\Heenv, usedefault=@]%
-  {#1;#2;#3;#4 \vdashghcil #5 \elabto #6:#7}
-
-\newcommandx*{\JCMod}[4][1=\Gamma, 2=\nu_0, usedefault=@]%
-  {#1; #2 \vdashghc #3 : #4}
-\newcommandx*{\JIlCMod}[3][1=\fenv, usedefault=@]%
-  {#1 \vdashghcil #2 : #3}
-\newcommandx*{\JCSig}[5][1=\Gamma, 2=\sh\tau, usedefault=@]%
-  {#1; #2 \vdashghc #3 \elabto #4;#5}
-\newcommandx*{\JCShSig}[5][1=\Gamma, 2=\sh\tau, usedefault=@]%
-  {#1; #2 \vdashghc #3 \elabto #4;#5}
-\newcommandx*{\JCModElab}[5][1=\Gamma, 2=\nu_0, usedefault=@]%
-  % {#1; #2 \vdashghc #3 : #4 \elabto #5}
-  {#1; #2 \vdashghc #3 : #4 \;\shade{\elabto #5}}
-
-\newcommandx*{\JCWfEenv}[2][1=\Haenv, usedefault=@]%
-  {#1 \vdashshghc #2~\syn{wf}}
-\newcommandx*{\JCWfEenvMap}[2][1=\Haenv, usedefault=@]%
-  {#1 \vdashshghc #2~\syn{wf}}
-\newcommandx*{\JIlCWfEenv}[2][1=\HIL\Haenv, usedefault=@]%
-  {#1 \vdashghcil #2~\syn{wf}}
-\newcommandx*{\JIlCWfEenvMap}[2][1=\HIL\Haenv, usedefault=@]%
-  {#1 \vdashghcil #2~\syn{wf}}
-
-\newcommandx*{\JIlTfexp}[3][1=\fenv, 2=f_0, usedefault=@]%
-  {#1; #2 \vdash #3}
-
-
-
-  % IL STUFF
-
-\newcommandx*{\JIlWf}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlKnd}[4][1=\fenv, 2=\kenv, usedefault=@]%
-  {#1;#2 \vdashghcil #3 \mathrel{\cc} #4}
-% \newcommandx*{\JIlSub}[4][1=\fenv, 2=f, usedefault=@]%
-%   {#1;#2 \vdash #3 \le #4}
-\newcommandx*{\JIlSub}[2][usedefault=@]%
-  {\vdash #1 \le #2}
-\newcommandx*{\JIlMerge}[3][usedefault=@]%
-  {\vdash #1 \oplus #2 \Rightarrow #3}
-
-\newcommandx*{\JIlDexp}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2}
-\newcommandx*{\JIlDexpTyp}[3][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 : #3}
-
-\newcommandx*{\JIlWfFenv}[2][1=\nil, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlWfFtyp}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlWfSpc}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlWfESpc}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlWfSig}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JIlWfFtypSpecs}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{specs-wf}}
-\newcommandx*{\JIlWfFtypExps}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{exports-wf}}
-\newcommandx*{\JIlWfFenvDeps}[2][1=\fenv, usedefault=@]%
-  {#1 \vdash #2 ~\syn{deps-wf}}
-
-% WF TYPE STUFF IN EL
-\newcommandx*{\JPkgValid}[1]%
-  {\vdash #1 ~\syn{pkg-valid}}
-\newcommandx*{\JWfPkgCtx}[1][1=\Delta, usedefault=@]%
-  {\vdash #1 ~\syn{wf}}
-\newcommandx*{\JWfPhCtx}[2][1=\nil, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfModTyp}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfModTypPol}[3][1=\Psi, usedefault=@]%
-  {#1 \vdash #2^{#3} ~\syn{wf}}
-\newcommandx*{\JWfLogSig}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfSpc}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfESpc}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfSig}[2][1=\nil, usedefault=@]%
-  {#1 \vdash #2 ~\syn{wf}}
-\newcommandx*{\JWfModTypSpecs}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{specs-wf}}
-\newcommandx*{\JWfModTypPolSpecs}[3][1=\Psi, usedefault=@]%
-  {#1 \vdash #2^{#3} ~\syn{specs-wf}}
-\newcommandx*{\JWfModTypExps}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{exports-wf}}
-\newcommandx*{\JWfPhCtxDeps}[2][1=\Psi, usedefault=@]%
-  {#1 \vdash #2 ~\syn{deps-wf}}
-\newcommandx*{\JWfPhCtxDepsOne}[4][1=\Psi, usedefault=@]%
-  {#1 \vdash \styp{#2}{#3}{#4} ~\syn{deps-wf}}
-
-% WF SHAPE STUFF IN EL
-\newcommandx*{\JWfShPhCtx}[2][1=\nil, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfModSh}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfModShPol}[3][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2^{#3} ~\syn{wf}}
-\newcommandx*{\JWfShLogSig}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfShSpc}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfShESpc}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfShSig}[2][1=\nil, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{wf}}
-\newcommandx*{\JWfModShSpecs}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{specs-wf}}
-\newcommandx*{\JWfModShPolSpecs}[3][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2^{#3} ~\syn{specs-wf}}
-\newcommandx*{\JWfModShExps}[2][1=\sh\Psi, usedefault=@]%
-  {#1 \vdashsh #2 ~\syn{exports-wf}}
-\newcommandx*{\JWfEenv}[4][1=\sh\Psi, 2=\nu_0, 3=\Hdefs, usedefault=@]%
-  {#1;#2;#3 \vdashshghc #4 ~\syn{wf}}
-
-\newcommandx*{\JCoreKnd}[4][1=\Psi, 2=\kenv, usedefault=@]%
-  {#1;#2 \vdashghc #3 \mathrel{\cc} #4}
-
-\newcommandx*{\JStampEq}[2]%
-  {\vdash #1 \equiv #2}
-\newcommandx*{\JStampNeq}[2]%
-  {\vdash #1 \not\equiv #2}
-\newcommandx*{\JUnif}[3]%
-  {\syn{unify}(#1 \doteq #2) \elabto #3}
-\newcommandx*{\JUnifM}[2]%
-  {\syn{unify}(#1) \elabto #2}
-
-\newcommandx*{\JModTypWf}[1]%
-  {\vdash #1 ~\syn{wf}}
-  
-\newcommandx*{\JModSub}[2]%
-  {\vdash #1 \le #2}
-\newcommandx*{\JModSup}[2]%
-  {\vdash #1 \ge #2}
-\newcommandx*{\JShModSub}[2]%
-  {\vdashsh #1 \le #2}
-
-\newcommandx*{\JModEq}[2]%
-  {\vdash #1 \equiv #2}
-% \newcommandx*{\JCShModEq}[3][3=\C]%
-%   {\vdashsh #1 \equiv #2 \mathbin{|} #3}
-
-\newcommandx*{\JETyp}[4][1=\Gamma, 2=\shctxsigma, usedefault=@]%
-  {#1;#2 \vdash #3 : #4}
-\newcommandx*{\JETypElab}[5][1=\Gamma, 2=\shctxsigma, usedefault=@]%
-  {\JETyp[#1][#2]{#3}{#4} \elabto #5}
-\newcommandx*{\JESh}[3][1=\sh\Gamma, usedefault=@]%
-  {#1 \vdashsh #2 \Rightarrow #3}
-
-\newcommandx*{\JBTyp}[5][1=\Delta, 2=\Gamma, 3=\shctx, usedefault=@]%
-  {#1;#2;#3 \vdash #4 : #5}
-\newcommandx*{\JBTypElab}[6][1=\Delta, 2=\Gamma, 3=\shctx, usedefault=@]%
-  % {\JBTyp[#1][#2][#3]{#4}{#5} \elabto #6}
-  {\JBTyp[#1][#2][#3]{#4}{#5} \;\shade{\elabto #6}}
-\newcommandx*{\JBSh}[4][1=\Delta, 2=\sh\Gamma, usedefault=@]%
-  {#1;#2 \vdashsh #3 \Rightarrow #4}
-  
-\newcommandx*{\JBVTyp}[4][1=\Delta, 2=\shctx, usedefault=@]%
-  {#1;#2 \vdash #3 : #4}
-\newcommandx*{\JBVTypElab}[5][1=\Delta, 2=\shctx, usedefault=@]%
-  % {\JBVTyp[#1][#2]{#3}{#4} \elabto #5}
-  {\JBVTyp[#1][#2]{#3}{#4} \;\shade{\elabto #5}}
-\newcommandx*{\JBVSh}[4][1=\Delta, usedefault=@]%
-  {#1 \vdashsh #2 \Rightarrow #3;\, #4}
-  
-\newcommandx*{\JImp}[3][1=\Gamma, usedefault=@]%
-  {#1 \vdashimp #2 \elabto #3}
-\newcommandx*{\JShImp}[3][1=\sh\Gamma, usedefault=@]%
-  {#1 \vdashshimp #2 \elabto #3}
-  
-\newcommandx*{\JGhcMod}[4]%
-  {#1; #2 \vdashghc #3 : #4}
-\newcommandx*{\JShGhcMod}[4]%
-  {#1; #2 \vdashshghc #3 : #4}
-  
-\newcommandx*{\JGhcSig}[5]%
-  {#1; #2 \vdashghc #3 \elabto #4;#5}
-\newcommandx*{\JShGhcSig}[5]%
-  {#1; #2 \vdashshghc #3 \elabto #4;#5}
-  
-\newcommandx*{\JThin}[3][1=t, usedefault=@]%
-  {\vdash #2 \xrightarrow{~#1~} #3}
-\newcommandx*{\JShThin}[3][1=t, usedefault=@]%
-  {\vdashsh #2 \xrightarrow{~#1~} #3}
-
-\newcommandx*{\JShMatch}[3][1=\nu, usedefault=@]%
-  {#1 \vdash #2 \sqsubseteq #3}
-  
-\newcommandx*{\JShTrans}[4]%
-  {\vdash #1 \le_{#2} #3 \elabto #4}
-  
-\newcommandx*{\JMerge}[3]%
-  {\vdash #1 + #2 \Rightarrow #3}
-\newcommandx*{\JShMerge}[5]%
-  {\vdashsh #1 + #2 \Rightarrow #3;\, #4;\, #5}
-\newcommandx*{\JShMergeNew}[4]%
-  {\vdashsh #1 + #2 \Rightarrow #3;\, #4}
-\newcommandx*{\JShMergeSimple}[3]%
-  {\vdashsh #1 + #2 \Rightarrow #3}
-
-\newcommandx*{\JDTyp}[3][1=\Delta, usedefault=@]%
-  {#1 \vdash #2 : #3}
-\newcommandx*{\JDTypElab}[4][1=\Delta, usedefault=@]%
-  % {#1 \vdash #2 : #3 \elabto #4}
-  {#1 \vdash #2 : #3 \;\shade{\elabto #4}}
-
-\newcommandx*{\JTTyp}[2][1=\Delta, usedefault=@]%
-  {#1 \vdash #2}
-
-\newcommandx*{\JSound}[3][1=\Psi_\syn{ctx}, usedefault=@]%
-  {#1 \vdash #2 \sim #3}
-
-\newcommandx*{\JSoundOne}[4][1=\Psi, 2=\fenv, usedefault=@]%
-  {\vdash #3 \sim #4}
-% \newcommand{\Smodi}[4]{\ensuremath{\oxb{=#2 \cc #3 \imps #4}^{#1}}}
-\newcommand{\Smodi}[3]{\ensuremath{\oxb{=#2 \cc #3}^{#1}}}
-\newcommand{\Smod}[2]{\Smodi{+}{#1}{#2}}
-\newcommand{\Ssig}[2]{\Smodi{-}{#1}{#2}}
-\newcommand{\Sreq}[2]{\Smodi{?}{#1}{#2}}
-\newcommand{\Shole}[2]{\Smodi{\circ}{#1}{#2}}
-
-\newcommand{\SSmodi}[2]{\ensuremath{\oxb{=#2}^{#1}}}
-\newcommand{\SSmod}[1]{\SSmodi{+}{#1}}
-\newcommand{\SSsig}[1]{\SSmodi{-}{#1}}
-\newcommand{\SSreq}[1]{\SSmodi{?}{#1}}
-\newcommand{\SShole}[1]{\SSmodi{\circ}{#1}}
-
-% \newcommand{\styp}[3]{\oxb{{#1}\cc{#2}}^{#3}}
-\newcommand{\styp}[3]{{#1}{:}{#2}^{#3}}
-\newcommand{\stm}[2]{\styp{#1}{#2}{\scriptscriptstyle+}}
-\newcommand{\sts}[2]{\styp{#1}{#2}{\scriptscriptstyle-}}
-
-% \newcommand{\mtypsep}{[\!]}
-\newcommand{\mtypsep}{\mbox{$\bm{;}$}}
-\newcommand{\mtypsepsp}{\hspace{.3em}}
-\newcommand{\msh}[3]{\aoxb{#1 ~\mtypsep~ #2 ~\mtypsep~ #3}}
-\newcommand{\mtyp}[3]{
-  \aoxb{\mtypsepsp #1 \mtypsepsp\mtypsep\mtypsepsp
-        #2 \mtypsepsp\mtypsep\mtypsepsp
-        #3 \mtypsepsp}}
-\newcommand{\bigmtyp}[3]{\ensuremath{
-  \left\langle\!\vrule \begin{array}{l}
-    #1 ~\mtypsep \\[0pt]
-    #2 ~\mtypsep \\
-    #3
-  \end{array} \vrule\!\right\rangle
-}}
-
-
-\newcommand{\mtypm}[2]{\mtyp{#1}{#2}^{\scriptstyle+}}
-\newcommand{\mtyps}[2]{\mtyp{#1}{#2}^{\scriptstyle-}}
-\newcommand{\bigmtypm}[2]{\bigmtyp{#1}{#2}^{\scriptstyle+}}
-\newcommand{\bigmtyps}[2]{\bigmtyp{#1}{#2}^{\scriptstyle-}}
-
-\newcommand{\mref}{\ensuremath{\mathit{mref}}}
-\newcommand{\selfpath}{\msyn{Local}}
-
-% \newcommand{\Ltyp}[3]{\oxb{#1 \mathbin{\scriptstyle\MVAt} #2}^{#3}}
-% \newcommand{\Ltyp}[2]{\poxb{#1 \mathbin{\scriptstyle\MVAt} #2}}
-\newcommand{\Ltyp}[2]{#1 {\scriptstyle\MVAt} #2}
-
-\newcommand{\Sshape}[1]{\ensuremath{\syn{shape}(#1)}}
-\newcommand{\Srename}[2]{\ensuremath{\syn{rename}(#1;#2)}}
-\newcommand{\Scons}[2]{\ensuremath{\syn{cons}(#1;#2)}}
-\newcommand{\Smkreq}[1]{\ensuremath{\syn{hide}(#1)}}
-\newcommand{\Sfv}[1]{\ensuremath{\syn{fv}(#1)}}
-\newcommand{\Sdom}[1]{\ensuremath{\syn{dom}(#1)}}
-\newcommand{\Srng}[1]{\ensuremath{\syn{rng}(#1)}}
-\newcommand{\Sdomp}[2]{\ensuremath{\syn{dom}_{#1}(#2)}}
-\newcommand{\Sclos}[1]{\ensuremath{\syn{clos}(#1)}}
-\newcommand{\Scloss}[2]{\ensuremath{\syn{clos}_{#1}(#2)}}
-\newcommand{\Snorm}[1]{\ensuremath{\syn{norm}(#1)}}
-\newcommand{\Sident}[1]{\ensuremath{\syn{ident}(#1)}}
-\newcommand{\Snec}[2]{\ensuremath{\syn{nec}(#1; #2)}}
-\newcommand{\Sprovs}[1]{\ensuremath{\syn{provs}(#1)}}
-\newcommand{\Smkstamp}[2]{\ensuremath{\syn{mkident}(#1; #2)}}
-\newcommand{\Sname}[1]{\ensuremath{\syn{name}(#1)}}
-\newcommand{\Snames}[1]{\ensuremath{\syn{names}(#1)}}
-\newcommand{\Sallnames}[1]{\ensuremath{\syn{allnames}(#1)}}
-\newcommand{\Shassubs}[1]{\ensuremath{\syn{hasSubs}(#1)}}
-\newcommand{\Snooverlap}[1]{\ensuremath{\syn{nooverlap}(#1)}}
-\newcommand{\Sreduce}[2]{\ensuremath{\syn{apply}(#1; #2)}}
-\newcommand{\Smkfenv}[1]{\ensuremath{\syn{mkfenv}(#1)}}
-\newcommand{\Svalidspc}[2]{\ensuremath{\syn{validspc}(#1; #2)}}
-\newcommand{\Srepath}[2]{\ensuremath{\syn{repath}(#1; #2)}}
-\newcommand{\Smksigenv}[2]{\ensuremath{\syn{mksigenv}(#1; #2)}}
-\newcommand{\Smksigshenv}[2]{\ensuremath{\syn{mksigshenv}(#1; #2)}}
-\newcommand{\Squalify}[2]{\ensuremath{\syn{qualify}(#1; #2)}}
-\newcommandx*{\Sdepends}[2][1=\Psi, usedefault=@]%
-  {\ensuremath{\syn{depends}_{#1}(#2)}}
-\newcommandx*{\Sdependss}[3][1=\Psi, 2=N, usedefault=@]%
-  {\ensuremath{\syn{depends}_{#1;#2}(#3)}}
-\newcommandx*{\Sdependsss}[4][1=\Psi, 2=V, 3=\theta, usedefault=@]%
-  {\ensuremath{\syn{depends}_{#1;#2;#3}(#4)}}
-\newcommand{\Snormsubst}[2]{\ensuremath{\syn{norm}(#1; #2)}}
-
-% \newcommand{\Smergeable}[2]{\ensuremath{\syn{mergeable}(#1; #2)}}
-\newcommand{\mdef}{\mathrel{\bot}}
-\newcommand{\Smergeable}[2]{\ensuremath{#1 \mdef #2}}
-
-\newcommand{\Sstamp}[1]{\ensuremath{\syn{stamp}(#1)}}
-\newcommand{\Stype}[1]{\ensuremath{\syn{type}(#1)}}
-
-\newcommand{\Strue}{\ensuremath{\syn{true}}}
-\newcommand{\Sfalse}{\ensuremath{\syn{false}}}
-
-\newcommandx*{\refsstar}[2][1=\nu_0, usedefault=@]%
-  {\ensuremath{\syn{refs}^{\star}}_{#1}(#2)}
-
-\renewcommand{\merge}{\boxplus}
-\newcommand{\meet}{\sqcap}
-
-\newcommand{\Shaslocaleenv}[3]{\ensuremath{\syn{haslocaleenv}(#1;#2;#3)}}
-\newcommand{\MTvalidnewmod}[3]{\ensuremath{\syn{validnewmod}(#1;#2;#3)}}
-\newcommand{\Sdisjoint}[1]{\ensuremath{\syn{disjoint}(#1)}}
-\newcommand{\Sconsistent}[1]{\ensuremath{\syn{consistent}(#1)}}
-\newcommand{\Slocmatch}[2]{\ensuremath{\syn{locmatch}(#1;#2)}}
-\newcommand{\Sctxmatch}[2]{\ensuremath{\syn{ctxmatch}(#1;#2)}}
-\newcommand{\Snolocmatch}[2]{\ensuremath{\syn{nolocmatch}(#1;#2)}}
-\newcommand{\Snoctxmatch}[2]{\ensuremath{\syn{noctxmatch}(#1;#2)}}
-\newcommand{\Sislocal}[2]{\ensuremath{\syn{islocal}(#1;#2)}}
-\newcommand{\Slocalespcs}[2]{\ensuremath{\syn{localespcs}(#1;#2)}}
-
-\newcommand{\Cprod}[1]{\syn{productive}(#1)}
-\newcommand{\Cnil}{\nil}
-\newcommand{\id}{\syn{id}}
-
-\newcommand{\nui}{\nu_{\syn{i}}}
-\newcommand{\taui}{\tau_{\syn{i}}}
-\newcommand{\Psii}{\Psi_{\syn{i}}}
-
-\newcommand{\vis}{\ensuremath{\mathsf{\scriptstyle V}}}
-\newcommand{\hid}{\ensuremath{\mathsf{\scriptstyle H}}}
-
-\newcommand{\taum}[1]{\ensuremath{\tau_{#1}^{m_{#1}}}}
-
-\newcommand{\sigmamod}{\sigma_{\syn{m}}}
-\newcommand{\sigmaprov}{\sigma_{\syn{p}}}
-
-\newcommand{\Svalidsubst}[2]{\ensuremath{\syn{validsubst}(#1;#2)}}
-\newcommand{\Salias}[1]{\ensuremath{\syn{alias}(#1)}}
-\newcommand{\Saliases}[1]{\ensuremath{\syn{aliases}(#1)}}
-\newcommand{\Simp}[1]{\ensuremath{\syn{imp}(#1)}}
-\newcommand{\Styp}[1]{\ensuremath{\syn{typ}(#1)}}
-\newcommand{\Spol}[1]{\ensuremath{\syn{pol}(#1)}}
-
-\newcommand{\stoff}{\stof{(-)}}
-\newcommand{\stheta}{\stof\theta}
-
-
-%%%%%%% FOR THE PAPER!
-\newcommand{\secref}[1]{Section~\ref{sec:#1}}
-\newcommand{\figref}[1]{Figure~\ref{fig:#1}}
-
-% typesetting for module/path names
-\newcommand{\mname}[1]{\textsf{#1}}
-\newcommand{\m}[1]{\mname{#1}}
-
-% typesetting for package names
-\newcommand{\pname}[1]{\textsf{#1}}
-
-\newcommand{\kpm}[2]{\angb{\pname{#1}.#2}}
-
-% for core entities
-\newcommand{\code}[1]{\texttt{#1}}
-\newcommand{\core}[1]{\texttt{#1}}
-
-\newcommand{\req}{\bsyn{req}}
-\newcommand{\hiding}[1]{\req~\m{#1}}
-
-\newcommand{\Emod}[1]{\ensuremath{[#1]}}
-\newcommand{\Esig}[1]{\ensuremath{[\cc#1]}}
-\newcommand{\Epkg}[2]{\bsyn{package}~\pname{#1}~\bsyn{where}~{#2}}
-% \newcommand{\Epkgt}[3]{\bsyn{package}~{#1}~\bsyn{only}~{#2}~\bsyn{where}~{#3}}
-\newcommand{\Epkgt}[3]{\bsyn{package}~\pname{#1}~{#2}~\bsyn{where}~{#3}}
-\newcommand{\Einc}[1]{\bsyn{include}~\pname{#1}}
-% \newcommand{\Einct}[2]{\bsyn{include}~{#1}~\bsyn{only}~{#2}}
-% \newcommand{\Einctr}[3]{\bsyn{include}~{#1}~\bsyn{only}~{#2}~{#3}}
-\newcommand{\Einct}[2]{\bsyn{include}~\pname{#1}~(#2)}
-\newcommand{\Eincr}[2]{\bsyn{include}~\pname{#1}~\angb{#2}}
-\newcommand{\Einctr}[3]{\bsyn{include}~\pname{#1}~(#2)~\angb{#3}}
-\newcommand{\Emv}[2]{#1 \mapsto #2}
-\newcommand{\Emvp}[2]{\m{#1} \mapsto \m{#2}}
-\newcommand{\Etr}[3][~]{{#2}{#1}\langle #3 \rangle}
-\newcommand{\Erm}[3][~]{{#2}{#1}\langle #3 \mapnil \rangle}
-\newcommand{\Ethin}[1]{(#1)}
-\newcommand{\Ethinn}[2]{(#1; #2)}
-
-
-% \newcommand{\Pdef}[2]{\ensuremath{\begin{array}{l} \Phead{#1} #2\end{array}}}
-% \newcommand{\Phead}[1]{\bsyn{package}~\pname{#1}~\bsyn{where} \\}
-% \newcommand{\Pbndd}[2]{\hspace{1em}{#1} = {#2} \\}
-% \newcommand{\Pbnd}[2]{\hspace{1em}\mname{#1} = {#2} \\}
-% \newcommand{\Pref}[2]{\hspace{1em}\mname{#1} = \mname{#2} \\}
-% \newcommand{\Pmod}[2]{\hspace{1em}\mname{#1} = [\code{#2}] \\}
-% \newcommand{\Psig}[2]{\hspace{1em}\mname{#1} \cc [\code{#2}] \\}
-\newcommand{\Pdef}[2]{\ensuremath{
-  \begin{array}{@{\hspace{1em}}L@{\;\;}c@{\;\;}l}
-    \multicolumn{3}{@{}l}{\Phead{#1}} \\
-    #2
-  \end{array}
-}}
-\newcommand{\Pdeft}[3]{\ensuremath{
-  \begin{array}{@{\hspace{1em}}L@{\;\;}c@{\;\;}l}
-    \multicolumn{3}{@{}l}{\Pheadt{#1}{#2}} \\
-    #3
-  \end{array}
-}}
-\newcommand{\Phead}[1]{\bsyn{package}~\pname{#1}~\bsyn{where}}
-\newcommand{\Pheadt}[2]{\bsyn{package}~\pname{#1}~(#2)~\bsyn{where}}
-\newcommand{\Pbnd}[2]{#1 &=& #2 \\}
-\newcommand{\Pref}[2]{\mname{#1} &=& \mname{#2} \\}
-\newcommand{\Pmod}[2]{\mname{#1} &=& [\code{#2}] \\}
-\newcommand{\Pmodd}[2]{\mname{#1} &=& #2 \\}
-\newcommand{\Psig}[2]{\mname{#1} &\cc& [\code{#2}] \\}
-\newcommand{\Psigg}[2]{\mname{#1} &\cc& #2 \\}
-\newcommand{\Pmulti}[1]{\multicolumn{3}{@{\hspace{1em}}l} {#1} \\}
-\newcommand{\Pinc}[1]{\Pmulti{\Einc{#1}}}
-\newcommand{\Pinct}[2]{\Pmulti{\Einct{#1}{#2}}}
-\newcommand{\Pincr}[2]{\Pmulti{\Eincr{#1}{#2}}}
-\newcommand{\Pinctr}[3]{\Pmulti{\Einctr{#1}{#2}{#3}}}
-\newcommand{\Pmodbig}[2]{\mname{#1} &=& \left[
-  \begin{codeblock}
-  #2
-  \end{codeblock}
-\right] \\}
-\newcommand{\Psigbig}[2]{\mname{#1} &\cc& \left[
-  \begin{codeblock}
-  #2
-  \end{codeblock}
-\right] \\}
-
-\newcommand{\Mimp}[1]{\msyn{import}~\mname{#1}}
-\newcommand{\Mimpq}[1]{\msyn{import}~\msyn{qualified}~\mname{#1}}
-\newcommand{\Mimpas}[2]{\msyn{import}~\mname{#1}~\msyn{as}~\mname{#2}}
-\newcommand{\Mimpqas}[2]{\msyn{import}~\msyn{qualified}~\mname{#1}~\msyn{as}~\mname{#2}}
-\newcommand{\Mexp}[1]{\msyn{export}~(#1)}
-
-\newcommand{\illtyped}{\hfill ($\times$) \; ill-typed}
-
-\newenvironment{example}[1][LL]%
-  {\ignorespaces \begin{flushleft}\begin{tabular}{@{\hspace{1em}}#1} }%
-  {\end{tabular}\end{flushleft} \ignorespacesafterend}
-
-\newenvironment{counterexample}[1][LL]%
-  {\ignorespaces \begin{flushleft}\begin{tabular}{@{\hspace{1em}}#1} }%
-  {& \text{\illtyped} \end{tabular}\end{flushleft}  \ignorespacesafterend}
-
-\newenvironment{codeblock}%
-  {\begin{varwidth}{\textwidth}\begin{alltt}}%
-  {\end{alltt}\end{varwidth}}
-
-\newcommand{\fighead}{\hrule\vspace{1.5ex}}
-\newcommand{\figfoot}{\vspace{1ex}\hrule}
-\newenvironment{myfig}{\fighead\small}{\figfoot}
-
-\newcommand{\Mhead}[2]{\syn{module}~{#1}~\syn{(}{#2}\syn{)}~\syn{where}}
-\newcommand{\Mdef}[3]{\ensuremath{
-  \begin{array}{@{\hspace{1em}}L}
-    \multicolumn{1}{@{}L}{\Mhead{#1}{\core{#2}}} \\
-    #3
-  \end{array}
-}}
-
-\newcommand{\HMstof}[1]{\ensuremath{#1}}
-% \newcommand{\HMstof}[1]{\ensuremath{\lfloor #1 \rfloor}}
-% \newcommand{\HMstof}[1]{\ensuremath{\underline{#1}}}
-% \newcommand{\HMstof}[1]{{#1}^{\star}}
-\newcommand{\HMhead}[2]{\syn{module}~\(\HMstof{#1}\)~\syn{(}{#2}\syn{)}~\syn{where}}
-\newcommand{\HMdef}[3]{\ensuremath{
-  \begin{array}{@{\hspace{1em}}L}
-    \multicolumn{1}{@{}L}{\HMhead{#1}{\core{#2}}} \\
-    #3
-  \end{array}
-}}
-\newcommand{\HMimpas}[3]{%
-  \msyn{import}~\ensuremath{\HMstof{#1}}~%
-  \msyn{as}~\mname{#2}~\msyn{(}\core{#3}\msyn{)}}
-\newcommand{\HMimpqas}[3]{%
-  \msyn{import}~\msyn{qualified}~\ensuremath{\HMstof{#1}}~%
-  \msyn{as}~\mname{#2}~\msyn{(}\core{#3}\msyn{)}}
-
-\newcommand{\stackedenv}[2][c]{\ensuremath{
-  \begin{array}{#1}
-  #2
-  \end{array}
-}}
-
-% \renewcommand{\nil}{\mathsf{nil}}
-\renewcommand{\nil}{\mathrel\emptyset}
-
-% \newcommand{\ee}{\mathit{ee}}
-\newcommand{\ee}{\mathit{dent}}
-
-\renewcommand{\gets}{\mathbin{\coloneqq}}
\ No newline at end of file
diff --git a/docs/backpack/commands-rebindings.tex b/docs/backpack/commands-rebindings.tex
deleted file mode 100644
index 96ad2bb2cc..0000000000
--- a/docs/backpack/commands-rebindings.tex
+++ /dev/null
@@ -1,57 +0,0 @@
-
-
-%% hide the full syntax of shapes/types for the paper
-\newcommand{\fullmsh}[3]{\aoxb{#1 ~\mtypsep~ #2 ~\mtypsep~ #3}}
-\newcommand{\fullmtyp}[3]{
-  \aoxb{\mtypsepsp #1 \mtypsepsp\mtypsep\mtypsepsp
-        #2 \mtypsepsp\mtypsep\mtypsepsp
-        #3 \mtypsepsp}}
-\newcommand{\fullbigmtyp}[3]{\ensuremath{
-  \left\langle\!\vrule \begin{array}{l}
-    #1 ~\mtypsep \\[0pt]
-    #2 ~\mtypsep \\
-    #3
-  \end{array} \vrule\!\right\rangle
-}}
-\renewcommand{\msh}[2]{\aoxb{#1 \mtypsepsp\mtypsep\mtypsepsp #2}}
-\renewcommand{\mtyp}[2]{
-  \aoxb{#1 ~\mtypsep~ #2}}
-\newcommand{\mtypstretch}[2]{
-  \left\langle\!\vrule
-    \mtypsepsp #1 \mtypsepsp\mtypsep\mtypsepsp #2 \mtypsepsp
-  \vrule\!\right\rangle
-}
-\renewcommand{\bigmtyp}[2]{\ensuremath{
-  \left\langle\!\vrule \begin{array}{l}
-    #1 ~\mtypsep \\[0pt] #2
-  \end{array} \vrule\!\right\rangle
-}}
-
-
-
-%% change syntax of signatures
-\renewcommand{\Esig}[1]{\ensuremath{\,[#1]}}
-
-\renewcommandx*{\JBVSh}[3][1=\Delta, usedefault=@]%
-  {#1 \vdashsh #2 \Rightarrow #3}
-
-
-% JUDGMENTS
-\renewcommandx*{\JBTypElab}[6][1=\Delta, 2=\Gamma, 3=\shctx, usedefault=@]%
-  % {\JBTyp[#1][#2][#3]{#4}{#5} \elabto #6}
-  {\JBTyp[#1][#2][#3]{#4}{#5} \;\shade{\elabto #6}}
-\renewcommandx*{\JBVTypElab}[5][1=\Delta, 2=\shctx, usedefault=@]%
-  % {\JBVTyp[#1][#2]{#3}{#4} \elabto #5}
-  {\JBVTyp[#1][#2]{#3}{#4} \;\shade{\elabto #5}}
-\renewcommandx*{\JDTypElab}[4][1=\Delta, usedefault=@]%
-  % {#1 \vdash #2 : #3 \elabto #4}
-  {#1 \vdash #2 : #3 \;\shade{\elabto #4}}
-\renewcommandx*{\JCModElab}[5][1=\Gamma, 2=\nu_0, usedefault=@]%
-  % {#1; #2 \vdashghc #3 : #4 \elabto #5}
-  {#1; #2 \vdashghc #3 : #4 \;\shade{\elabto #5}}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "paper"
-%%% End: 
diff --git a/docs/backpack/diagrams.xoj b/docs/backpack/diagrams.xoj
deleted file mode 100644
index acec8d02de..0000000000
--- a/docs/backpack/diagrams.xoj
+++ /dev/null
diff --git a/docs/backpack/pkgdb.png b/docs/backpack/pkgdb.png
deleted file mode 100644
index 9779444b42..0000000000
--- a/docs/backpack/pkgdb.png
+++ /dev/null