Definite compilation is a go

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

1 files changed, 412 insertions, 145 deletions

diff --git a/docs/backpack/backpack-impl.tex b/docs/backpack/backpack-impl.tex
index c34e3cb051..c29ec8a7c4 100644
--- a/docs/backpack/backpack-impl.tex
+++ b/docs/backpack/backpack-impl.tex
@@ -11,6 +11,8 @@
 \usepackage{color}
 \usepackage{footnote}
 \usepackage{float}
+\usepackage{algorithm}
+\usepackage{algpseudocode}
 \usetikzlibrary{arrows}
 \usetikzlibrary{positioning}
 \setlength{\droptitle}{-6em}
@@ -29,6 +31,8 @@
 
 \input{commands-rebindings.tex}
 
+\newcommand{\var}[1]{\textsf{#1}}
+
 \newcommand{\ghcfile}[1]{\textsl{#1}}
 
 \title{Implementing Backpack}
@@ -899,165 +903,164 @@ 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{Compilation of definite modules}\label{sec:compiling-definite}
-
-Of course, we still have to compile the code, and this includes any
-subpackages which we have mixed in the dependencies to make them fully
-definite.  Let's take the following set of packages as an example:
+\subsection{Compiling definite packages}
+
+% 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}$, $flags_H$}
+    \State$flags\gets \emptyset$
+    \State$\mathcal{K}$ $\gets$ \Call{Hash}{$P + \textsc{HoleInsts}(\vec{B}, flags_H)$}
+    \State$cwd\gets \textrm{fresh working directory for compilation}$
+    \For{$B$ \textbf{in} $\vec{B}$}
+        \Case{$p$ $\cc$ $p$\texttt{.hsig}}
+            \State\Call{Exec}{\texttt{ghc -sig} $p$\texttt{.hsig} $flags$ \texttt{-hole-flags} ``$flags_H$''}
+        \EndCase%
+        \Case{$p = p\texttt{.hs}$}
+            \State\Call{Exec}{\texttt{ghc -c} $p$\texttt{.hs} \texttt{-package-name} $\mathcal{K}$ $flags$}
+                  \Comment{}Nota bene\@: no $flags_H$!
+        \EndCase%
+        \Case{$p = p'$}
+            \State\Call{Exec}{\texttt{ghc -alias} $p$ $p'$}
+        \EndCase%
+        \Case{\Cinc{$P'$}}
+        \State$\mathcal{K}'\gets$ \Call{Compile}{$P'$, $flags_H$ $flags$ \texttt{-package-loc} $(\mathcal{K}\to cwd)$ \texttt{-package} $\mathcal{K}$}
+            \State$flags\gets flags$ \texttt{-package} $\mathcal{K}'$
+            \State\Call{Exec}{\texttt{ghc -check} $flags$}
+        \EndCase%
+        \Case{\Cinc{$P'$} $\langle \vec{p_H\mapsto p'_H}, \vec{p\mapsto p'} \rangle$}
+        \State$\mathcal{K}'\gets$ \Call{Compile}{$P'$, $flags_H$ $flags$ \texttt{-package-loc} $(\mathcal{K}\to cwd)$ \texttt{-reset-module-env} $\vec{p_H\mapsto p'_H}$}
+            \State$flags\gets flags$ \texttt{-package} $\mathcal{K}'$ $\langle\vec{p\mapsto p'}\rangle$
+            \State\Call{Exec}{\texttt{ghc -check} $flags$}
+        \EndCase%
+    \EndFor%
+    \State\Call{Exec}{\texttt{ghc-pkg copy \&\& ghc-pkg register}} \Comment{Records if $P$ exports a thinning}
+    \State\Return$\mathcal{K}$
+    \EndProcedure%
+\end{algorithmic}
+\end{algorithm}
+
+The full recursive procedure for compiling a Backpack package 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 algorith, line-by-line:
+
+\paragraph{The parameters} To compile a package description for package
+$P$, we need to know a list of $flags_H$, which are flags that are
+passed to \texttt{ghc} to let it know where to find the instantiated
+holes.  Logically, these flags determine a mapping from each hole's
+logical name $p_H$ to a physical module identity $\nu$; we accordingly
+use these flags at the very beginning of compilation to calculate the
+package key $\mathcal{K}$ of the package being compiled, using the
+pre-pass \textsc{HoleInsts}, which finds all of the holes defined in the
+package and looks up what would have been selected for each of them
+based on $flags_H$.  Why don't we pass the actual mapping? It's more
+convenient to use flags, because the flags may be much more compact than
+a full mapping.  (Of course, for the package key, we have to compute the
+true mapping, because the flags may contain spurious dependencies.)  We
+distinguish hole flags ($flags_H$), which are passed in as arguments,
+from flags ($flags$), which are accumulated as we include packages,
+although the reason for this distinction will not be clear until we
+consider the commands themselves.
+
+\subsection{Compiling signatures}
+
+Signature compilation uses a new compilation mode \verb|-sig|.  This
+mode is similar to the behavior of how we process \verb|hs-boot| files,
+but with one difference: we first check the environment as specified by
+$flags$ and $flags_H$ to see if there is already an \verb|hi| file
+(i.e., from an implementation) with the same logical name of this
+signature, e.g.,  as would occur compiling the marked signature in this
+example:
 
 \begin{verbatim}
-package pkg-a where
-    A = [ a = 0; b = 0 ] -- b is not visible
-    B = ... -- this code is ignored
-package pgk-b where -- indefinite package
-    A :: [ a :: Bool ]
-    B = [ import A; b = 1 ]
-package pkg-c where
-    include pkg-a (A)
-    include pkg-b
-    C = [ import B; ... ]
+package p where
+    A :: ...    -- *
+    B = [ import A; ... ]
+package q where
+    A = [ ... ]
+    include p
 \end{verbatim}
 
-Note: in the following example, we will assume that we are operating
-under the packaging scheme specified in Section~\ref{sec:one-per-definite-package}
-with the indefinite package refinement.
-
-With the linking invariant, we can simply walk the Backpack package ``tree'',
-compiling each of its dependencies.  Let's walk through it explicitly.\footnote{To simplify matters, we assume that there is only one instance of any
-PackageId in the database, so we omit the unique-ifying hashes from the
-ghc-pkg registration commands; we ignore the existence of version numbers
-and Cabal's dependency solver; finally, we do the compilation in
-one-shot mode, even though Cabal in practice will use the Make mode.}
+If there is, we check the implementation to ensure that it is compatible
+with the signature, and then we output a \texttt{hisig} 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
+\texttt{hisig} file, not the original one \texttt{hi} file.
 
-First, we have to build \verb|pkg-a|.  This package has no dependencies
-of any kind, so compiling is much like compiling ordinary Haskell.  If
-it was already installed in the database, we wouldn't even bother compiling it.
+\paragraph{Absence of an \texttt{hi} file}
+By default, if we find an appropriate \texttt{hi} file, we'll use it
+(even if there are other \texttt{hisig} files in the search path), but
+sometimes there won't be any immediate \texttt{hi}, as in this case:
 
 \begin{verbatim}
-ADEPS =    # empty!
-ghc -c A.hs -package-name pkg-a-ADEPS
-ghc -c B.hs -package-name pkg-a-ADEPS
-# install and register pkg-a-ADEPS
-\end{verbatim}
-
-Next, we have to build \verb|pkg-b|.  This package has a hole \verb|A|,
-intuitively, it depends on package A.   This is done in two steps:
-first we check if the signature given for the hole matches up with the
-actual implementation provided. Then we build the module properly.
-
-\begin{verbatim}
-BDEPS = "A -> pkg-a-ADEPS:A"
-ghc -c A.hs-boot -package-name pkg-b-BDEPS -hide-all-packages \
-    -package "pkg-a-ADEPS(A)"
-ghc -c B.hs      -package-name pkg-b-BDEPS -hide-all-packages \
-    -package "pkg-a-ADEPS(A)"
-# install and register pkg-b-BDEPS
+package p where
+    P :: [ x :: Int ]
+    A = P
+package q where
+    P :: [ x :: Int ]
+    include p
+    A :: [ x :: Int, y :: Int ] -- *
+package r where
+    P = [ x = 1; y = 1 ]
+    include q
 \end{verbatim}
 
-These commands mostly resemble the traditional compilation process, but
-with some minor differences.  First, the \verb|-package| includes must
-also specify a thinning (and renaming) list.  This is because when
-\verb|pkg-b| is compiled, it only sees module \verb|A| from it, not
-module \verb|B| (as it was thinned out.)  Conceptually, this package is
-being compiled in the context of some module environment \verb|BDEPS| (a
-logical context, in Backpack lingo) which maps modules to original names
-and is utilized by the module finder to lookup the import in
-\verb|B.hs|; we load/thin/rename packages so that the package
-environment accurately reflects the module environment.
-
-Similarly, it is important that the compilation of \verb|B.hs| use \verb|A.hi-boot|
-to determine what entities in the module are visible upon import; this is
-automatically detected by \verb|GHC| when the compilation occurs.  Otherwise,
-in module \verb|pkg-b:B|, there would be a name collision between the local
-definition of \verb|b| and the identifier \verb|b| which was
-accidentally pulled in when we compiled against the actual implementation of
-\verb|A|.  It's actually a bit tempting to compile \verb|pkg-b:B| against the
-\verb|hi-boot| generated by the signature, but this would unnecessarily
-lose out on possible optimizations which are stored in the original \verb|hi|
-file, but not evident from \verb|hi-boot|.
-
-Finally, we created all of the necessary subpackages, and we can compile
-our package proper.
+When compiling the marked signature, we have $flags_H =
+\texttt{-package-loc}\ (\pname{r} \to cwd_r)$ and $flags =
+\texttt{-package}$ \pname{p$(\pname{m} \to \pname{r}$:$\m{P})$}.  The
+only interface files for \m{A} in these two environments is the
+\texttt{hisig} from package \pname{p}.  However, if we use that
+\texttt{hisig}, we will falsely conclude that \m{A} is not sufficiently
+implemented, when in fact it is.  The answer to this conundrum? When
+only \texttt{hisig} files are found, we lookup the \emph{original}
+\texttt{hi} file, and typecheck against that.  An invariant that should
+hold is that all such \texttt{hisig} files should have the same original
+\texttt{hi} file (if this invariant is violated, then we attempt to link
+two physical module implementations together, which is a type error!)
+
+\paragraph{Imports are resolved using only $flags$}
+Another important detail is that $flags_H$ is \emph{only} used to tell
+if there is already a module with the logical name: if the signature
+file contains an import statement, this lookup should be done with
+respect to just $flags$.  As an example:
 
 \begin{verbatim}
-CDEPS =         # empty!!
-ghc -c C.hs -package-name pkg-c-CDEPS -hide-all-packages \
-    -package "pkg-a-ADEPS(A)" \
-    -package "pkg-b-BDEPS"
-# install and register package pkg-c-CDEPS
-\end{verbatim}
-
-This command is quite similar, although it's worth mentioning that now,
-the \verb|package| flags directly mirror the syntax in Backpack.
-Additionally, even though \verb|pkg-c| ``depends'' on subpackages, these
-do not show in its package-name identifier, e.g. CDEPS\@.  This is
-because this package \emph{chose} the values of ADEPS and BDEPS
-explicitly (by including the packages in this particular order), so
-there are no degrees of freedom.\footnote{In the presence of a
-    Cabal-style dependency solver which associates a-0.1 with a concrete
-identifier a, these choices need to be recorded in the package ID.}
-
-Overall, there are a few important things to notice about this architecture.
-First, because the \verb|pkg-b-BDEPS| product is installed, if in another package
-build we instantiate the indefinite module B with exactly the same \verb|pkg-a|
-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{Sometimes you need a module environment instead}  In the compilation
-description here, we've implicitly assumed that any external modules you might
-depend on exist in a package somewhere.  However, a tricky situation
-occurs when some of these modules come from a parent package:
-\begin{verbatim}
-package pkg-b where
-    A :: [ a :: Bool ]
-    B = [ import A; b = 1 ]
-package pkg-c where
-    A = [ a = 0; b = 0 ]
-    include pkg-b
-    C = [ import B; ... ]
+package p where
+    A :: [ x :: Int ]
+    B :: [ import A; y :: Int ]
+    C = [ import B; z = y ]
+package q where
+    A = [ x = 0; y = 0 ]
+    B = [ y = 1 ]
+    include p
 \end{verbatim}
 
-How this problem gets resolved depends on what our library granularity is (Section~\ref{sec:flatten}).
+If we processed the import in \m{B} using $flags_H$, we might
+accidentally pick up the implementation of \m{A} from package \pname{q},
+where we actually wanted to use the forwarding signature built when
+processing signature \m{A}.  Notice that this is opposite of what occurs
+when we are looking for an implementation to check consistency against!
+These imports work the same way as resolving imports for compiled implementations;
+in particular, see an important detail in the next section.
 
-In the ``only definite packages are compiled'' world
-(Section~\ref{sec:one-per-definite-package}), we need to pass a
-special ``module environment'' to the compilation of libraries
-in \verb|monte-carlo| to say where to find \verb|System.Random|.
-The compilation of \verb|pkg-b| now looks as follows:
-
-\begin{verbatim}
-BDEPS = "A -> pkg-a-ADEPS:A"
-ghc -c A.hs-boot -package-name pkg-a-ADEPS -module-env BDEPS
-ghc -c B.hs      -package-name pkg-a-ADEPS -subpackage-name pkg-b-BDEPS -module-env BDEPS
-\end{verbatim}
-
-The most important thing to remember here is that in the ``only definite
-packages are compiled'' world, we must create a \emph{copy} of
-\verb|pkg-b| in order to instantiate its hole with \verb|pkg-a:A|
-(otherwise, there is a circular dependency.)  These packages must be
-distinguished from the parent package (\verb|-subpackage-name|), but
-logically, they will be installed in the \verb|pkg-a| library.  The
-module environment specifies where the holes can be found, without
-referring to an actual package (since \verb|pkg-a| has, indeed, not been
-installed yet at the time we process \verb|B.hs|).  These files are
-probably looked up in the include paths.\footnote{It's worth remarking
-    that a variant of this was originally proposed as the one true
-    compilation strategy.  However, it was pointed out that this gave up
-    applicativity in all cases.  Our current refinement of this strategy
-gives up applicativity for modules which have not been placed in an
-external package.}
-
-Things are a bit different in sliced world and physical module identity
-world (Section~\ref{sec:one-per-package-identity}); here, we really do
-compile and install (perhaps to a local database) \verb|pkg-c:A| before
-starting with the compilation of \verb|pkg-b|.  So package imports will
-continue to work fine.
-
-\subsection{Restricted recursive modules ala hs-boot}\label{sec:hs-boot-restrict}
+\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}
 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
@@ -1066,6 +1069,9 @@ 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
@@ -1085,6 +1091,267 @@ 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 implementations}
+
+Compiling a module is the same as usual; however, we \emph{omit}
+$flags_H$ from the environment.  This is to force compilation to use any
+\emph{locally} compiled \texttt{hisig} files from signature compilation,
+so we see an appropriately thinned version of the module.
+
+\paragraph{Multiple signatures}  When there are multiple signatures
+defined for a logical name, we must merge them together.  Although we
+assume that a single package doesn't have multiple signatures, we could
+bring in a signature from an include:
+
+\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}
+
+In the compilation of \texttt{B}, there is no one \texttt{hisig} found
+in $flags$ (remember that \pname{r}:\m{A} is not findable from $flags$!)
+which provides all the necessary identifiers.  Instead, we have to look
+in both \texttt{hisig} files.  Internally, when we lookup the module, we
+discover there are distinct interface files for the module; however,
+they point to the same original interface file, so the module finder
+loads all of them, merges them together, and uses that as the interface.
+
+An alternate scheme is to perform signature merging in the \verb|-check| step,
+and have some way of telling what the ``latest'' \verb|hi|/\verb|hisig| file is.
+
+\subsection{Compiling aliases}
+
+Aliasing is a new compilation mode designated by \verb|-alias|.  In
+general, in the alias $p = p'$, what is done will vary depending on how
+$p$ and $p'$ are defined in the $flags$ environments.
+(Due to the linking restriction, both are guaranteed to be findable in
+one or the other.)  Here, we say $p\in flags$ to mean that given the
+configuration of the module database with $flags$, $p$ can be found.
+
+\paragraph{$p\in flags$, $p'\not\in flags$ }  This is a type error, $p'$ is
+not findable in the environment, so there's nothing to link against. (Sure,
+it might be in $flags_H$, but these things are not visible in subpackages
+unless we declare a signature.)  Example (marked line fails):
+
+\begin{verbatim}
+package p where
+    A :: ...
+    A = B       -- *
+package q where
+    A = ...
+    B = ...
+    include p
+\end{verbatim}
+
+This is a side effect of the fact that Backpack aliases are oriented;
+one could imagine an alternate scheme where the aliases are symmetric.
+
+\paragraph{$p\not\in flags$, $p'\in flags$ }  Here,
+$p$ is completely undefined, so we are simply defining it from $p'$, no
+linking occurs.  If $p'$ is an \texttt{hisig}, we copy it; if it is an \texttt{hi},
+we create a forwarding \texttt{hisig} to it which reexports \emph{all} of
+its entities.  Both examples are presented below:
+
+\begin{verbatim}
+-- A.hisig available in flags
+package p where
+    A :: ...
+    B = A       -- *
+package q where
+    A = ...
+    include p
+
+-- A.hi available in flags
+package p where
+    A = ...
+    B = A       -- *
+\end{verbatim}
+
+Especially for the first example, we do \emph{not} consider \texttt{B} as
+part of the holes of package \texttt{p} (only explicit signatures count.)
+This means that even if $p\in flags_H$, causing a problem, we will discover
+it only when we go back to checking the parent package, as seen in this
+example:
+
+\begin{verbatim}
+package p where
+    A :: ...
+    B = A       -- this is fine
+package q where
+    A = ...
+    B = ...
+    include p   -- this is not (A != B)
+\end{verbatim}
+
+\paragraph{$p\in flags$, $p'\in flags$ }
+This is the most interesting situation: we'll have to do some sort of linking,
+and it will depend on what we find in $flags$ for both modules.  For all cases
+we need to check whatever the \texttt{hi}/\texttt{hisig} files are, their backing
+implementations are the same (remember the linking restriction!) as in these
+examples:
+
+\begin{verbatim}
+package p where
+    A = ...
+    B = A
+    B = A -- succeeds
+package q where
+    A1 = ...
+    A2 = ...
+    B = A1
+    B = A2 -- fails
+\end{verbatim}
+
+Furthermore, if only an \texttt{hisig} file is available for $p$ in $flags$, Paper
+Backpack instructs us to extend its signature to include everything from $p'$.
+
+\begin{verbatim}
+package p where
+    A :: [ x :: Bool ]
+    B :: [ y :: Bool ]
+    B = A
+    C = [ import B; z = x + y ] -- typechecks
+    D = [ import A; z = x + y ] -- doesn't typecheck
+\end{verbatim}
+
+But this might be a bit of a bother to implement if we don't have a way of dealing
+with multiple \texttt{hisig} files per module name\ldots
+
+\subsection{Compiling includes}
+
+We consider two cases separately; first the simple case with no
+thinning/renaming, and then the case with renaming (for compactness of
+presentation, we assume thinning is represented as a set of identity
+renamings).
+
+In both cases, we need to compute a set of flags which will be
+sufficient to determine where the implementations of holes in the
+subpackage are.  In the case where there is no renaming, the logical
+names that could be linked against are precisely the ones available in
+the current environment: implementations from holes, implementation
+which were defined from includes, and even the modules from the
+in-progress compilation of the current package.  All of these components
+are incorporated into the $flags_H$ parameter of the recursive call.  In
+particular, the new \texttt{-package-loc} lets us define a temporary
+mapping from a package key to a working directory to do lookups, since
+$\mathcal{K}$ will generally not be registered in the package database,
+but we still need to find the relevant \texttt{hi} files.
+
+Once we've compiled the subpackage $\mathcal{K}'$, we need to do two things.
+First, we need to add the package to our $flags$, so that later modules we
+compile are able to see the modules (and signatures) which were defined.
+Second, we need to make sure that the subpackage is \emph{consistent} with
+our current environment.  For example:
+
+\begin{verbatim}
+package p where
+    A = ...
+package q where
+    A = ...
+    include p
+\end{verbatim}
+
+\pname{p} is a perfectly good package, but we can't include in \pname{q} because
+the identities of the two \m{A}'s don't match up.  Of course, if they were the
+same \m{A}, this would be fine.
+
+If we adopt the system where we merge signature files as we go along, this checking
+phase would also be a good time to merge any \texttt{hisig} files from the subpackage
+with any in the current $flags$ environment.
+
+\paragraph{With renaming}  Renaming poses an interesting challenge because \emph{holes}
+can be renamed:
+
+\begin{verbatim}
+package p where
+    A :: ...
+package q where
+    B = ...
+    include p (A as B)
+\end{verbatim}
+
+This renaming makes it possible for the include statement to explicitly say how
+holes should be implemented, but it also means that \emph{just} stuffing the current set of flags
+is unlikely to work, because everything has been renamed.  At the same time, we can't
+drop the $flags_H$, because it may contain information about how to find packages which
+are not registered in package database yet (\verb|-package-loc|).
+
+Instead, what we do is pass the same set of flags as before, but use these package
+locations \emph{solely} to resolve the mapping in \verb|-reset-module-env| from holes
+to their implementations: this mapping replaces the old $flags_H$, except for these
+explicitly instantiated modules.
+
+\emph{ToDo: maybe something better can be done here}
+
+\subsection{Commentary}
+
+\paragraph{So how the heck are \texttt{flags} processed}  Previously, the purpose of
+\verb|-package| flags was to modify the exposed flag on entries in the in-memory package
+database, which itself was used to create a map from modules to all packages which
+defined them.
+
+The existence of \verb|-hole-flags| means we need to track a second package state just for
+the lookup needed when we're compiling an \verb|hsig| file and want to know if it is
+implemented in $flags_H$.  Additionally, \verb|-package-loc| and \verb|-reset-module-env|
+mean that not all modules in the database are necessarily in the package database. (It's worth
+remarking why we can't use \verb|-I|: the package key is not right, since \verb|-I| assumes
+that you are adding extra include directories for the compilation of the \emph{current} package
+key, not necessarily one of, say, a parent package.)  Finally, \verb|-package| arguments
+are now augmented with explicit thinning and renaming.
+
+Thus, the new model is to do away with ``exposed packages'', and instead have a package
+database mapping package keys to packages (when we need to find original names), and then
+a mapping of modules to their respective packages which is updated by the various commands.
+
+\begin{itemize}
+    \item \verb|-package| adds the package to the package key map, and
+        dumps all of the exposed modules of the package into the module
+        map.  If it has renamings, the entries placed in the module map
+        are tweaked accordingly.
+    \item \verb|-package-loc| adds the location to the package key map,
+        and scans the directory for all interface files and puts them in
+        the module map (alternately, this could be done lazily, or the
+        modules could be explicitly provided.)
+    \item \verb|-reset-module-env| performs some module resolutions based
+        on the current module map, and then replaces the map with the result
+        of the resolution. (The package key map is left alone.)
+\end{itemize}
+
+\paragraph{Just because it compiled, doesn't mean the individual packages type check}
+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.''
+It's a bit unavoidable, really.
+
 \section{Shaped Backpack}
 
 Despite the simplicity of shapeless Backpack with the linking
@@ -1093,7 +1360,7 @@ 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.
+to support it at some point.
 
 \subsection{Efficient shaping}