Type families + hs-boot files = unsafeCoerce

changed weight to 5

Attached file Bug.tar.gz (download).

Files in original report

Richard Eisenberg does it again! Ticket #9422 (closed) seems related. I support the proposed solution. (Note that the situation is different for module signatures ala #9252 (closed), because when we compile against a signature's hi file we can pull in the original implementation to get its type family instances for a consistency check.)

Ouch! I conjecture that the following lighter restriction will restore type soundness: a hs-boot file must list all type instance declarations used (transitively) in the typechecking of any definition whose declaration appears in the hs-boot file. (That is, a type instance declaration must be listed if its axiom would appear in the fully-unfolded elaborated Core term corresponding to any declaration in the hs-boot file.)

Even if this conjecture is correct, of course, this may be unreasonably hard to implement/explain.

changed weight to 7

Bumping priority here, as it exposes a hole in Safe Haskell.

Trac metadata

Trac field	Value
Priority	normal → high

mentioned in issue #10270

I think #10270 is related

Trac metadata

Trac field	Value
Related	→ #10270

Edward, you are familiar with this territory. Is this bug something you might look at?

Simon

Trac metadata

Trac field	Value
CC	→ ezyang

assigned to @ezyang

Sure, assuming we decide on a resolution.

A relaxation on Richard's proposal is to allow ONLY the left-hand side of type families to be specified in the hs-boot file. This is because we don’t really need the type families to reduce, unless people want them to, and reduces burden on hs-boot file writers, because having to pull in identifiers from the RHS could be pretty annoying. We'd need to add a new syntactic form for RHS-less type families.

As for normal instance declarations, the situation here is no worse than the classic diamond example, where two conflicting instances can be used without triggering an error, so I'm less inclined to demand that case.

After discussion with Richard

