Backpack docs: merge backpack-shaping into algorithm, sigs no longer provide

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

5 files changed, 376 insertions, 934 deletions

diff --git a/docs/backpack/Makefile b/docs/backpack/Makefile
index ea7b79d331..a8df945d7d 100644
--- a/docs/backpack/Makefile
+++ b/docs/backpack/Makefile
@@ -1,4 +1,4 @@
-all: backpack-impl.pdf backpack-manual.pdf ubackpack.pdf backpack-shaping.pdf algorithm.pdf
+all: backpack-impl.pdf backpack-manual.pdf ubackpack.pdf algorithm.pdf
 
 ubackpack.pdf: ubackpack.tex
 	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 ubackpack.tex || ! rm -f $@
@@ -9,8 +9,5 @@ backpack-impl.pdf: backpack-impl.tex
 backpack-manual.pdf: backpack-manual.tex
 	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-manual.tex || ! rm -f $@
 
-backpack-shaping.pdf: backpack-shaping.tex
-	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-shaping.tex || ! rm -f $@
-
 algorithm.pdf: algorithm.tex
 	latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 algorithm.tex || ! rm -f $@
diff --git a/docs/backpack/algorithm.pdf b/docs/backpack/algorithm.pdf
index e6af2accc6..8865b94a9b 100644
--- a/docs/backpack/algorithm.pdf
+++ b/docs/backpack/algorithm.pdf
diff --git a/docs/backpack/algorithm.tex b/docs/backpack/algorithm.tex
index 89cfeef549..956480b0e4 100644
--- a/docs/backpack/algorithm.tex
+++ b/docs/backpack/algorithm.tex
@@ -37,41 +37,48 @@
 This document describes the Backpack shaping and typechecking
 passes, as we intend to implement it.
 
+\section{Changelog}
+
+\paragraph{April 28, 2015}  A signatures declaration no longer provides
+a signature in the technical shaping sense; the motivation for this change
+is explained in \textbf{Signatures cannot be provided}.  This means that,
+by default, all requirements are importable (Derek has stated that he doesn't
+think this will be too much of a problem in practice); we can consider extensions
+which allow us to hide requirements from import.
+
 \section{Front-end syntax}
 
 For completeness, here is the package language we will be shaping and typechecking:
 
 \begin{verbatim}
