This is a new proposal for solving #1409. The big addition here is that we create **two** hs-boot files for each hs file: one that is a full hs-boot file to be imported by hs files to break loops, and a second which only includes abstract types for hs-boot files to import. C.f. #10679 (closed)

• *Discussion.** Here is a slightly goofy hs-boot file I've excerpted from GHC:

module Packages where

import {-# SOURCE #-} Module (PackageKey)
import {-# SOURCE #-} DynFlags (DynFlags)

packageKeyPackageIdString :: DynFlags -> PackageKey -> Maybe String

The hs-boot file must itself import hs-boot files, because this boot file is used by Module and DynFlags; without {-# SOURCE #-}, the boot file itself will participate in a cycle!

But notice that there is something very interesting: a boot file is ONLY ever interested in importing other modules to get types. Never to import constructors or functions!

We can use this observation to give us a mechanical transformation of an hs file to an hs-boot file, ASSUMING we can define a "second level" of hs-boot file to record our abstract types.

• *Example.** In this example, we have chosen to break the loop from As import to B.

module A where
  import {-# SOURCE #-} B
  data A = A B
  f :: A -> Bool
  f (A (B (A b))) = g b
  f _ = True

module B where
  import A
  data B = B A
  g :: B -> Bool
  g (B (A (B b))) = f b
  g _ = False

The first-level hs-boots are:

module A where -- not actually used
  import {-# SOURCE 2 #-} B
  data A = A B
  f :: A -> Bool

module B where
  import {-# SOURCE 2 #-} A
  data B = B A
  g :: B -> Bool

The second-level hs-boots are:

module A where
  data A

module B where -- not actually used
  data B

• *Commentary.** Here are some remarks:

1. Because we have to lift the transitive dependencies of anything we {-# SOURCE #-} import, it doesn't make sense to have a pragma which explicitly says what to put in the hs-boot file; instead, we just put in everything that we *can* handle in an hs-boot file (so exclude anything with missing type signatures, type families, etc.) Ideally, these automatic hs-boot files are generated lazily, but they should be reused as necessary.
2. This facility actually makes {-# SOURCE #-} a lot more attractive for increasing separate compilation: you can mark an import {-# SOURCE #-} to ensure that if its implementation changes, you don't have to recompile this module / you can build the module in parallel with that module. The downside is that when the imported file is modified, we have to regenerate the hs-boot stub before we conclude that the types have not changed (as opposed to with separate hs-boot files, where a modification to hs would not bump the timestamp on hs-boot.
3. With Haskell98, you should never need more than two levels of hs-boot nesting. However, with data kind promotion, you may need arbitrarily many levels of nesting. You could simply exclude promoted data kinds ala **Handling unsupported boot features**; however an alternate thing to do is generalize hs-boot to arbitrarily many levels. However, this might be annoying to implement because dependency analysis needs to know how to determine universe stratification so it can tell how many levels of hs-boot are necessary.
4. We can't force the first level of hs-boot files to be abstract types, for two reasons: (1) a source file importing the hs-boot file may really need the selector/constructor, and (2) the hs-boot files will reflect any cycles from the source files, that's no good! Rolling out to the second level breaks the cycle because abstract types never need any imports.
5. What about type class instances? I propose that instances be lifted to the hs-boot level (so hs file usages of the instance continue to work), but not the hs-boot2 level (so that we can still "bottom out"). This can result in some slightly unintuitive behavior, however:

module A where
  instance Eq (a -> b) where ...
module B where
  import A
module C where
  import {-# SOURCE #-} B

In this case, C would NOT see the Eq instance for functions defined in A.

• *Handling unsupported boot features.** Some type-level features in Haskell are not supported at the boot-level (type families, etc), so the automatic generation of hs-boot needs a way of transitively(!) excluding these definitions from hs-boot files. We can exclude things from the boot file in the following way:

1. If a declaration is not liftable to the hs-boot file, we replace it with a "not bootable" declaration, which specifies that there is something with this Name, but we don't have any information about it. (This is a sort of generalized version of an abstract type).
2. If we are type-checking a declaration and make reference to a not bootable declaration, the full declaration itself is considered not bootable.

Alternately, we can just make sure all language features are supported in boot files.