[docs/backpack] Get lint to stop complaining
[ghc.git] / docs / backpack / backpack-impl.tex
index 99fb832..46e397f 100644 (file)
@@ -275,11 +275,11 @@ Backpack proper can be implemented.  These additions are described in
 red in the architectural diagrams.  The current structure of this
 section is to describe the additions bottom up.
 
-\subsection{Concrete physical identity = PackageId$^*$ + Module name}\label{sec:ipi}
+\subsection{Concrete physical identity = PackageId + Module name + Module dependencies}\label{sec:ipi}
 
 \begin{figure}
     \center{\begin{tabular}{r l}
-        PackageId & hash of ``package name, package version, dependency resolution, module environment'' \\
+            PackageId & hash of ``package name, package version, dependency resolution, \emph{module} environment'' \\
         InstalledPackageId & hash of ``PackageId, source code, way, compiler flags'' \\
     \end{tabular}}
 \label{fig:proposed-pkgid}\caption{Proposed new structure of package identifiers.}
@@ -290,27 +290,32 @@ In Backpack, there needs to be some mechanism for assigning
 typechecking Backpack packages, since they let us tell if two types are
 equal or not.
 
-If it looks like a duck and quacks like a duck, it is a duck.  In GHC,
-our method of testing whether or not two types are equal is by comparing
-their original names, which is a tuple of a PackageId and the module
-name.  Furthermore, we rely on ``module name'' to be some user visible
-string which they can refer to in error messages\footnote{I wonder what
-happens when you start renaming module names\ldots}, so really our only
-degree of freedom is modifying the PackageId associated with a module.
-What changes to the PackageId are necessary?
-
-Fortunately, in current Cabal packages, we require that modules always
-be given a package-unique module name, thus it's not necessary to
-disambiguate between multiple ``module literals'', as was the case in
-Paper Backpack.  However, current PackageIds are insufficient for
-another reason: a module physical identity is not just its name, but
-also the regular tree representing all of its \emph{module} dependencies.  The
-PackageId needs to include this regular tree, \emph{which may differ
-between modules in the same package (Section~\ref{sec:flatten})}, along with the
-other information about the package such as its name. (I think
-Figure~\ref{fig:proposed-pkgid} is out of date now.)  Since this tree in
-general may be quite long, it needs to be shortened in some way, such as
-by hashing.
+In GHC, our method of testing whether or not two types are equal is by
+comparing their original names, which is a tuple of a PackageId and the
+module name (summarized in Figure~\ref{fig:current-pkgid}).  If it looks
+like a duck and quacks like a duck, it is a duck: we might reasonable
+imagine that \emph{concrete physical identity = PackageId and module
+name}.  But is this sufficient to represent Backpack's physical module
+identities?
+
+If we look at how physical module identities are allocated in Paper Backpack,
+we can see that each module corresponds to an identity constructor (in
+Backpack this is the package name, some representation of the module
+source, and a disambiguating integer if module source is duplicated)
+\emph{as well as} physical module identities which were applied to
+this constructor.  The current PackageId + Module name scheme adequately encodes
+the constructor (in particular, a single package can't have multiple modules
+with the same name), but it does not encode the \emph{module} dependencies.
+We have to add these to our original names.  There are three ways we can do
+this:
+
+\begin{enumerate}
+    \item Augment original names to have a third component.  This is less than ideal because it requires pervasive changes to all parts of the compiler.
+    \item Augment the module name to record module dependency information.  This is a bit of an odd place to put the information, because our module names correspond quite concretely to the actual source file a user wrote some source in.
+    \item Augment the PackageId to record module dependency information.  For now, this is the regime we will use; however, see Section~\ref{sec:flatten} for why the issue is more subtle.
+\end{enumerate}
+
+(XXX Figure~\ref{fig:proposed-pkgid} is out of date now.)
 
 And now, the complications\ldots
 
@@ -384,12 +389,13 @@ we talk about packages with holes.
 
 \subsection{Flatten the package database}\label{sec:flatten}
 
-In the previous section, I implied that the \emph{module dependency regular
-tree} needed to be placed in the \emph{package ID}.  Type error? Yes!
+In the previous section, I implied that the \emph{module} dependencies
+could be recorded with the \emph{package} ID\@.  Type error? Yes!
 
