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-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
A
s 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-boot
s 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-boot
s 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-boot
file; instead, we just put in everything that we *can* handle in anhs-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. - 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-boot
stub before we conclude that the types have not changed (as opposed to with separatehs-boot
files, where a modification tohs
would 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-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) thehs-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. - 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 thehs-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 theEq
instance 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-boot
needs a way of transitively(!) excluding these definitions fromhs-boot
files. We can exclude things from the boot file in the following way:
- 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 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.