[GHC] #12994: Module and export level signature thinning in Backpack

[GHC]

#12994: Module and export level signature thinning in Backpack
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  backpack
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by ezyang:

@@ -17,2 +17,1 @@
- it does not have any modules, and itself depends only on fully
- instantiated packages or signature packages.
+ it does not export any modules.
@@ -29,2 +28,3 @@
- By default, all signatures in scope at a name get merged to a name. We add
- a pragma for controlling what declarations from packages get merged in:
+ By default, all signatures in scope at a name get merged to a name.
+ However, by specifying the export list of a signature, we can control
+ which declarations from signature packages come into scope:
@@ -33,2 +33,1 @@
- signature A where
- {-# MERGE "sig-pkg" (T, S, foo, bar, baz) #-}
+ signature A (T, foo) where
@@ -36,1 +35,0 @@
- qux :: T -> T
@@ -39,2 +37,4 @@
- This line means, "merge in the declarations T, foo, bar, baz from the
- signature in sig-pkg." Two things to note:
+ Notice that `foo` is not mentioned in the body of the signature A: in this
+ case, foo is expected to come from a signature from a signature package.
+ If the signature from the signature package also require bar, that
+ requirement is NOT included in A.
@@ -42,1 +42,3 @@
- 1. If `foo :: S`, you're obligated to also declare `S` in the import list,
+ Two things to note:
+
+ 1. If `foo :: S`, you're obligated to also declare `S` in the export list,
@@ -44,1 +46,2 @@
- always explicit what is going to be required in the end.
+ always explicit what is going to be required in the end. GHC will give an
+ error if this is not true.
@@ -46,13 +49,5 @@
- 2. Even if `T` is in the merge list, you still have to declare it locally
- if you want to make use of it. These are not imports!
-
- (:TODO: There is no provision for disambiguating between two signatures
- from the same package, but mix-linked differently. This seems like a
- pretty rare case.)
-
- The semantics is that we proceed as we do now, but when merging, we apply
- the explicit import list to reduce the set of entities we actually
- typecheck and merge in (checking, however, to ensure that these are all
- well-formed.)
-
- That's it, I think.
+ 2. If you depended upon a library that had requirements and exposed
+ modules, you can't thin declarations from the signature this way: they are
+ always exported, no matter if they're specified in the export list or not.
+ But we'll attach warnings to these if you actually try to use them. (Maybe
+ we really should filter them out of things that are brought into scope)

New description:

 **The problem.** We want to write signature packages to allow us to reuse
 signatures, but Backpack in its current incarnation forces us to depend on
 ALL of the signatures from the signature package. This is troublesome if
 we only really needed a subset of the signatures from the package. What
 we'd like is a way to "thin" out the signatures, keeping only the ones we
 need.

 In the original design of Backpack, this was not allowed, because if a
 signature was requiring a function so that a module from that package
 could use it, you're not permitted to just drop that requirement (someone
 really needs it!) But signature packages: packages that consist of only
 signatures (no modules) do not have any such requirement. So let's allow
 module and export level signature thinning here.

 **Design.** First, during the course of mix-in linking we infer if a
 package is a signature package or not. A package is a signature package if
 it does not export any modules.

 A signature package is eligible for requirement thinning. A signature
 package can be thinned at the module level using the `signature-mixins`
 field, by saying `include-signatures: sig-pkg (A)` (we don't reuse
 `mixins` field to distinguish signature packages from regular indefinite
 packages); this means that we only are bringing the signature `A` into
 scope. If `A` imports another signature `B`, the user is obligated to also
 bring that signature into scope (if they do not, we will error, although
 this can only be done by GHC.)

 By default, all signatures in scope at a name get merged to a name.
 However, by specifying the export list of a signature, we can control
 which declarations from signature packages come into scope:

 {{{
 signature A (T, foo) where
 data T
 }}}

 Notice that `foo` is not mentioned in the body of the signature A: in this
 case, foo is expected to come from a signature from a signature package.
 If the signature from the signature package also require bar, that
 requirement is NOT included in A.

 Two things to note:

 1. If `foo :: S`, you're obligated to also declare `S` in the export list,
 even if you are not otherwise using it. The reason for this is to make it
 always explicit what is going to be required in the end. GHC will give an
 error if this is not true.

 2. If you depended upon a library that had requirements and exposed
 modules, you can't thin declarations from the signature this way: they are
 always exported, no matter if they're specified in the export list or not.
 But we'll attach warnings to these if you actually try to use them. (Maybe
 we really should filter them out of things that are brought into scope)

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12994#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler