Teach GHC to interpret all hs files as two levels of hs-boot files (abstract types only/full types + values)
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-bootfile 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 toB.
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:
- 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 thehs-bootfile; instead, we just put in everything that we *can* handle in anhs-bootfile (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. - 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 thehs-bootstub before we conclude that the types have not changed (as opposed to with separatehs-bootfiles, where a modification tohswould not bump the timestamp onhs-boot. - 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.
- We can't force the first level of
hs-bootfiles to be abstract types, for two reasons: (1) a source file importing the hs-boot file may really need the selector/constructor, and (2) thehs-bootfiles 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. - What about type class instances? I propose that instances be lifted to the
hs-bootlevel (so hs file usages of the instance continue to work), but not thehs-boot2level (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,
Cwould NOT see theEqinstance for functions defined inA.
- *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-bootneeds a way of transitively(!) excluding these definitions fromhs-bootfiles. We can exclude things from the boot file in the following way:
- If a declaration is not liftable to the
hs-bootfile, we replace it with a "not bootable" declaration, which specifies that there is something with thisName, but we don't have any information about it. (This is a sort of generalized version of an abstract type). - 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.