Opened 5 years ago

Last modified 3 years ago

#9562 new bug

Type families + hs-boot files = unsafeCoerce

Reported by: goldfire Owned by: ezyang
Priority: high Milestone:
Component: Compiler Version: 7.8.3
Keywords: TypeFamilies, SafeHaskell hs-boot Cc: ezyang
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: #10270 Differential Rev(s):
Wiki Page:

Description

Consider the following bundle of modules:

A.hs:

{-# LANGUAGE TypeFamilies #-}

module A where

type family F a b

B.hs-boot:

module B where

import A

oops :: F a b -> a -> b

B.hs:

{-# LANGUAGE TypeFamilies #-}

module B where

import A
import C

type instance F a b = b

oops :: F a b -> a -> b
oops = const

C.hs:

module C (oops) where

import {-# SOURCE #-} B

D.hs:

{-# LANGUAGE TypeFamilies #-}

module D where

import A
import C

type instance F a b = a

unsafeCoerce :: a -> b
unsafeCoerce x = oops x x

Main.hs:

module Main where

import D ( unsafeCoerce )

main = print $ (unsafeCoerce True :: Int)

When loading these into GHCi, we quite reasonably get a type family instance overlap error. But, separate compilation leads to disaster:

rae:01:49:47 ~/temp/bug> ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.8.3
rae:01:49:49 ~/temp/bug> ghc -c A.hs
rae:01:49:53 ~/temp/bug> ghc -c B.hs-boot 
rae:01:49:58 ~/temp/bug> ghc -c C.hs
rae:01:50:09 ~/temp/bug> ghc -c B.hs
rae:01:50:13 ~/temp/bug> ghc -c D.hs
rae:01:50:17 ~/temp/bug> ghc Main.hs -o Unsafe
[6 of 6] Compiling Main             ( Main.hs, Main.o )
Linking Unsafe ...
rae:01:50:23 ~/temp/bug> ./Unsafe
2882303761534249061

Yikes!

Proposed (terrible) solution: hs-boot files must list all type instance declarations in the corresponding modules. It may also be a good idea to require all normal instance declarations in the hs-boot file as well, because this same trick can be used to introduce incoherence (I think -- haven't tested).

This bug persists even if Main declares that it is Safe.

I've attached a tarball of the files for ease of testing.

(Credit to Edward Yang and Geoff Mainland, whose discussion provoked the line of inquiry that led to this discovery.)

Attachments (1)

Bug.tar.gz (464 bytes) - added by goldfire 5 years ago.
Files in original report

Download all attachments as: .zip

Change History (18)

Changed 5 years ago by goldfire

Attachment: Bug.tar.gz added

Files in original report

comment:1 Changed 5 years ago by ezyang

Richard Eisenberg does it again! Ticket #9422 seems related. I support the proposed solution. (Note that the situation is different for module signatures ala #9252, 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.)

comment:2 Changed 5 years ago by adamgundry

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.

comment:3 Changed 5 years ago by goldfire

Priority: normalhigh

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

comment:4 Changed 5 years ago by goldfire

I think #10270 is related

comment:5 Changed 5 years ago by simonpj

Cc: ezyang added

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

Simon

comment:6 Changed 5 years ago by ezyang

Owner: set 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.

comment:7 Changed 5 years ago by simonpj

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):

  1. 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.
  1. 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!

comment:8 Changed 5 years ago by ezyang

Some clarifications:

  1. 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.
  1. 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.

comment:9 Changed 5 years ago by ezyang

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.

comment:10 Changed 5 years ago by ezyang

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.

Version 5, edited 5 years ago by ezyang (previous) (next) (diff)

comment:11 Changed 5 years ago by ezyang

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.

comment:12 Changed 5 years ago by Edward Z. Yang <ezyang@…>

In 23582b0c16bb147dad6bd7dee98686a8b61eacea/ghc:

Add failing test for #9562.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

comment:13 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:14 Changed 4 years ago by thomie

Keywords: SafeHaskell added

comment:15 Changed 4 years ago by ezyang

Keywords: hs-boot added

comment:16 Changed 3 years ago by rwbarton

With the caveat that I don't feel like I fully grok type checking in the middle of an import cycle, let me offer a variant on goldfire's and adamgundry's proposals: When we type check a module that has an hs-boot file (here B.hs), do so in the type family instance environment of B.hs-boot. In other words, allow type family instances in hs-boot files and require of the user that if they want to use a type family instance while compiling B.hs, it must already be present in B.hs-boot.

This is more lenient than "every type family in B.hs must be listed in B.hs-boot" and I think it's a clearer or at least more implementable version of adamgundry's "must list all type instance declarations used (transitively) in the typechecking of [...]". Maybe it's even exactly equivalent to that.

comment:17 Changed 3 years ago by goldfire

rwbarton's comment:16 looks very plausible. I can't quite convince myself that it's right, but I also can't think of a counterexample. It's certainly easier to explain (and likely to implement) than many other solutions mentioned here.

Note: See TracTickets for help on using tickets.