-package     ::= "package" pkgname [pkgexports] "where" pkgbody
-pkgbody     ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
-pkgdecl     ::= "module"    modid [exports] where body
-              | "signature" modid [exports] where body
-              | "include"   pkgname [inclspec]
-inclspec    ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
-                [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
-pkgexports  ::= inclspec
-renaming    ::= modid "as" modid
+    package     ::= "package" pkgname [pkgexports] "where" pkgbody
+    pkgbody     ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
+    pkgdecl     ::= "module"    modid [exports] where body
+                  | "signature" modid [exports] where body
+                  | "include"   pkgname [inclspec]
+    inclspec    ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
+                    [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
+    pkgexports  ::= inclspec
+    renaming    ::= modid "as" modid
 \end{verbatim}
-
 See the ``Backpack manual'' for more explanation about the syntax.  It
 is slightly simplified here by removing any constructs which are easily implemented as
-syntactic sugar (e.g. a \verb|modid| renaming is simply \verb|modid as modid|.)
+syntactic sugar (e.g., a \verb|modid| renaming is simply \verb|modid as modid|.)
 
 \section{Shaping}
 
 Shaping computes a \verb|Shape| which has this form:
 
 \begin{verbatim}
-Shape ::= provides: { ModName -> Module { Name } }
-          requires: { ModName ->        { Name } }
-
-PkgKey      ::= SrcPkgId "(" { ModName "->" Module } ")"
-              | HOLE
-Module      ::= PkgKey ":" ModName
-Name        ::= Module "." OccName
-OccName     ::= -- a plain old name, e.g. undefined, Bool, Int
+    Shape ::= provides: { ModName -> Module { Name } }
+              requires: { ModName ->        { Name } }
+
+    PkgKey      ::= SrcPkgId "(" { ModName "->" Module } ")"
+                  | HOLE
+    Module      ::= PkgKey ":" ModName
+    Name        ::= Module "." OccName
+    OccName     ::= undefined | Bool | Int | ...
 \end{verbatim}
-
 Starting with the empty shape, we incrementally construct a shape by
 shaping package declarations (the partially constructed shape serves as
 a context for renaming modules and signatures and instantiating
@@ -89,85 +96,225 @@ See more about this in the type checking section.
 In the description below, we'll assume \verb|THIS| is the package key
 of the package being processed.
 
-\newpage
+\begin{aside}
+\textbf{\texttt{OccName} is implied by \texttt{Name}.}
+In Haskell, the following is not valid syntax:
+
+\begin{verbatim}
+    import A (foobar as baz)
+\end{verbatim}
+In particular, a \verb|Name| which is in scope will always have the same
+\verb|OccName| (even if it may be qualified.)  You might imagine relaxing
+this restriction so that declarations can be used under different \verb|OccName|s;
+in such a world, we need a different definition of shape:
+
+\begin{verbatim}
+    Shape ::=
+        provided: ModName -> { OccName -> Name }
+        required: ModName -> { OccName -> Name }
+\end{verbatim}
+Presently, however, such an \verb|OccName| annotation would be redundant: it can be inferred from the \verb|Name|.
+\end{aside}
+
+\begin{aside}
+\textbf{Holes of a package are a mapping, not a set.} Why can't the \verb|PkgKey| just record a
+set of \verb|Module|s, e.g. \verb|PkgKey ::= SrcPkgKey { Module }|?  Consider:
+
+\begin{verbatim}
+    package p (A) requires (H1, H2) where
+        signature H1(T) where
+            data T
+        signature H2(T) where
+            data T
+        module A(A(..)) where
+            import qualified H1
+            import qualified H2
+            data A = A H1.T H2.T
+
+    package q (A12, A21) where
+        module I1(T) where
+            data T = T Int
+        module I2(T) where
+            data T = T Bool
+        include p (A as A12) requires (H1 as I1, H2 as I2)
+        include p (A as A21) requires (H1 as I2, H2 as I1)
+\end{verbatim}
+With a mapping, the first instance of \verb|p| has key \verb|p(H1 -> q():I1, H2 -> q():I2)|
+while the second instance has key \verb|p(H1 -> q():I2, H2 -> q():I1)|; with
+a set, both would have the key \verb|p(q():I1, q():I2)|.
+\end{aside}
+
+
+\begin{aside}
+\textbf{Signatures can require a specific entity.}
+With requirements like \verb|A -> { HOLE:A.T, HOLE:A.foo }|,
+why not specify it as \verb|A -> { T, foo }|,
+e.g., \verb|required: { ModName -> { OccName } }|?  Consider:
+
+\begin{verbatim}
+    package p () requires (A, B) where
+        signature A(T) where
+            data T
+        signature B(T) where
+            import T
+\end{verbatim}
+The requirements of this package specify that \verb|A.T| $=$ \verb|B.T|; this
+can be expressed with \verb|Name|s as
+
+\begin{verbatim}
+    A -> { HOLE:A.T }
+    B -> { HOLE:A.T }
+\end{verbatim}
+But, without \verb|Name|s, the sharing constraint is impossible:  \verb|A -> { T }; B -> { T }|. (NB: \verb|A| and \verb|B| don't have to be implemented with the same module.)
+\end{aside}
+
+\begin{aside}
+\textbf{The \texttt{Name} of a value is used to avoid
+ambiguous identifier errors.}  We state that two types
+are equal when their \texttt{Name}s are the same; however,
+for values, it is less clear why we care.  But consider this example:
+
+\begin{verbatim}
+    package p (A) requires (H1, H2) where
+        signature H1(x) where
+            x :: Int
+        signature H2(x) where
+            import H1(x)
+        module A(y) where
+            import H1
+            import H2
+            y = x
+\end{verbatim}
+The reference to \verb|x| in \verb|A| is unambiguous, because it is known
+that \verb|x| from \verb|H1| and \verb|x| from \verb|H2| are the same (have
+the same \verb|Name|.)  If they were not the same, it would be ambiguous and
+should cause an error.  Knowing the \verb|Name| of a value distinguishes
+between these two cases.
+\end{aside}
+
+\begin{aside}
+\textbf{Absence of \texttt{Module} in \texttt{requires} implies holes are linear}
+Because the requirements do not record a \verb|Module| representing
+the identity of a requirement, it means that it's not possible to assert
+that hole \verb|A| and hole \verb|B| should be implemented with the same module,
+as might occur with aliasing:
+
+\begin{verbatim}
+    signature A where
+    signature B where
+    alias A = B
+\end{verbatim}
+%
+The benefit of this restriction is that when a requirement is filled,
+it is obvious that this is the only requirement that is filled: you won't
+magically cause some other requirements to be filled.  The downside is
+it's not possible to write a package which looks for an interface it is
+looking for in one of $n$ names, accepting any name as an acceptable linkage.
+If aliasing was allowed, we'd need a separate physical shaping context,
+to make sure multiple mentions of the same hole were consistent.
+
+\end{aside}
+
+%\newpage
 
 \subsection{\texttt{module M}}
 
-Merge with this shape:
+A module declaration provides a module \verb|THIS:M| at module name \verb|M|. It
+has the shape:
 
 \begin{verbatim}
     provides: { M -> THIS:M { exports of renamed M } }
     requires: (nothing)
 \end{verbatim}
-
-\noindent Example:
+Example:
 
 \begin{verbatim}
-    -- provides: (nothing)
-    -- requires: (nothing)
-
     module A(T) where
         data T = T
 
-    -- provides: A -> THIS:A { THIS:A.T }           -- NEW
-    -- requires: (nothing)
-
-    module M(T, f) where
-        import A(T)
-        f x = x
-
     -- provides: A -> THIS:A { THIS:A.T }
-                 M -> THIS:M { THIS:A.T, THIS:M.f } -- NEW
     -- requires: (nothing)
 \end{verbatim}
 
 \newpage
 \subsection{\texttt{signature M}}
 
-Merge with this shape:
+A signature declaration creates a requirement at module name \verb|M|.  It has the shape:
 
 \begin{verbatim}
-    provides: { M -> HOLE:M { exports of renamed M } }
-    requires: { M ->        { exports of renamed M } }
+    provides: (nothing)
+    requires: { M -> { exports of renamed M } }
 \end{verbatim}
 
 \noindent Example:
 
 \begin{verbatim}
-    -- provides: (nothing)
-    -- requires: (nothing)
-
     signature H(T) where
         data T
 
-    -- provides: H -> HOLE:H { HOLE:H.T }
-    -- requires: H ->        { HOLE:H.T }
+    -- provides: H -> (nothing)
+    -- requires: H -> { HOLE:H.T }
+\end{verbatim}
 
-    module A(T) where
-        import H(T)
-    module B(T) where
-        data T = T
+\begin{aside}
+\textbf{Signatures cannot be provided}.  A signature \emph{never} counts
+as a provision, as far as shaping is concerned.  While it seems like
+a signature package which provides signatures for import should actually,
+you know, \emph{provide} its signatures, this observation at its
+logical conclusion is a mess.  The problem can most clearly be
+seen in this example:
 
-    -- provides: H -> HOLE:H { HOLE:H.T }
-    --           A -> THIS:A { HOLE:H.T } -- NEW
-    --           B -> THIS:B { THIS:B.T } -- NEW
-    -- requires: H ->        { HOLE:H.T }
+\begin{verbatim}
+    package a-sigs (A) requires (A) where -- ***
+        signature A where
+            data T
 
-    signature H(T, f) where
-        import B(T)
-        f :: a -> a
+    package a-user (B) requires (A) where
+        signature A where
+            data T
+            x :: T
+        module B where
+            ...
 
-    -- provides: H -> HOLE:H { THIS:B.T, HOLE:H.f } -- UPDATED
-    --           A -> THIS:A { THIS:B.T }           -- UPDATED
-    --           B -> THIS:B { THIS:B.T }
-    -- requires: H ->        { THIS:B.T, HOLE:H.f } -- UPDATED
+    package p where
+        include a-sigs
+        include a-user
 \end{verbatim}
+%
+When we consider merging in the shape of \verb|a-user|, does the
+\verb|A| provided by \verb|a-sigs| fill in the \verb|A| requirement
+in \verb|a-user|?  It \emph{should not}, since \verb|a-sigs| does not
+actually provide enough declarations to satisfy \verb|a-user|'s
+requirement: the intended semantics \emph{merges} the requirements
+of \verb|a-sigs| and \verb|a-user|, but doesn't use the provision to
+fill the signature.  However, in this case:
 
-Notice that in the last example, when a signature with reexports is merged,
-it can result in updates to the shapes of other module names.
+\begin{verbatim}
+    package a-sigs (M as A) requires (H as A) where
+        signature H(T) where
+            data T
+        module M(T) where
+            import H(T)
+\end{verbatim}
+%
+We rightly should error, since the provision is a module. And in this situation:
 
-\newpage
+\begin{verbatim}
+    package a-sigs (H as A) requires (H) where
+        signature H(T) where
+            data T
+\end{verbatim}
+%
+The requirements should be merged, but should the merged requirement
+be under the name \verb|H| or \verb|A|?
 
+It may still be possible to use the \verb|(A) requires (A)| syntax to
+indicate exposed signatures, but this would be a mere syntactic
+alternative to \verb|() requires (exposed A)|.
+\end{aside}
+%
+
+\newpage
 \subsection{\texttt{include pkg (X) requires (Y)}}
 
 We merge with the transformed shape of package \verb|pkg|, where this
@@ -176,16 +323,14 @@ shape is transformed by:
 \begin{itemize}
     \item Renaming and thinning the provisions according to \verb|(X)|
     \item Renaming requirements according to \verb|(Y)| (requirements cannot
-          be thinned, so non-mentioned requirements are passed through.)
+          be thinned, so non-mentioned requirements are implicitly passed through.)
           For each renamed requirement from \verb|Y| to \verb|Y'|,
           substitute \verb|HOLE:Y| with \verb|HOLE:Y'| in the
           \verb|Module|s and \verb|Name|s of the provides and requires.
-          (Freshen holes.)
-    \item If there are no thinnings/renamings, you just merge the
-          shape unchanged!
 \end{itemize}
-
-\noindent Example:
+%
+If there are no thinnings/renamings, you just merge the
+shape unchanged! Here is an example:
 
 \begin{verbatim}
     package p (M) requires (H) where
@@ -195,70 +340,114 @@ shape is transformed by:
             import H
             data S = S T
 
-    -- p requires: M -> { p(H -> HOLE:H):M.S }
-    --   provides: H -> { HOLE:H.T }
-
     package q (A) where
         module X where
             data T = T
+        include p (M as A) requires (H as X)
+\end{verbatim}
+%
+The shape of package \verb|p| is:
 
-        -- provides: X -> { q():X.T }
-        -- requires: (nothing)
+\begin{verbatim}
+    requires: M -> { p(H -> HOLE:H):M.S }
+    provides: H -> { HOLE:H.T }
+\end{verbatim}
+%
+Thus, when we process the \verb|include| in package \verb|q|,
+we make the following two changes: we rename the provisions,
+and we rename the requirements, substituting \verb|HOLE|s.
+The resulting shape to be merged in is:
 
-        include p (M as A) requires (H as X)
-        -- 1. Rename/thin provisions:
-        --      provides: A -> { p(H -> HOLE:H):M.S }
-        --      requires: H -> { HOLE:H.T }
-        -- 2. Rename requirements, substituting HOLEs:
-        --      provides: A -> { p(H -> HOLE:X):M.S }
-        --      requires: X -> { HOLE:X.T }
+\begin{verbatim}
+    provides: A -> { p(H -> HOLE:X):M.S }
+    requires: X -> { HOLE:X.T }
+\end{verbatim}
+%
+After merging this in, the final shape of \verb|q| is:
 
-        -- (after merge)
-        -- provides: X -> { q():X.T }
-        --           A -> { p(H -> q():X):M.S }
-        -- requires: (nothing)
+\begin{verbatim}
+    provides: X -> { q():X.T }              -- from shaping 'module X'
+              A -> { p(H -> q():X):M.S }
+    requires: (nothing)                     -- discharged by provided X
 \end{verbatim}
 
 \newpage
 
 \subsection{Merging}
 
-Merging combines two shapes, filling requirements with implementations
-and substituting information we learn about the identities of
-\verb|Name|s.  Importantly, merging is a \emph{directed} process, akin
-to taking two boxes with input and output ports and wiring them up so
-that the first box feeds into the second box.  This algorithm does not
-support mutual recursion.
+The shapes we've given for individual declarations have been quite
+simple.  Merging combines two shapes, filling requirements with
+implementations and substituting information we learn about the
+identities of \verb|Name|s; it is the most complicated part of the
+shaping process.
+
+The best way to think about merging is that we take two packages with
+inputs (requirements) and outputs (provisions) and ``wiring'' them up so
+that outputs feed into inputs.  In the absence
+of mutual recursion, this wiring process is \emph{directed}: the provisions
+of the first package feed into the requirements of the second package,
+but never vice versa.  (With mutual recursion, things can go in the opposite
+direction as well.)
 
-Suppose we are merging shape $p$ with shape $q$.  Merging proceeds as follows:
+Suppose we are merging shape $p$ with shape $q$ (e.g., $p; q$).  Merging
+proceeds as follows:
 
 \begin{enumerate}
     \item \emph{Fill every requirement of $q$ with provided modules from
-        $p$.} For each requirement $M$ of $q$ that is provided by $p$,
+        $p$.} For each requirement $M$ of $q$ that is provided by $p$ (in particular,
+        all of its required \verb|Name|s are provided),
         substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
         provided $p(M)$, merge the names, and remove the requirement from $q$.
-    \item \emph{Merge in provided signatures of $q$, add the provided modules of $q$.}
-        For each provision $M$ of $q$: if $q(M)$ is a hole, substitute every
-        \verb|Module| occurrence of \verb|HOLE:|$q(M)$ with $p(M)$ if it exists and merge
-        the names; otherwise, add it to $p$, erroring if $p(M)$ exists.
+        Error if a provision is insufficient for the requirement.
+    \item If mutual recursion is supported, \emph{fill every requirement of $p$ with provided modules from $q$.}
+    \item \emph{Merge leftover requirements.}  For each requirement $M$ of $q$ that is not
+        provided by $p$ but required by $p$, merge the names.  (It's not
+        necessary to substitute \verb|Module|s, since they are guaranteed to be the same.)
+    \item \emph{Add provisions of $q$.} Union the provisions of $p$ and $q$, erroring
+        if there is a duplicate that doesn't have the same identity.
 \end{enumerate}
-
-Substitutions apply to both shapes.  To merge two sets of names, take
-each pair of names with matching \verb|OccName|s $n$ and $m$.
+%
+To merge two sets of names, take each pair of names with matching \verb|OccName|s $n$ and $m$.
 
 \begin{enumerate}
-    \item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$. (E.g., pick the one with the lexicographically first \verb|ModName|).
+    \item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$.
     \item If one $n$ is from a hole, substitute $n$ with $m$.
     \item Otherwise, error if the names are not the same.
 \end{enumerate}
-
+%
 It is important to note that substitutions on \verb|Module|s and substitutions on
 \verb|Name|s are disjoint: a substitution from \verb|HOLE:A| to \verb|HOLE:B|
 does \emph{not} substitute inside the name \verb|HOLE:A.T|.
-Here is a simple example:
+
+Since merging is the most complicated step of shaping, here are a big
+pile of examples of it in action.
+
+\subsubsection{A simple example}
+
+In the following set of packages:
+
+\begin{verbatim}
+    package p(M) requires (A) where
+        signature A(T) where
+            data T
+        module M(T, S) where
+            import A(T)
+            data S = S T
+
+    package q where
+        module A where
+            data T = T
+        include p
+\end{verbatim}
+
+When we \verb|include p|, we need to merge the partial shape
+of \verb|q| (with just provides \verb|A|) with the shape
+of \verb|p|.  Here is each step of the merging process:
 
 \begin{verbatim}
           shape 1                       shape 2
+          --------------------------------------------------------------------------------
+(initial shapes)
 provides: A -> THIS:A { q():A.T }       M -> p(A -> HOLE:A) { HOLE:A.T, p(A -> HOLE:A).S }
 requires: (nothing)                     A ->                { HOLE:A.T }
 
@@ -272,133 +461,76 @@ provides: A -> THIS:A         { q():A.T }
 requires: (nothing)
 \end{verbatim}
 
-Here are some more involved examples, which illustrate some important
-cases:
+Notice that we substituted \verb|HOLE:A| with \verb|THIS:A|, but \verb|HOLE:A.T| with \verb|q():A.T|.
 
-\subsubsection{Sharing constraints}
+\subsubsection{Requirements merging can affect provisions}
 
-Suppose you have two signature which both independently define a type,
-and you would like to assert that these two types are the same.  In the
-ML world, such a constraint is known as a sharing constraint.  Sharing
-constraints can be encoded in Backpacks via clever use of reexports;
-they are also an instructive example for signature merging.
-For brevity, we've omitted \verb|provided| from the shapes in this example.
+When a merge results in a substitution, we substitute over both
+requirements and provisions:
 
 \begin{verbatim}
-signature A(T) where
-    data T
-signature B(T) where
-    data T
+    signature H(T) where
+        data T
+    module A(T) where
+        import H(T)
+    module B(T) where
+        data T = T
 
--- requires: A -> HOLE:A        { HOLE:A.T }
-             B -> HOLE:B        { HOLE:B.T }
+    -- provides: A -> THIS:A { HOLE:H.T }
+    --           B -> THIS:B { THIS:B.T }
+    -- requires: H ->        { HOLE:H.T }
 
--- the sharing constraint!
-signature A(T) where
-    import B(T)
--- (shape to merge)
--- requires: A -> HOLE:A        { HOLE:B.T }
+    signature H(T, f) where
+        import B(T)
+        f :: a -> a
 
--- (after merge)
--- requires: A -> HOLE:A        { HOLE:A.T }
---           B -> HOLE:B        { HOLE:A.T }
+    -- provides: A -> THIS:A { THIS:B.T }           -- UPDATED
+    --           B -> THIS:B { THIS:B.T }
+    -- requires: H ->        { THIS:B.T, HOLE:H.f } -- UPDATED
 \end{verbatim}
 
-Notably, we could equivalently have chosen \verb|HOLE:B.T| as the post-merge
-name.  \Red{Actually, I don't think any choice can be wrong. The point is to
-ensure that the substitution applies to everything we know about, and since requirements
-monotonically increase in size (or are filled), this will hold.}
-
-\subsubsection{Provision linking does not discharge requirements}
-
-It is not an error to define a module, and then define a signature
-afterwards: this can be useful for checking if a module implements
-a signature, and also for sharing constraints:
-
-\begin{verbatim}
-module M(T) where
-    data T = T
-signature S(T) where
-    data T
-
-signature M(T)
-    import S(T)
--- (partial)
--- provides: S -> HOLE:S { THIS:M.T } -- resolved!
-
--- alternately:
-signature S(T) where
-    import M(T)
-\end{verbatim}
+\subsubsection{Sharing constraints}
 
-However, in some circumstances, linking a signature to a module can cause an
-unrelated requirement to be ``filled'':
+Suppose you have two signature which both independently define a type,
+and you would like to assert that these two types are the same.  In the
+ML world, such a constraint is known as a sharing constraint.  Sharing
+constraints can be encoded in Backpacks via clever use of reexports;
+they are also an instructive example for signature merging.
 
 \begin{verbatim}
-package p (S) requires (S) where
-    signature S where
+    signature A(T) where
+        data T
+    signature B(T) where
         data T
 
-package q (A) requires (B) where
-    include S (S as A) requires (S as B)
-
-package r where
-    module A where
-        data T = T
-    include q (A) requires (B)
-    -- provides: A -> THIS:A { THIS:A.T }
-    -- requires: (nothing)
-\end{verbatim}
-
-Notice that the requirement was discharged because we unified \verb|HOLE:B|
-with \verb|THIS:A|.  While this is certainly the most accurate picture
-of the package we can get from this situation, it is a bit unsatisfactory
-in that looking at the text of module \verb|r|, it is not obvious that
-all the requirements were filled; only that there is some funny business
-going on with multiple provisions with \verb|A|.
-
-Note that we \emph{cannot} disallow multiple bindings to the same provision:
-this is a very important use-case when you want to include one signature,
-include another signature, and see the merge of the two signatures in your
-context.  \Red{So maybe this is what we should do.}  However, there is
-a saving grace, which is signature-signature linking can be done when
-linking requirements; linking provisions is unnecessary in this case.
-So perhaps the merge rule should be something like:
+    -- requires: A -> { HOLE:A.T }
+                 B -> { HOLE:B.T }
 
-\begin{enumerate}
-    \item \emph{Fill every requirement of $q$ with provided modules from
-        $p$.} For each requirement $M$ of $q$ that is provided by $p$,
-        substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
-        provided $p(M)$, merge the names, and remove the requirement from $q$.
-    \item \emph{Merge requirements.}  For each requirement $M$ of $q$ that is not
-        provided by $p$ but required by $p$, merge the names.
-    \item \emph{Add provisions of $q$.} For each provision $M$ of $q$:
-        add it to $p$, erroring if the addition is incompatible with an
-        existing entry in $p$.
-\end{enumerate}
+    -- the sharing constraint!
+    signature A(T) where
+        import B(T)
+    -- (shape to merge)
+    -- requires: A -> { HOLE:B.T }
 
-Now, because there is no provision linking, and the requirement \verb|B| is
-not linked against anything, \verb|A| ends up being incompatible with
-the \verb|A| in context and is rejected.  We also reject situations where
-a provision unification would require us to pick a signature:
+    -- (after merge)
+    -- requires: A -> { HOLE:A.T }
+    --           B -> { HOLE:A.T }
+\end{verbatim}
+%
+\Red{I'm pretty sure any choice of \texttt{Name} is OK, since the
+subsequent substitution will make it alpha-equivalent.}
 
-\begin{verbatim}
-package p (S) requires (S) where
-    signature S
+%   \subsubsection{Leaky requirements}
 
-package q where
-    include p (S) requires (S as A)
-    include p (S) requires (S as B)
-    -- rejected; provided S doesn't unify
-    -- (if we accepted, what's the requirement? A? B?)
-\end{verbatim}
+%   Both requirements and provisions can be imported, but requirements
+%   are always available
 
-\Red{How to relax this so hs-boot works}
+%\Red{How to relax this so hs-boot works}
 
-\Red{Example of how loopy modules which rename requirements make it un-obvious whether or not
-a requirement is still required.  Same example works declaration level.}
+%\Red{Example of how loopy modules which rename requirements make it un-obvious whether or not
+%a requirement is still required.  Same example works declaration level.}
 
-\Red{package p (A) requires (A); the input output ports should be the same}
+%\Red{package p (A) requires (A); the input output ports should be the same}
 
 % We figure out the requirements (because no loopy modules)
 %
@@ -413,46 +545,54 @@ a requirement is still required.  Same example works declaration level.}
 % things on things, merging things together as you discover that this is
 % the case.
 
-\newpage
+%\newpage
 
 \subsection{Export declarations}
 
 If an explicit export declaration is given, the final shape is the
 computed shape, minus any provisions not mentioned in the list, with the
-appropriate renaming applied to provisions and requirements.  (Provisions
+appropriate renaming applied to provisions and requirements.  (Requirements
 are implicitly passed through if they are not named.)
-
 If no explicit export declaration is given, the final shape is
-the computed shape, minus any provisions which did not have an in-line
-module or signature declaration.
+the computed shape, including only provisions which were defined
+in the declarations of the package.
 
 \begin{aside}
-\textbf{Guru meditation.}  The defaulting behavior for signatures
-is slightly delicate, as can be seen in this example:
+\textbf{Signature visibility, and defaulting}
+The simplest formulation of requirements is to have them always be
+visible.  Signature visibility could be controlled by associating
+every requirement with a flag indicating if it is importable or
+not: a signature declaration sets a requirement to be visible, and
+an explicit export list can specify if a requirement is to be visible
+or not.
+
+When an export list is absent, we have to pick a default visibility
+for a signature.  If we use the same behavior as with modules,
+a strange situation can occur:
 
 \begin{verbatim}
-package p (S) requires (S) where
-    signature S where
-        x :: True
-
-package q where
-    include p
-    signature S where
-        y :: True
-    module M where
-        import S
-        z = x && y      -- OK
-
-package r where
-    include q
-    module N where
-        import S
-        z = y           -- OK
-        z = x           -- ???
+    package p where -- S is visible
+        signature S where
+            x :: True
+
+    package q where -- use defaulting
+        include p
+        signature S where
+            y :: True
+        module M where
+            import S
+            z = x && y      -- OK
+
+    package r where
+        include q
+        module N where
+            import S
+            z = y           -- OK
+            z = x           -- ???
 \end{verbatim}
-
+%
 Absent the second signature declaration in \verb|q|, \verb|S.x| clearly
-should not be visible.  However, what ought to occur when this signature
+should not be visible in \verb|N|.  However, what ought to occur when this signature
 declaration is added?  One interpretation is to say that only some
 (but not all) declarations are provided (\verb|S.x| remains invisible);
 another interpretation is that adding \verb|S| is enough to treat
@@ -470,9 +610,6 @@ package q where
     include p
     signature S where
 \end{verbatim}
-
-Note that if \verb|p| didn't provide \verb|S|, \verb|x| would \emph{never}
-be visible unless it was redeclared in an interface.
 \end{aside}
 %
 %   SPJ: This would be too complicated (if there's yet a third way)
@@ -484,7 +621,7 @@ a mapping \verb|M -> HOLE:M|.  Annoyingly, you don't know the full set of
 requirements until the end of shaping, so you don't know the package key ahead of time;
 however, it can be substituted at the end easily.
 
-\newpage
+%\newpage
 
 \section{Type checking}
 
diff --git a/docs/backpack/backpack-shaping.pdf b/docs/backpack/backpack-shaping.pdf
deleted file mode 100644
index 50b8a17309..0000000000
--- a/docs/backpack/backpack-shaping.pdf
+++ /dev/null
diff --git a/docs/backpack/backpack-shaping.tex b/docs/backpack/backpack-shaping.tex
deleted file mode 100644
index b77cb9d9bc..0000000000
--- a/docs/backpack/backpack-shaping.tex
+++ /dev/null
@@ -1,692 +0,0 @@
-\documentclass{article}
-
-\usepackage{mdframed}
-\usepackage{pifont}
-\usepackage{graphicx} %[pdftex] OR [dvips]
-\usepackage{fullpage}
-\usepackage{wrapfig}
-\usepackage{float}
-\usepackage{titling}
-\usepackage{hyperref}
-\usepackage{tikz}
-\usepackage{color}
-\usepackage{footnote}
-\usepackage{float}
-\usepackage{algorithm}
-\usepackage{algpseudocode}
-\usepackage{bigfoot}
-\usepackage{amssymb}
-
-\newenvironment{aside}
-  {\begin{mdframed}[style=0,%
-      leftline=false,rightline=false,leftmargin=2em,rightmargin=2em,%
-          innerleftmargin=0pt,innerrightmargin=0pt,linewidth=0.75pt,%
-      skipabove=7pt,skipbelow=7pt]\small}
-  {\end{mdframed}}
-
-\setlength{\droptitle}{-6em}
-
-\newcommand{\Red}[1]{{\color{red} #1}}
-
-\title{Backpack shaping by example}
-
-\begin{document}
-
-\maketitle
-
-Note: this document assumes familiarity with the syntax of Backpack. Go
-read the Backpack Manual (\url{http://web.mit.edu/~ezyang/Public/backpack-manual.pdf}) if you haven't already.
-
-\begin{aside}
-\textbf{Guru meditation.} These asides contain more complex examples
-which justify certain design choices. They can be skipped without missing
-out on important information.  You might have to have read further to
-understand them.
-\end{aside}
-
-\section{What is shaping?}
-
-When you write an ordinary Haskell package, if you define
-the data type \verb|ByteString| in \verb|Data.ByteString.Lazy|,
-and define it again in \verb|Data.ByteString.Strict|, you
-do not expect these types to be the same.
-
-However, if you are doing modular programming with module interfaces, you
-might want to define a type in a module interface, but not say where
-it comes from: that's the job of whoever implements the
-interface.  \verb|ByteString| defined in two interfaces could be
-the same\ldots or they might be different.  Shaping tells you whether
-or not they are the same.
-
-Imagine you have two signature packages: \verb|haskell98-base-sigs|,
-which just exports \verb|Prelude| defining \verb|Int|; and \verb|ghc-base-sigs|,
-which provides a more internal version of \verb|Int| in \verb|GHC.Base|, with
-\verb|Prelude| simply reexporting the definition there.
-
-\begin{verbatim}
-package haskell98-base-sigs (Prelude) where
-    signature Prelude(Int) where
-        data Int
-
-package ghc-base-sigs (Prelude, GHC.Base) where
-    include ghc-prim
-    signature GHC.Base(Int(..)) where
-        import GHC.Prim(Int#)
-        data Int = I# Int#
-    signature Prelude(Int) where
-        import GHC.Base
-\end{verbatim}
-
-Now, suppose you want to type-check a package which is using both
-signatures at the same time:
-
-\begin{verbatim}
-package p (A) where
-    include haskell98-base-sigs
-    include ghc-base-sigs
-    module A where
-        import Prelude
-        import GHC.Base
-        ... Int ...
-\end{verbatim}
-
-There are two places where \verb|Int| is defined, and we ought not to
-accept \verb|A| unless \verb|haskell98-base-sigs:Prelude.Int| and
-\verb|ghc-base-sigs:GHC.Base.Int| are the same.  In fact, they are the
-same;\footnote{The reason is \verb|p| \emph{linked} the two \verb|Prelude|s
-together: they must be implemented with the same module.  Since any
-implementation of \verb|Prelude| can only define one entity named
-\verb|Int|, we can infer that the separate \verb|Int|s in the signatures
-must be the same; and by inference, that
-\verb|ghc-base-sigs:GHC.Base.Int| is equivalent as well.} however, if you
-remove module \verb|ghc-base-sigs:Prelude|, the two \verb|Int|s are no longer
-equal!
-
-Shaping is the process responsible for concluding that these two types are
-equal.  By the end of this document, you should understand how and why \verb|Int|
-is type equal in the previous example, as well as understand other examples.
-
-\section{Defining pre-shape}
-
-Informally, a package consists of a collection of modules and
-signatures, which, given some \emph{required} holes at some module
-names, can \emph{provide} some modules (at some other module names) for
-import by anyone who includes the package.  The requires and provides
-of a package can be written explicitly in the header of a package:
-
-\begin{verbatim}
-pkgexports ::= { ModName } "requires" { ModName }
-\end{verbatim}
-
-Here are the explicit headers of the packages in the introductory example:
-
-\begin{verbatim}
-package haskell98-base-sigs (Prelude)           requires (Prelude)
-package ghc-base-sigs       (Prelude, GHC.Base) requires (Prelude, GHC.Base)
-package p                   (A)                 requires (Prelude, GHC.Base)
-\end{verbatim}
-
-When you instantiate a package, an instance is identified by a \emph{package key},
-which what module each hole was instantiated with (or the module is put
-in a special \verb|HOLE| package if it was not instantiated at all, as you
-might when type-checking a package which still has holes in it):
-
-\begin{verbatim}
-PkgKey  ::= SrcPkgId "(" { ModName "->" Module } ")"
-          | HOLE
-\end{verbatim}
-
-A module might get instantiated multiple times (when its package is instantiated
-multiple times): a particular instance of a module is identified by the
-its enclosing package key plus its module name:
-
-\begin{verbatim}
-Module  ::= PkgKey ":" ModName
-\end{verbatim}
-
-To infer the provides and requires of a package, however, 
-
-The full pre-shape of a package, however, also specifies the module identities
-of everything it exports:
-
-\begin{verbatim}
-preshape ::= { ModName "->" Module } "requires" { ModName "->" Module }
-\end{verbatim}
-
-\begin{verbatim}
-haskell98-base-sigs
-    provides: Prelude  -> HOLE:Prelude
-
-ghc-base-sigs
-    provides: Prelude  -> HOLE:Prelude
-              GHC.Base -> HOLE:GHC.Base
-p
-    provides: A        -> p(Prelude  -> HOLE:Prelude,
-                            GHC.Base -> HOLE:GHC.Base):A
-\end{verbatim}
-
-
-Depending on how we vary how the requirements of a package are filled,
-the types and values defined in the package may be different.  So a
-mapping of required hole names to proper modules uniquely defines an
-instance of the package: we identify these instances with \emph{package
-keys} (\verb|PkgKey|).
-
-
-
-An example package key would be \verb|prelude-sig(Prelude -> base():Prelude)|,
-where \verb|prelude-sig| has a single requirement that was filled by the
-\verb|Module| \verb|base():Prelude|.
-
-\section{Defining shape}
-
-
-A \emph{shape} adds more information about the declarations that the
-module exports.  Nothing as fancy as a full type; just a \verb|Name|
-which identifies the name in question.  We'll say more about what
-\verb|Name|s are shortly, but the important property is that if two
-\verb|Name|s of two types are the same, they are type-equal (value-equal
-in the case of values).  We can thus define a shape as a mapping of
-module name to the set of \verb|Name|s it provides and the set of
-\verb|Name|s it requires.
-
-\begin{verbatim}
-Shape ::=
-    "provided:" { ModName "->" { Name } }
-    "required:" { ModName "->" { Name } }
-\end{verbatim}
-
-We should say a little bit about \verb|Name|s.  This terminology
-comes from the internals of GHC, where it is very useful to have a
-representation of identity that distinguishes a type from anything else.
-In old versions of GHC, a \verb|Name| was the source package ID (\verb|bytestring-0.1|)
-plus the module name it was defined in (\verb|Data.ByteString.Lazy|)
-plus the actual name of the type (\verb|ByteString|).  As a simplifying assumption
-in this document, we'll assume version numbers don't exist, but technically
-everywhere there is a package name in this document, there should also be
-a version number.
-
-In Backpack, this is \emph{still} not enough: we must also record
-the mapping from each required module name to the actual \verb|Module| which
-is fulfilling that requirement. Thus, the full specification of \verb|Name|
-(omitting version numbers) is:
-
-\begin{verbatim}
-Name    ::= Module "." OccName
-OccName ::= -- a plain old name, e.g. undefined, Bool, Int
-\end{verbatim}
-
-\newpage
-
-\begin{aside}
-\textbf{Mini-guru meditation.}  Why do we need the mapping of holes to modules? Consider:
-\begin{verbatim}
-package p (A) requires (H) where
-    signature H(T) where
-        data T
-    module A(A) where
-        import H
-        data A = A T
-package q (A1, A2) where
-    module H1(T) where
-        data T = T Int
-    module H2(T) where
-        data T = T Bool
-    include p (A as A1) requires (H as H1)
-    include p (A as A2) requires (H as H2)
-\end{verbatim}
-
-If we conclude that \verb|A1.T| $=$ \verb|A2.T|, that would be
-disaster!
-\end{aside}
-
-\begin{aside}
-\textbf{Guru meditation.} Why can't the \verb|PkgKey| just record a
-set of \verb|Module|s, e.g. \verb|PkgKey ::= SrcPkgKey { Module }|?  Consider:
-
-\begin{verbatim}
-package p (A) requires (H1, H2) where
-    signature H1(T) where
-        data T
-    signature H2(T) where
-        data T
-    module A(A(..)) where
-        import qualified H1
-        import qualified H2
-        data A = A H1.T H2.T
-
-package q (A12, A21) where
-    module I1(T) where
-        data T = T Int
-    module I2(T) where
-        data T = T Bool
-    include p (A as A12) requires (H1 as I1, H2 as I2)
-    include p (A as A21) requires (H1 as I2, H2 as I1)
-\end{verbatim}
-
-The sets of modules provided for both includions of \verb|p| are the same,
-but \verb|A12.A :: I1.T -> I2.T -> A12.A| while \verb|A21.A :: I2.T -> I1.T -> A12.A|.
-\end{aside}
-
-\newpage
-
-\begin{aside}
-\textbf{Guru meditation.} Why can't the required portion of a shape
-refer to \verb|OccName|s instead of \verb|Name|s, e.g. \verb|"required:" { ModName "->" { OccName } }|?  Consider:
-
-\begin{verbatim}
-package p () requires (A, B) where
-    signature A(T) where
-        data T
-    signature B(T) where
-        import T
-\end{verbatim}
-
-This has the shape:
-
-\begin{verbatim}
-provided: (empty)
-required:
-    A -> { HOLE:A.T }
-    B -> { HOLE:A.T }
-\end{verbatim}
-
-In particular, we conclude \verb|A.T| $=$ \verb|B.T|.
-\end{aside}
-
-\begin{aside}
-\textbf{Guru meditation.} Why do \verb|Name|s matter for values?  Consider:
-
-\begin{verbatim}
-package p (A) requires (H1, H2) where
-    signature H1(x) where
-        x :: Int
-    signature H2(x) where
-        import H1(x)
-    module A(y) where
-        import H1
-        import H2
-        y = x
-\end{verbatim}
-
-The reference to \verb|x| in \verb|A| is unambiguous, because it is known
-that \verb|x| from \verb|H1| and \verb|x| from \verb|H2| are the same (have
-the same \verb|Name|.)  If this was not known, it would be ambiguous and
-cause an error.
-\end{aside}
-
-\section{How to shape}
-
-\emph{You might consider skipping this section and reading some of the
-examples, before coming back.}
-
-Here is the core Backpack language (minus some syntactic sugar and
-ascription.)
-
-\begin{verbatim}
-package ::= "package" pkgname [pkgexports] "where" pkgbody
-pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
-pkgdecl ::= "module"    modid [exports] "where" body
-          | "signature" modid [exports] "where" body
-          | "include"   pkgname [inclspec]
-inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")" -- (provides list)
-             [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
-pkgexports ::= inclspec
-renaming ::= modid [ "as" modid ]
-\end{verbatim}
-
-Shaping proceeds in a few steps:
-
-\paragraph{Pre-shaping}  Pre-shaping recursively calculates the provided
-and required module names of packages.  Equivalently, it elaborates
-package declarations and includes so that \verb|pkgexports| and
-\verb|inclspec| are specified explicitly.
-
-The pre-shape of a package is calculated by processing declarations in
-order, calculating a set of provided module names $P$ (modules we are
-planning to expose outside the package), available module names $A$
-(modules which can be imported and fill requirements) and required
-module names $R$ (requirements that must be filled by a user of the
-package).  Then, absent a \verb|pkgexports|, the shape of the package is
-(provides: $P$, requires: $R$).
-
-\paragraph{Module} Given ``\verb|module M|'': let $P' = P \cup \{M\}$, $A' = A \cup \{M\}$ and $R' = R - \{M\}$. A module definition is both provided and available, and fills any requirement with the same name.
-
-\paragraph{Signature} Given ``\verb|signature S|'': let $R' = R \cup \{S\}$ if $S \notin A$, and no change otherwise. A signature definition creates a requirement if there is not already another definition available.  This definition could be another signature, in which case $S \in R$ already!
-
-\paragraph{Include}
-
-Let the pre-shape of the included package be (provides: $P_I$, requires: $R_I$). \\
-Given ``\verb|include pkgname (X0 as X'0, ..., Xn as X'n) requires (Y0 as Y'0, ..., Yn as Yn')|'':
-
-\begin{itemize}
-    \item Fail if \verb|X0, ..., Xn| $\nsubseteq P_I$
-    \item Fail if \verb|Y0, ..., Yn| $\nsubseteq R_I$
-    \item Let $A' = A \cup \{$ \verb|X'0, ..., X'n| $\}$
-    \item Let $R_0 = $
-    \item Let $R' = R - \{$ \verb|X'0, ..., X'n| $\} + \{$ \verb|Y'0, ..., Y'n| $\}$
-    \item Add \verb|InclRequires| minus \verb|Y0, ..., Yn| to $R$, for all not in $A$
-\end{itemize}
-
-If you have a sole \verb|Xi| in any renaming list, it is sugar for \verb|Xi as Xi|. When an
-\verb|inclspec| is absent, let the \verb|inclspec| be $P_I$ \verb|requires| $R_I$.
-
-\section{Definite packages are simple}
-
-When there aren't any signatures, package shapes are simple:
-given an identifier named \verb|T| declared in a module \verb|A| in a package \verb|p|,
-the module \verb|A| provides the name \verb|p():A.T|.  Thus
-
-\begin{verbatim}
-package p (A) where
-    module A(T,x) where
-        data T = T
-        x = False
-\end{verbatim}
-
-has the shape
-
-\begin{verbatim}
-provides:
-    A -> { p():A.T, p():A.x }
-requires:
-    (nothing)
-\end{verbatim}
-
-\paragraph{Reexports}  The Haskell source-language supports reexports.
-In such a case, the shape of the module reports the \emph{original}
-name.
-
-\begin{verbatim}
-package p(A,B) where
-    module A(T) where
-        data T = T
-    module B(T) where
-        import A
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    A -> { p():A.T }
-    B -> { p():A.T } -- not p():B.T!
-requires:
-    (nothing)
-\end{verbatim}
-
-Haskell does not support changing the \verb|OccName| upon reexport;
-the usual way of renaming types and values results in a new \verb|Name|.
-
-\begin{verbatim}
-package p (A,B) where
-    module A(T, x) where
-        data T = T
-        x = True
-    module B(S, y) where
-        import A
-        type S = T
-        y = x
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    A -> { p():A.T, p():A.x }
-    B -> { p():B.S, p():B.y } -- not p():A.T, p():A.x!
-requires:
-    (nothing)
-\end{verbatim}
-
-\begin{aside}
-\textbf{Guru meditation.}  If we can change \verb|OccName|s on reexport,
-we need a different definition of shape:
-\begin{verbatim}
-Shape ::=
-    "provided:" ModName "->" { OccName ":" Name }
-    "required:" ModName "->" { OccName ":" Name }
-\end{verbatim}
-
-Without \verb|OccName| renaming, the \verb|OccName| always equals
-the \verb|OccName| of the \verb|Name|.
-\end{aside}
-
-\section{Signatures in indefinite packages}
-
-If there is a signatures, we say its identifiers are from the special
-\verb|HOLE| package.  (These are a bit like skolem variables.)
-Signatures add to the requirement of a module shape
-in addition to the provides.
-
-\begin{verbatim}
-package p-sig (A) requires (A) where
-    signature A(T,x) where
-        data T
-        x :: Bool
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    A -> { HOLE:A.T, HOLE:A.x }
-requires:
-    A -> { HOLE:A.T, HOLE:A.x }
-\end{verbatim}
-
-\paragraph{No export}  You don't have to export a signature,
-but you must require it.  In that case, it is required but
-not provided.
-
-\begin{verbatim}
-package p-sig (B) requires (A,B) where
-    signature A(T) where
-        data T
-    signature B(S) where
-        import A
-        data S = S T
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    B -> { HOLE:B.S }
-requires:
-    A -> { HOLE:A.T }
-    B -> { HOLE:B.S }
-\end{verbatim}
-
-\paragraph{Reexports}  Signatures also support reexports. They
-work in the same way as in modules.
-
-\begin{verbatim}
-package p (A,B) where
-    signature A(T) where
-        data T = T
-    signature B(T) where
-        import A
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    A -> { HOLE:A.T }
-    B -> { HOLE:A.T }
-requires:
-    A -> { HOLE:A.T }
-    B -> { HOLE:A.T }
-\end{verbatim}
-
-Signatures can import modules too!
-
-\section{Modules in indefinite packages}
-
-When you define a module in a package with holes, when constructing
-the package key for names defined in this module, you must also specify
-how the holes in the package are filled in.  For example:
-
-\begin{verbatim}
-package p (A) requires (H) where
-    signature H where
-        x :: Bool
-    module A where
-        import H
-        y = x
-\end{verbatim}
-
-has shape
-
-\begin{verbatim}
-provides:
-    A -> { p(H -> HOLE:H):A.y } -- not p():A.y!
-requires:
-    H -> { HOLE:H.x }
-\end{verbatim}
-
-The mapping \verb|H -> HOLE:H| says that \verb|p| was instantiated with
-
-\section{Includes}
-
-An include brings the shape of the package included into the context
-of our package:
-
-\begin{verbatim}
-package p (A) where
-    module A(x) where
-        x = True
-
-package q (A, B) where
-    include A
-    module B(y) where
-        y = True
-\end{verbatim}
-
-\verb|p| provides \verb|A -> { p:A.x }|, while \verb|q| has shape:
-
-\begin{verbatim}
-provides:
-    A -> { p:A.x }
-    B -> { q:B.y }
-requires:
-    (nothing)
-\end{verbatim}
-
-If none of the module names from the included package and the
-current package overlap, things are simple. Things are more
-complex when there are overlapping names: in this case, \emph{linking}
-should occur.
-
-\paragraph{Renaming holes}
-
-If you rename a hole, the occurrences of \verb|HOLE:A| in modules and names
-are renamed:
-
-\begin{verbatim}
-package p (M) requires (A) where
-    signature A(x) where
-        x :: Bool
-    module M(y) where
-        import A
-        y = x
-
-package q (M) requires (B) where
-    include A (M) requires (A as B)
-\end{verbatim}
-
-has shapes:
-
-\begin{verbatim}
-p provides:
-    M -> { p(A -> HOLE:A):M.y }
-p requires:
-    A -> { HOLE:A.x }
-
-q provides:
-    M -> { p(A -> HOLE:B):M.y }
-q requires:
-    B -> { HOLE:B.x }
-\end{verbatim}
-
-\paragraph{Linking a signature with an implementation}
-
-If you fill a hole with an implementation, the occurrences of the hole's \verb|Module|, e.g. \verb|HOLE:A|, are replaced with the implementation module identity, and the
-occurences of the hole's \verb|Name|s, e.g. \verb|HOLE:A.x|, are replaced with
-the implementation's matching \verb|Name| (e.g., having the same \verb|OccName|).
-These are two separate substitutions!
-
-\begin{verbatim}
-package p (B) requires (A) where
-    signature A(T) where
-        data T
-    module B(T, x) where
-        import A(T)
-        x :: Bool
-
-package q (A, B) where
-    module A(T) where
-        data T = T
-    include p
-\end{verbatim}
-
-has shapes:
-
-\begin{verbatim}
-p provides:
-    B -> { HOLE:A.T, p(A -> HOLE:A):B.x }
-p requires:
-    A -> { HOLE:A.T }
-
-q provides:
-    B -> { q():A.T, p(A -> q():A):B.x }
-    A -> { q():A.T }
-q requires:
-    (nothing)
-\end{verbatim}
-
-Note that I can also include first and then define the module; the
-result is the same.
-
-\begin{aside}
-\textbf{Guru meditation.}  Why can't we just replace all occurrences of
-\verb|HOLE:A| with \verb|q():A|?  A modified \verb|package q|:
-
-\begin{verbatim}
-package q (TyA, A, B) where
-    module TyA(T) where
-        data T = T
-    module A(T) where
-        import TyA(T)
-    include p
-\end{verbatim}
-
-should have shape:
-
-\begin{verbatim}
-q provides:
-    TyA -> { q():TyA.T }
-    A   -> { q():TyA.T }
-    B   -> { q():TyA.T, p(A -> q():A):B.x }     -- NB: not p(A -> q():TyA)
-q requires:
-    (nothing)
-\end{verbatim}
-
-\verb|HOLE:A.T| is substituted with \verb|q():TyA.T|, but \verb|HOLE:A| is
-substituted with \verb|q():A|!
-\end{aside}
-
-\paragraph{Linking a signature with a signature}
-
-\begin{verbatim}
-package p requires (H) where
-    include base
-    signature H(Int) where
-        import Prelude
-
-package q requires (H) where
-    include base
-\end{verbatim}
-
-\end{document}