-The upshot is that in some cases, compilations of separate packages may
-result in the installation of code that should be the \emph{same} (code
-that is shared at the module level, rather than the package level).
+In the old world order, we think of dependencies as being associated with
+packages as a whole.  However, Paper Backpack specifies dependency tracking
+at the \emph{module} level, which means that different compilations of
+an indefinite package may result in modules which should be identified.
 Here is a Backpack package which demonstrates the issue:
 
 \begin{verbatim}
@@ -428,12 +434,12 @@ versions of \verb|Q|).  The upshot is that we are in an awkward position,
 where package \verb|a| contains some modules which must be distinct, and other
 modules which must be unified over several installs.
 
-The solution to this conundrum is to flatten the package database, so
-that we no longer insist that all compiled code associate with a package
-live together in a single directory: instead, \emph{the installed
-    package database is a directory of physical module identities to
-objects/interfaces}.  Installed packages are represented as (possibly
-overlapping) sets over this store of modules.
+The theory, thus, demands that we flatten the package database, so that
+we no longer insist that all compiled code that is produced when a
+package is installed live together in a single directory: instead,
+\emph{the installed package database is a directory of physical module
+identities to objects/interfaces}.  Installed packages are represented
+as (possibly overlapping) sets over this store of modules.
 
 \paragraph{Do we really care about this use case?}  Scott gave me one
 good argument why this is a nice feature to have: it permits users to
@@ -472,16 +478,23 @@ interaction could still be surprising: Backpack can remodularize modules, but
 it can't remodularize values inside a module, so if a module has a dependency
 but some global state in the module doesn't, the resulting behavior can be
 surprising.  Perhaps the moral of the story really is, ``Don't do side effects
-in an applicative module system! No really!''}
+in an applicative module system! No really!''} \\
 
-\paragraph{Package slicing} Another possibility is to automatically
+\subsection{Alternatives to flattening package DB}
+Flattening can be seen as one of four different representations of packages
+at the OS/library level. While it promotes maximal sharing of identical
+modules, it is perhaps too fine-grained for most purposes.
+\emph{ToDo: Describe the alternatives.}
+
+\paragraph{Package slicing} Instead of changing the package database,
+we automatically
 slice a single package into multiple packages, so that the sliced
 packages have dependencies which accurately reflect their constitutent
 modules.  For a well modularized package, the slicing operation should
 be a no-op.  This would also be useful in some other situations (see the
 \verb|-module-env| discussion in Section~\ref{sec:compiling-definite}).
 In fact, which slice a module should be placed in can be automatically
-calculated by taking the package identity with the regular tree
+calculated by taking the package name with the regular tree
 associated with the module (Section~\ref{sec:ipi}).
 
 A minor downside of package slicing is in a dynamically linked environment,
@@ -502,7 +515,8 @@ Our motivating example, then, would fail to witness sharing.
 
 This might be the simplest thing to do, but it is a change in the
 Backpack semantics, and rules out modularization without splitting a package
-into multiple packages.
+into multiple packages.  Maybe Scott can give other reasons why this
+would not be so good.  SPJ is quite keen on this plan.
 
 \subsection{Exposed modules should allow external modules}\label{sec:reexport}
 
@@ -557,7 +571,7 @@ same message.  This is especially true when renaming is in place:
 you not only want to print out the name in scope, but probably some indication
 of what the original name is.  In short, when it comes to error messages, tread with care!
 
-\section{Simplifying Backpack}\label{sec:simplifying-backpack}
+\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.
@@ -570,15 +584,17 @@ implementation problems:
     \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.
+        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, which makes it a slightly more expensive
+        version of \verb|ghc -M|.)
 
     \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 also means
-        that either GHC must compile an entire package in one go, or it
-        must first do a shaping pass, and then revisit every module and
+        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
@@ -598,11 +614,14 @@ implementation problems:
         code without recursive dependencies. Programmers should avoid
         this code organization, except when it is absolutely necessary.
 
-    \item \emph{GHC is architecturally ill-suited for 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.
+    \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}
 
@@ -622,8 +641,8 @@ 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!)
 
-So, if we want to jettison the shaping analysis, we'd like a subset
-of Backpack which does not allow mutually recursive modules.
+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
@@ -792,6 +811,8 @@ implementation, we can skip the compilation process and reuse the version.
 This is because the calculated \verb|BDEPS| will be the same, and thus the package
 IDs will be the same.
 
+XXX ToDo: actually write down pseudocode algorithm for this
+
 \paragraph{Module environment or package flags?}  In the previous
 section, I presented two ways by which one can tweak the behavior of
 GHC's module finder, which is responsible for resolving \verb|import B|