Note that B is never imported by anyone! (Although somehow GHC knows to link in B.o nevertheless.)
If B had been imported by some module, then the aggressive type-function overlap check would have detected the conflict with D. (Provided that the optimisation in that check, which avoids checking conflicts that have already been checked in some sub-tree, isn't fooled by B.hs-boot.)

Possible ways to fix (two variants of the same thing):

GHC should not link and run a program in which B.hs is never imported (only B.hs-boot is). That'd force the programmer to import B, and hence the overlap check would fire.
Alternatively, when GHC is preparing the list of modules to send to the linker, perform an overlap check on type functions, as if you were compiling module Top where { import Main; import B }. Where the "B" is the module(s) that are never imported by anyone except via {-# SOURCE #-}.

Richard likes (2); Simon likes (1). I'd go with whatever is easier to implement. But in (1) the error message should be clear and explicit.

Edward: thanks for the offer!

Some clarifications:

It would appear that we always do GhcMake dependency analysis when linking (there does not seem to be a way to feed GHC a list of object files to link together and coax it to skip linking), so it is sufficient to check that some correctness condition applies to boot files in the import graph.
If B is imported by another module which is not used by anyone, this will not cause the overlap check to find the overlap. So the condition is, more accurately, for each boot file, the implementing file must be transitively imported from the root of the module graph.

I'm pretty sure (1) is easiest to implement.

There does not seem to be a way to feed GHC a list of object files to link together and coax it to skip linking

Actually, this is not true:

ezyang@sabre:~$ ghc -c A.hs
ezyang@sabre:~$ ghc -c B.hs-boot
ezyang@sabre:~$ ghc -c C.hs
ezyang@sabre:~$ ghc -c B.hs
ezyang@sabre:~$ ghc -c D.hs
ezyang@sabre:~$ ghc -c Main.hs
ezyang@sabre:~$ ghc Main.o A.o B.o C.o D.o -o Unsafe
ezyang@sabre:~$ ./Unsafe
-5692549928996289131

Unfortunately, GHC has no idea about the dependency structure of the object files; for all it knows, it could have been produced by another compiler. So there actually is no way for GHC to figure out that B.o is type-unsafe in this case. This would imply the only way to safely link Haskell objects is to use ghc Main.hs (which will do dependency resolution.)

Note that Richard's original proposed fix will work in this case, since B.hs will be refused as B.hs-boot doesn't report enough type families.

Here is a thought: should this even really be reporting an error?

ezyang@sabre:~/Dev/haskell/T9562/p$ ghc --make D -fforce-recomp
[1 of 5] Compiling A                ( A.hs, A.o )
[2 of 5] Compiling B[boot]          ( B.hs-boot, B.o-boot )
[3 of 5] Compiling C                ( C.hs, C.o )
[4 of 5] Compiling B                ( B.hs, B.o )
[5 of 5] Compiling D                ( D.hs, D.o )

B.hs:8:15:
    Conflicting family instance declarations:
      type instance F a b -- Defined at B.hs:8:15
      type instance F a b -- Defined at D.hs:8:15

In the fix proposals that have been discussed here, we should only error upon *linking* conflicting instances together. However, we didn't really link B and D together, so really there shouldn't be any complaints. We're only seeing this family instance conflict because of the same problem as #10270.

Indeed, if you can convince ghc --make to compile things in a different order, no error occurs:

ezyang@sabre:~/Dev/haskell/T9562/p$ ghc --make B C D A -fforce-recomp
[1 of 5] Compiling A                ( A.hs, A.o )
[2 of 5] Compiling B[boot]          ( B.hs-boot, B.o-boot )
[3 of 5] Compiling C                ( C.hs, C.o )
[4 of 5] Compiling D                ( D.hs, D.o )
[5 of 5] Compiling B                ( B.hs, B.o )

This is 7.8; in 7.10 the compilation order is more stable so it seems harder to tickle this case; but you can twiddle the topsort code (reversing initial_graph in topSortModuleGraph seems to be enough) to get this behavior.

However, there is a very compelling counterexample: what happens when you compile into a library? The standard procedure for making a foo.a library are:

GHC compiles object files for all the modules.
Cabal calls ar to "link" a foo.a library.

Now a client of the library can use the incompatible modules, and once again, there is no way for a link time check to figure out that there is a problem, because once a Haskell module is put into a package we pretend hs-boot files don't exist.

Richard and I had a discussion, and we decided that solution 2 (when GHC is preparing the list of modules to send to the linker, perform an overlap check on type functions) is the only solution that works for linking together LIBRARY files (e.g. libfoo.a). Solution 1 does not work in this case, since when you link a library there isn't actually an executable to overlap check.

This has a consequence that (at least for safe usage) you can't just use ar to put .o files together: you must call GHC to do the overlap check. This means we need a new major mode for GHC, to do the overlap check for a set of modules (or even to just do the linking). The overlap check should be implied when --make is used. It's harmless for --make to report an overlap early (as is the case currently), but we must always do overlap check at the end, in case D is compiled before B (as was the case in 7.8). The overlap check can be skipped if there are no boot files.

Aside: There is an alternate strategy we can use which avoids the need for an overlap check at the very end. However, it requires that one-shot compilation be done in a specific order, so we don't think we should actually use it. Here's what you do: every A.hs/A.hs-boot pair induces a cycle of imports, which must be compiled before A.hs can be compiled. We always compile this cycle before we compile any other modules which depend on A.hs-boot. When compiling a module which transitively imports a boot file, we check if the real module has already been compiled; if so, we load it and add its instances to our environment. An instance which conflicts with the instance in A.hs will either be in a critical cycle, or not. If it is in the critical cycle, we will report overlap when A.hs is typechecked. Otherwise, we will load A.hi when typechecking the module and report overlap.

One silly way to enforce this ordering is, when compiling a module which transitively depends on a boot file, to produce a pre-hi file; only when the real module has been compiled, only then can you re-process the hi file to produce the real hi file.

mentioned in commit 23582b0c

added 1 deleted label

added hs-boot label

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Type families + hs-boot files = unsafeCoerce

Child items 0

Activity

Type families + hs-boot files = unsafeCoerce

Relates to

Activity