[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        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  backpack       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 **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 have any modules, and itself depends only on fully
 instantiated packages or signature packages.

 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. We add
 a pragma for controlling what declarations from packages get merged in:

 {{{
 signature A where
 {-# MERGE "sig-pkg" (T, S, foo, bar, baz) #-}
 data T
 qux :: T -> T
 }}}

 This line means, "merge in the declarations T, foo, bar, baz from the
 signature in sig-pkg." Two things to note:

 1. If `foo :: S`, you're obligated to also declare `S` in the import 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.

 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.

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