@@ -856,15 +877,108 @@ package pkg-d where
 when it is compiled by itself, it will generate its own instance of B,
 even though it should be the same as C.  This is bad news.
 
+\subsection{Restricted recursive modules ala hs-boot}\label{sec:hs-boot-restrict}
+
+It should be possible to support GHC-style mutual recursion using the
+Backpack formalism immediately using hs-boot files.  However, to avoid
+the need for a shaping pass, we must 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.
+
+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.
+
+\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 ponit.
+
+\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}
 
-When we are typechecking a package that contains some holes, some extra
-care must be taken.  We can no longer assume that there are no holes in
-the physical context, and while 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.)
+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:
 
@@ -923,7 +1037,7 @@ package r where
     include q
 \end{verbatim}
 
-Another possibility is that it might be acceptable to do a small shaping
+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:
@@ -940,8 +1054,10 @@ 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). See Section~\ref{sec:hs-boot-restrict}
-for more details.
+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}
 
@@ -966,6 +1082,42 @@ 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{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
@@ -994,33 +1146,6 @@ 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.
 
-\subsection{Restricted recursive modules ala hs-boot}\label{sec:hs-boot-restrict}
-
-It should be possible to support GHC-style mutual recursion using the
-Backpack formalism immediately using hs-boot files.  However, to avoid
-the need for a shaping pass, we must 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}.  We then
-compile modules as usual, but compiling against the signature as if it
-were an hs-boot file.
-
-(ToDo: Figure out why this eliminates the shaping pass)
-
-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.
-
-\subsection{In defense of shaping}
-
-In the introduction to this section, we argued that for the vast
-majority of programs, having to run a shaping pass would be
-onacceptable.  In this section, I attempt to debunk those claims,
-and argue that, actually, we should have a shaping pass.
-
-(XXX But I have not written this section yet.)
-
 \section{Surface syntax}
 
 In the Backpack paper, a brand new module language is presented, with
@@ -1087,8 +1212,10 @@ all of the signatures and modules are placed in appropriately
 named files):
 
 \begin{verbatim}
+package: libfoo
+...
 build-depends: base, libfoo (Foo, Bar as Baz)
-holes: A A2
+holes: A A2 -- deferred for now
 exposed-modules: Foo B C
 aliases: A = A2
 other-modules: D
@@ -1099,24 +1226,136 @@ 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:
+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 Run Cabal's constraint solver to determine which specific
-        packages we will depend on (i.e., resolve the names in \verb|build-depends|).
-        For each package $p$ in this order, record a \verb|include p| in
-        the Backpack package.  Because of the topological sorting, every
-        included package has all of its holes filled in upon inclusion,
-        preserving the linking invariant.
-    \item (XXX something wonderful)
+
+    \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}
 
-\paragraph{Thinning and renaming}  The elaboration above is over-simplified,
-because it cannot deal with thinning and renaming.  The obvious choice of
-simply taking the thinning/renaming and slapping it on the include does not
-work, because this renaming will affect 
+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}  The proposal 
+\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
@@ -1124,7 +1363,94 @@ 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}
+\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{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.
+
+\subsection{Type families}
+
+Like type classes, type families must not overlap (and this is a question of
+type safety!)
+
+A more subtle question is compatibility and apartness of type family
+equations.  Under these checks, aliasing of modules can fail if it causes
+two type families to be identified, but their definitions are not apart.
+Here is a simple example:
+
+\begin{verbatim}
+A :: [
+    type family F a :: *
+    type instance F Int = Char
+]
+B :: [
+    type family F a :: *
+    type instance F Int = Bool
+]
+\end{verbatim}
+
+Now it is illegal for \verb|A = B|, because when the type families are
+unified, the instances now fail the apartness check.  However, if the second
+instance was \verb|F Int = Char|, the families would be able to link together.
+
+To make matters worse, an implementation may define more axioms than are
+visible in the signature:
+
+\begin{verbatim}
+package a where
+    A :: [
+        type family F a :: *
+        type instance F Int = Bool
+    ]
+package b where
+    include a
+    B = [
+        import A
+        type instance F Bool = Bool
+        ...
+    ]
+package c where
+    A = [
+        type family F a :: *
+        type instance F Int = Bool
+        type instance F Bool = Int
+    ]
+    include b
+\end{verbatim}
+
+It would seem that private axioms cannot be naively supported. Is
+there any way that thinning axioms could be made to work?
 
 \section{Open questions}\label{sec:open-questions}