Rewrite section 1 of the Backpack manual. [skip ci]

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

1 files changed, 344 insertions, 202 deletions

diff --git a/docs/backpack/backpack-manual.tex b/docs/backpack/backpack-manual.tex
index bcb33b4b9b..31a0ce5d84 100644
--- a/docs/backpack/backpack-manual.tex
+++ b/docs/backpack/backpack-manual.tex
@@ -2,6 +2,7 @@
 
 \usepackage{color}
 \usepackage{fullpage}
+\usepackage{hyperref}
 
 \newcommand{\Red}[1]{{\color{red} #1}}
 
@@ -11,64 +12,37 @@
 
 \maketitle
 
-\section{GHC}
-
-\subsection{Conventions}
+\paragraph{What is this?}  This is an in-depth technical specification of
+all of the new components associated with Backpack, a new module system
+for Haskell.  This is \emph{not} a tutorial, and it assumes you are
+familiar with the basic motivation and structure of Backpack.
+
+\paragraph{How to read this manual}  This manual is split into three
+sections, in dependency order.  The first section describes the new
+features added to GHC, e.g., new compilation flags and input formats.
+In principle, a user could take advantage of Backpack using just these
+features, without using Cabal or cabal-install; thus, we describe it
+first.  The next section describes the new features added to the library
+Cabal, and the last section describes how cabal-install drives the
+entire process.  A downside of this approach is that we start off by
+describing low-level GHC features which are quite dissimilar from the
+high-level Backpack interface, but we're not really trying to explain
+Backpack to complete new users.  \Red{Red indicates features which are
+not implemented yet.}
 
-In this subsection, we describe some recurrent patterns you will see in the
-Backpack implementation.
-
-\paragraph{Package key}  A package key is an opaque identifier
-identifying a package which serves as the basis for type identity and
-linker symbols.  Informally, you might think of a package as a package
-name and its version, e.g., \texttt{containers-0.9}; however, sometimes,
-it is necessary to distinguish between installed instances of a package
-with the same name and version which were compiled with different
-dependencies.  Thus, in practice, a package key looks something like
-\texttt{conta\_GtvvBIboSRuDmyUQfSZoAx}.  In this document, we'll use
-\texttt{containers\_KEY} as a convenient shorthand to refer to some
-package key for the \texttt{containers} package.  The package key is
-programatically generated by Cabal (consisting of a hash of the
-dependencies), but as far as GHC is concerned, the details of this
-generation are not important.
-
-The package key is different from an \emph{installed package ID}, which
-is a more fine-grained identifier for a package.  Identical installed
-package IDs imply identical package keys, but not vice versa.  However,
-in this subsection, we will treat them as equivalent, since within a single
-run of GHC we enforce that package keys and (non-shadowed) installed
-package IDs are in one-to-one correspondence.
-
-\paragraph{Syntax of original names}  In a few command flags
-(\texttt{-sig-of} and \texttt{-shape-of}), we need to specify an
-original name and/or original module.  These are qualified names which
-unambiguously specify some entity, and are the combination of a
-\emph{package key}, a \emph{module name} and, in the case of original
-names, the unqualified \emph{name} itself.  We use the convention of
-representing such names as \texttt{package:The.Module} or
-\texttt{package:The.Module.name} in the case of original names.%
-\footnote{As a forward reference: Cabal adopts a different convention which
-utilizes installed package IDs rather than package keys (and a
-correspondingly different syntactic convention, since installed package
-IDs are permitted to contain colons).  Why does GHC prefer package keys?
-It is the preferred internal format (since it is used for type
-identity), and converting from installed package IDs to package keys is
-not possible until the package database is loaded, which occurs after
-package flag parsing.}
+\section{GHC}
 
 \subsection{Signatures}
 
-Backpack introduces a new type of file, \texttt{hsig} files, which
-represent signatures for Haskell modules.  A signature can be used
-to type-check client code which uses a module (without the module
+An \texttt{hsig} file represents a (type) signature for a Haskell
+module, containing type signatures, data declarations, type classes,
+type class instances, but not 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.)
-
-The syntax of an \texttt{hsig} file is similar to an \texttt{hs-boot}
-file.  Value definitions are not permitted, but you can write type
-signatures, data declarations, type classes and type class instances.
-At the moment, data families and type families are not supported.  Here
-is an example of a module signature representing an abstract map type:
+signature (without a client implementation.)} The syntax of an
+\texttt{hsig} file is similar to an \texttt{hs-boot} file.  Here is an
+example of a module signature representing an abstract map type:
 
 \begin{verbatim}
 type role Map nominal representational
@@ -77,24 +51,30 @@ instance Functor (Map k)
 empty :: Map k a
 \end{verbatim}
 
-An \texttt{hsig} file can be processed by GHC with or without a backing
-implementation.
+An \texttt{hsig} file can either be type-checked or compiled against some
+\emph{backing implementation}, an \texttt{hs} module which provides all
+of the declarations that a signature advertises.
 
-\paragraph{Typechecking only} When no backing implementation is provided, we are
-only able to generate an interface file for the module, as in the
-following command:
+\paragraph{Typechecking} A signature file can be type-checked in the same
+way as an ordinary Haskell file:
 
 \begin{verbatim}
 $ ghc -c Map.hsig -fno-code -fwrite-interface
 \end{verbatim}
 
-By default, this generated interface file has a \emph{fresh} original
-names for everything in the signature. For example, in our
-previous example, the default original name of \texttt{Map} compiled as
-a signature is \texttt{main:Map.Map} (even if, say, eventually, you
-discover that in fact the original name is
-\texttt{containers\_KEY:Data.Map.Map}.)  You can also explicitly specify what
-original name should be assigned to some data types, as follows:
+This procedure generates an interface file, which can be used to type
+check other modules which depend on the signature, even if no backing
+implementation is available.  By default, this generated interface file
+is given \emph{fresh} original names for everything in the signature.
+For example, if \texttt{data T} is defined in two signature files
+\texttt{A.hsig} and \texttt{B.hsig}, they would not be considered
+type-equal, and could not be used interconvertibly, even if they
+had the same structure.
+
+\begin{color}{red}
+To explicitly specify what original name should be assigned (e.g.,
+to make the previous example type-equal) the \texttt{-shape-of} flag
+can be used:
 
 \begin{verbatim}
 $ ghc -c Map.hsig -shape-of "Map is containers_KEY:Data.Map.Map" \
@@ -102,36 +82,204 @@ $ ghc -c Map.hsig -shape-of "Map is containers_KEY:Data.Map.Map" \
 \end{verbatim}
 
 \texttt{-shape-of} is comma separated list of \texttt{name is origname}
-pairs, which overrides the original name specified in the new interface
-file.  \Red{At the moment, \texttt{-shape-of} is not implemented, and the syntax
-is not finalized.}
+entries, where \texttt{name} is an unqualified name and
+\texttt{origname} is an original name, of the form
+\texttt{package\_KEY:Module.name}, where \texttt{package\_KEY} is a
+package key identifying the origin of the identifier (or a fake
+identifier for a symbol whose provenance is not known).  Each instance
+of \texttt{origname} in the signature is instead assigned the original
+name \texttt{origname}, instead of the default original name.
+
+(TODO: This interface will work pretty poorly with \texttt{--make})
+\end{color}
+
+\paragraph{Compiling} We can specify a backing implementation for
+a signature and compile the signature against it using the
+\texttt{-sig-of} flag:
+
+\begin{verbatim}
+$ ghc -c Map.hsig -sig-of "package_KEY:Module"
+\end{verbatim}
+
+The \texttt{-sig-of} flag takes as an argument a module, specified
+as a package key, a colon, and then the module name.  \Red{This module
+must be a proper, \texttt{exposed-module}, and not a reexport or
+signature.}
+
+Compilation of a signature entails two things.  First, a consistency
+check is performed between the signature and the backing
+implementation, ensuring that the implementation accurately implements
+all of the types in the signature.  For every declaration in the
+signature, there must be an equivalent one in the backing implementation
+with an identical type (this check is quite similar to the one used
+for \texttt{hs-boot}).  Second, an interface file is generated
+which reexports the set of identifiers from the backing
+implementation that were specified in the signature. A file which
+imports the signature will use this interface file.\footnote{This
+interface file is similar to a module which reexports identifiers
+from another module, except that we also record the backing implementation
+for the purpose of handling imports, described in the next section.}
+
+\subsection{Extended format in the installed package database}
+
+After a set of Haskell modules has been compiled, they can be registered
+in the installed package database so that their exposed modules and
+signatures can be made available for import using the \texttt{-package}
+flag.  An entry in the installed package database specifies what modules
+and signatures from the package itself are exposed. It can also
+re-export modules and signatures from other packages.\footnote{Signature
+reexports are essential for creating signature packages in a modular
+way; module reexports are very useful for backwards-compatibility
+packages and also taking an package that has been instantiated multiple
+ways and giving its modules unique names.}
+
+There are three fields of an entry in the installed package database of note.
+
+\begin{color}{red}
+
+First, the \texttt{exposed-modules} field is a comma-separated list of
+module names, possibly with two extra, optional pieces of information
+about the module in question: what the \emph{original module/signature}
+is (if it is a reexport)\footnote{Knowing the original module/signature
+makes it possible for GHC to directly load the interface file, without
+having to follow multiple hops in the package database.}, and what the
+\emph{backing implementation} is (if it is a signature)\footnote{Knowing
+the backing implementation makes it possible to tell if an import is
+unambiguous without having to load the interface file first.}.
+
+\begin{verbatim}
+exposed-modules:
+    A,                              # original module
+    B from ipid:B,                  # reexported module
+    C is ipid:CImpl,                # exposed signature
+    D from ipid:D is ipid:DImpl,    # reexported signature
+    D from ipid:D2 is ipid:DImpl    # duplicates can be OK
+\end{verbatim}
 
+If no reexports or signatures are used, the commas can be omitted
+(making this syntax backwards compatible with the original syntax.)
+
+Entries to the installed package database are registered using \texttt{ghc-pkg}.
+\texttt{ghc-pkg} validates that all entries in \texttt{exposed-modules} are
+unambiguous; the criterion for which we will establish in the next section.\footnote{Note
+that this does mean duplicates can be allowed in some circumstances.  This is most useful
+when combining multiple signatures together.}
+
+TODO: What is currently implemented is
+that \texttt{reexported-modules} has a seperate field, where the
+original module is always set and backing implementation is always empty.
+I came to this generalization when I found I needed to add support for
+signatures and reexported signatures.  An alternate design is just to
+have a separate list for every parameter: however, we end up with a lot
+of duplication in the validation and handling code GHC side.  I do like
+the parametric approach better, but since the original
+\texttt{exposed-modules} was space separated, there's not an easy way to
+extend the syntax in a backwards-compatible way.  The current proposal
+suggests we add the comma variant because it is unambiguous with the old
+syntax.
+\end{color}
+
+Second, the \texttt{instantiated-with} field records the \emph{original
+module} which instantiated any holes associated with a package (i.e.,
+what \texttt{-sig-of} parameter was used during compilation.)
 
-\paragraph{Compilation}  A backing implementation can be specified
-using the \texttt{-sig-of} flag:
+Finally, the \texttt{key} field records the \emph{package key} of a
+package.  A package key is an opaque identifier identifying a package
+which serves as the basis for type identity and linker
+symbols.\footnote{Informally, you might think of a package as a package
+name and its version, e.g., \texttt{containers-0.9}; however, sometimes,
+it is necessary to distinguish between installed instances of a package
+with the same name and version which were compiled with different
+dependencies.} \footnote{The package key is different from an
+\emph{installed package ID}, which is a more fine-grained identifier for
+a package.  Identical installed package IDs imply identical package
+keys, but not vice versa.  However, within a single run of GHC, we
+enforce that package keys and (non-shadowed) installed package IDs are
+in one-to-one correspondence.}
+
+The package key is programatically generated by Cabal\footnote{In
+practice, a package key looks something like
+\texttt{conta\_GtvvBIboSRuDmyUQfSZoAx}.  In this document, we'll use
+\texttt{containers\_KEY} as a convenient shorthand to refer to some
+package key for the \texttt{containers} package.}; while GHC has no say
+in the generation process,  Cabal's must choose distinct package keys if
+any of the following fields in the installed package database are
+distinct:
+
+\begin{itemize}
+\item \texttt{name} (e.g., \texttt{containers})
+\item \texttt{version} (e.g., \texttt{0.8})
+\item \texttt{depends} modulo package keys
+\item \texttt{instantiated-with} modulo package keys
+\end{itemize}
+
+\subsection{Module thinning and renaming}
+
+The \texttt{-package} flag and its variants (\texttt{-package-id} and
+\texttt{-package-key}) now support ``thinning and renaming''
+annotations, which allows a user to selectively expose only certain
+modules from a package, possibly under different names.\footnote{This
+feature has utility both with and without Backpack.  The ability to
+rename modules makes it easier to deal with third-party packages which
+export conflicting module names; under Backpack, this situation becomes
+especially common when an indefinite package is instantiated multiple
+time with different dependencies.}
+
+The command line flag \texttt{-package pkgname} causes all
+exposed modules of \texttt{pkgname} to become visible under their
+original names for imports.  Thinning and renaming can be applied
+using the extended syntax \texttt{-package "pkgname
+(rns)"}, where \texttt{rns} is a comma separated list of
+module renamings \texttt{OldName as NewName}.  Bare module names are
+also accepted, where \texttt{Name} is shorthand for \texttt{Name as
+Name}.  A package exposed this way only causes modules (specified before
+the \texttt{as}) explicitly listed in the renamings to become visible
+under their new names (specified after the \texttt{as}).  For example,
+\texttt{-package "containers (Data.Set, Data.Map as Map)"} makes
+\texttt{Data.Set} and \texttt{Map} (pointing to
+\texttt{Data.Map}) available for import.\footnote{See also Cabal files
+for a twist on this syntax.}
+
+When the \texttt{-hide-all-packages} flag is applied, uses of the
+\texttt{-package} flag are \emph{cumulative}; each argument is processed
+and its bindings added to the global module map.  For example,
+\texttt{-hide-all-packages -package containers -package "containers
+(Data.Map as Map)"} brings both the default exposed modules of
+containers and a binding for \texttt{Map} into scope.\footnote{The
+previous behavior, and the current behavior when
+\texttt{-hide-all-packages} is not set, is for a second package flag for
+the same package name to override the first one.}\footnote{We defer
+discussion of what happens when a module name is bound multiple times until
+we have discussed signatures, which have interesting behavior on this front.}
+
+\subsection{Disambiguating imports}
+
+With module thinning and renaming, as well as the installed package
+database, it is possible for GHC to have multiple bindings for a single
+module name.  If the bindings are ambiguous, GHC will report an error
+when the user attempts to use the identifier.
+
+Define the \emph{true module} associated with a binding to be the
+backing implementation, if the binding is for a signature,\footnote{This
+implements signature merging, as otherwise, we would not necessarily
+expect original signatures to be equal} and the original module
+otherwise.  A binding is unambiguous if the true modules of all the
+bindings are equal.  Here is an example of an unambiguous set of exposed
+modules:
 
 \begin{verbatim}
-$ ghc -c Map.hsig -sig-of "containers_KEY:Data.Map"
+exposed-modules:
+    A from pkg:AImpl,
+    A is pkg:AImpl,
+    A from other-pkg:Sig is pkg:AImpl
 \end{verbatim}
 
-GHC does two things in this case.  First, it does a consistency check
-between the signature and the original implementation and makes sure
-that the implementation accurately implements all of the types in the
-signature.  This is a simple, width-subtyping check, nearly identical to
-the check used by \texttt{hs-boot}.  Second, it generates an interface
-file which reexports the set of identifiers from the original
-implementation that were specified in the signature.  Any files which
-import the signature (as opposed to the implementation) will use this
-interface file to find relevant implementations, in the same way that
-modules today can reexport identifiers from other modules.
-
-\paragraph{Imports} An import of a signature operates in much the same
-way as ordinary imports.  When a source file imports two modules with
-conflicting identifiers, we report an error when a user attempts to use
-such an ambiguous identifier.  However, if the identifiers have the same
-original name, the import is unambiguous.  Similarly for signatures, if
-a user imports two signature files exporting the same name, we will only
-report an error if the identifiers have conflicting original names.\footnote{This implements ``signature merging'' as described by the original Backpack paper; notably, it was not necessary to synthesize a new interface file for the combined signature.}
+This mapping says that this package reexports \texttt{pkg:AImpl} as
+\texttt{A}, has an \texttt{A.hsig} which was compiled against
+\texttt{pkg:AImpl}, and reexports a signature from \texttt{other-pkg}
+which itself was compiled against \texttt{pkg:AImpl}.
+
+Here are some more examples:
 
 \begin{verbatim}
 $ cat > AImpl.hsig
@@ -163,17 +311,15 @@ $ ghc -c Main.hs
 FAILS due to ambiguous original name
 \end{verbatim}
 
-There is a twist, however: when we are only type-checking, GHC
-performs an \emph{additional} check and ensure that identifiers with the
-same original names originating from different signature files have
-compatible types: e.g.  \texttt{foo} from \texttt{ASig} and \texttt{foo}
-from \texttt{BSig} have the same type. (This also applies to type
-definitions, etc.)  This is because the \texttt{-shape-of} flag could be
-used to cause two incompatible definitions to be given the same original
-name.  This check is not necessary during compilation, because
-\texttt{-sig-of} will ensure that the signatures are compatible with a
-common, unique backing implementation.  \Red{The additional check is not implemented yet.}
+\paragraph{Typechecking}  \Red{When typechecking only, there is not
+necessarily a backing implementation associated with a signature.  In
+this case, even if the original names match up, we must perform an
+\emph{additional} check to ensure declarations have compatible types.}
+This check is not necessary during compilation, because \texttt{-sig-of}
+will ensure that the signatures are compatible with a common, unique
+backing implementation.
 
+\begin{color}{red}
 \begin{verbatim}
 $ ghc -c ASig.hsig -fno-code -fwrite-interface
 $ ghc -c BSig.hsig -fno-code -fwrite-interface
@@ -199,119 +345,115 @@ $ ghc -c BSig.hsig -shape-of "foo is main:AImpl" -fno-code -fwrite-interface
 $ ghc -c Main.hs -fno-code -fwrite-interface
 FAILS due to mismatchng types
 \end{verbatim}
+\end{color}
 
-\subsection{Compiled external packages}
-
-This subsection concerns external packages which have been fully compiled.
-They may have had some abstract signatures, but those signatures were
-filled with implementations before installation to the package database.
-
-\paragraph{Installed package database}
-The format of packages in the installed package database has been
-generalized to support exposed signatures and module/signature
-reexports.  Previously, installed package info recorded
-\texttt{exposed-modules} and \texttt{hidden-modules}: exposed modules
-provided a list of modules that should be added to the module import map
-for processing \texttt{import} statements, whereas hidden modules was a
-purely documentary mechanism to let users know if they attempted to
-import a hidden module (rather than just saying the module didn't exist
-at all.)
-
-With Backpack, \texttt{exposed-modules} has been generalized to record
-two extra, optional pieces of information about the module in question:
-what the \emph{original module/signature} is (if it is a reexport), and
-what the \emph{backing implementation} is (if it is a signature).
-
-\begin{verbatim}
-exposed-modules:
-    A,                              # original module
-    B from ipid:B,                  # reexported module
-    C is ipid:CImpl,                # exposed signature
-    D from ipid:D is ipid:DImpl,    # reexported signature
-    D from ipid:D2 is ipid:DImpl    # duplicates can be OK
-\end{verbatim}
-
-If no reexports or signatures are used, the commas can be omitted
-(making this syntax backwards compatible with the original syntax.)
-
-\texttt{ghc-pkg}, when processing this field, does a simple validation
-that, for any duplicate exposed modules, their backing implementation
-or original module if there is no backing implementation must be equal.
-
-\Red{All of this is not implemented.  What is currently implemented is
-that \texttt{reexported-modules} has a seperate field, where the
-original module is always set and backing implementation is always empty.
-I came to this generalization when I found I needed to add support for
-signatures and reexported signatures.  An alternate design is just to
-have a separate list for every parameter: however, we end up with a lot
-of duplication in the validation and handling code GHC side.  I do like
-the parametric approach better, but since the original
-\texttt{exposed-modules} was space separated, there's not an easy way to
-extend the syntax in a backwards-compatible way.  The current proposal
-suggests we add the comma variant because it is unambiguous with the old
-syntax.}
-
-\Red{Breadcrumb for abandoned design path: at one point, simonpj proposed
-that we not only allow duplicate signatures, but also duplicate implementations.
-We decided later that there was no compelling use-case for this functionality
-at the moment.}
-
-\paragraph{External imports}
-In order to support imports of modules which are not in the home package
-(modules that are currently being compiled), GHC builds a mapping from module
-names to implementations based on the exposed packages. Previously, if
-two exposed packages attempted to create a mapping for the same name,
-this resulted in ambiguity.
-
-With signatures and reexports, some collisions are now no longer
-considered ambiguous and trigger different behavior when their name is
-imported.  Specifically, define the \emph{true module} of a package export
-to be the backing implementation, if the module is a signature, or the
-original module otherwise.  For any module name, we consider the set of
-mappings for it to be \emph{unambiguous} if all of their true modules
-are equal.  Here is an example of an unambiguous set of mappings:
-
-\begin{verbatim}
-exposed-modules:
-    A from pkg:AImpl,
-    A is pkg:AImpl,
-    A from other-pkg:Sig is pkg:AImpl
-\end{verbatim}
-
-This mapping says that this package reexports \texttt{pkg:AImpl} as
-\texttt{A}, has an \texttt{A.hsig} which was compiled against
-\texttt{pkg:AImpl}, and reexports a signature from \texttt{other-pkg}
-which itself was compiled against \texttt{pkg:AImpl}.
-
-When there are multiple, unambiguous mappings for a module name, which
-interface do we load when we actually \texttt{import} it?  If any
-mapping in the set is an implementation (\texttt{hs} file), we just use
-the interface of the true module (it doesn't matter which mapping, since
-they are all equivalent).  Otherwise, we load the interface files of
-\emph{all} the signatures, as if there were multiple import statements.
-For example, if package \texttt{a} and package \texttt{b} both offer
-exposed signatures for \texttt{ASig}, then if I \texttt{import ASig}
-with both packages exposed, it is equivalent to having said:
-
-\begin{verbatim}
-import "a" ASig
-import "b" ASig
-\end{verbatim}
-
-\Red{Behavior for signatures is not implemented yet.}
+\Red{EDITORS CUT HERE}
 
 \subsection{Indefinite external packages}
 
-\Red{This is not implemented yet.}
+\Red{Not implemented yet.}
 
 \section{Cabal}
 
-\subsection{Cabal file syntax}
-
-\subsection{Setup new flags}
+\subsection{Reexports and signatures}
+
+The Cabal file is a user-facing description of a package, which is
+processed into an \texttt{InstalledPackageInfo} by Cabal.  Currently,
+package authors use \texttt{exposed-modules} in the \texttt{library}
+section to specify what \texttt{hs} modules are available for import
+when the package is exposed.  Backpack extends the Cabal files with four
+new fields:
+
+\paragraph{reexported-modules}  A comma-separated list of module or
+signature reexports.  It is represented in the installed package
+database as an module with a non-empty original module/signature: the
+original module is resolved by Cabal.  There are three valid syntactic
+forms:
+
+\begin{itemize}
+    \item \texttt{Orig}, which reexports any module with the
+    name \texttt{Orig} in the current scope (e.g.,
+    as specified by \texttt{build-depends}).
+
+    \item \texttt{Orig as New}, which reexports a module with
+    the name \texttt{Orig} in the current scope.  \texttt{Orig}
+    can be a home module and doesn't necessarily have to come
+    from \texttt{build-depends}.
+
+    \item \texttt{package:Orig as New}, which reexports a module
+    with name \texttt{Orig} from the specific source package \texttt{package}.
+\end{itemize}
+
+If multiple modules with the same name are in scope, we check
+if it is unambiguous (the same check used by GHC); if they are
+we reexport all of the modules; otherwise, we give an error.
+In this way, packages which reexport multiple signatures to the
+same name can be valid; a package may also reexport a signature
+onto a home \texttt{hsig} signature.
+
+\paragraph{required-signatures}  A space-separated list of module names
+specifying internal signatures (in \texttt{hsig} files) of the package.
+This field is analogous to \texttt{other-modules}, but with signatures.
+Signatures specified in this field can be imported by other home
+modules, but are not registered in the installed package database and
+available for external import.  In order for this package to be
+compiled, implementations for all these signatures must be provided (see
+the section on \texttt{Setup}).
+
+\paragraph{exposed-signatures}  A space-separated list of module names
+specifying externally visible signatures (in \texttt{hsig} files) of the package.  It is
+represented in the installed package database as a module with a
+non-empty backing implementation.  Signatures exposed in this way are
+available external import.  In order for this package to be compiled,
+implementations for all these signatures must be provided (see the
+section on \texttt{Setup}).
+
+\paragraph{indefinite}  A package is \emph{indefinite} if it has any
+\texttt{required-signatures} or \texttt{exposed-signatures}, or it
+transitively depends on an indefinite package whose signatures have
+not been instantiated.  In principle, this parameter can be calculated
+by Cabal, but serves a documentory purpose for packages which do not
+have any signatures themselves, but depend on packages which do (without
+providing implementations for those signatures.)
 
 \subsection{Package key generation}
 
+The algorithm Cabal uses in order to calculate what 
+
+\subsection{build-depends}
+
+This field has been extended with new syntax
+to provide the access to GHC's new thinning and renaming functionality
+and to have the ability to include an indefinite package \emph{multiple times}
+(with different instantiations for its holes).  Renaming is the
+\emph{primary} mechanism by which holes are instantiated in a mix-in module
+system, however, this instantiation only occurs when running \texttt{cabal-install}.
+
+Here is an example entry in \texttt{build-depends}: \texttt{foo >= 0.8
+(ASig as A1, B as B1; ASig as A2, ...)}.  This statement includes the
+package \texttt{foo} twice, once with \texttt{ASig} instantiated with
+\texttt{A1} and \texttt{B} renamed as \texttt{B1}, and once with
+\texttt{ASig} instantiated with \texttt{A2}, and all other modules
+imported with their original names.  Assuming that the key of the first
+instance of \texttt{foo} is \texttt{foo\_KEY1} and the key of the second instance
+is \texttt{foo\_KEY2}, and that \texttt{ASig} is an \texttt{exposed-signature}, then this \texttt{build-depends} would turn into
+these flags for GHC: \texttt{-package-key "foo\_KEY1 (ASig as A1, B as B1)" -package-key "foo\_KEY2" -package-key "foo\_KEY2 (ASig as A2)"}
+
+Syntactically, the thinnings and renamings are placed inside a
+parenthetical after the package name and version constraints.
+Semicolons distinguish separate inclusions of the package, and the inner
+comma-separated lists indicate the thinning/renamings of the module.
+You can also write \texttt{...}, which simply
+includes all of the default bindings from the package.
+\Red{This is not implemented. Should this only refer to modules which were not referred to already? Should it refer only to holes?}
+
+There are two marks that should be made about separate instantiations of
+the package.  First, Cabal will automatically ``de-duplicate'' instances of
+the package which are equivalent: thus, \texttt{foo (A; B)} is equivalent to
+\texttt{foo (A, B)} when \texttt{foo} is a definite package, or 
+
+\subsection{Setup new flags}
+
 \subsection{Metadata in the installed package database}
 
 Cabal records