[GHC] #9562: Type families + hs-boot files = unsafeCoerce
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: GHC Blocked By: | accepts invalid program Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Consider the following bundle of modules: A.hs: {{{#!hs {-# LANGUAGE TypeFamilies #-} module A where type family F a b }}} B.hs-boot: {{{#!hs module B where import A oops :: F a b -> a -> b }}} B.hs: {{{#!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: {{{#!hs module C (oops) where import {-# SOURCE #-} B }}} D.hs: {{{#!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: {{{#!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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: accepts invalid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: accepts invalid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * priority: normal => high Comment: Bumping priority here, as it exposes a hole in Safe Haskell. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * related: => #10270 Comment: I think #10270 is related -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * cc: ezyang (added) Comment: Edward, you are familiar with this territory. Is this bug something you might look at? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by ezyang): * owner: => ezyang Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. 2. 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. 2. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
There does not seem to be a way to feed GHC a list of object files to
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ezyang): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ezyang): Here is something curious: {{{ 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 }}} however, {{{ 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 ) }}} I don't know why in the latter case no error is reported. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: ezyang
Type: bug | Status: new
Priority: high | Milestone:
Component: Compiler | Version: 7.8.3
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC accepts | Unknown/Multiple
invalid program | Test Case:
Blocked By: | Blocking:
Related Tickets: #10270 | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Edward Z. Yang
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: TypeFamilies, | SafeHaskell hs-boot Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ezyang): * keywords: TypeFamilies, SafeHaskell => TypeFamilies, SafeHaskell hs-boot -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: TypeFamilies, | SafeHaskell hs-boot Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9562: Type families + hs-boot files = unsafeCoerce -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ezyang Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: TypeFamilies, | SafeHaskell hs-boot Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #10270 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9562#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC