
The straw-man proposal is that with `{-# UNDECIDABLE #-}` (or some other
#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:15 simonpj]: pragma name) on a closed type family, the surely-apart check is strengthened, allowing more reductions to fire. This seems to be precisely my {-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma. Declaring this property of a type function seems orthogonal to whether or not evaluating the function terminates -- I could see both `{-# UNDECIDABLE #-}` and `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` as separate pragmas, where neither implies the other. The first means that GHC might not terminate; the second means your program might not be type-safe.
Richard, you rightly point out that if you put that on `Equal`, then
`Equal x [x]` would return `False`, as you'd expect if all types were finite. But you also claim that if you can define an infinite type, then you can get `unsafeCoerce`. I believe you (c.f Section 6 of the [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ Closed Type Families paper]). But can you exhibit an example? See #8162. That example uses open type families, and will compile and seg- fault with 7.6.3. The improved checking in 7.8.x stops compilation. However, an open type family with all of its instances in one module (such as `F` in #8162) is fully equivalent to a closed type family (with equations in any order). Why? Because all open type family instances must be ''compatible'', and a closed type family where all the equations are compatible skips the apartness check during reduction. (See the closed type families paper for details.) Thus, if we did the wrong apartness check (that is, ignored the possibility of infinite types) in 7.8.x, then an example along the lines of #8162 would cause a seg-fault.
And if you can, can you translate it back into an example using
overlapping classes, probably with equality superclasses? If so, perhaps our existing compiler is unsound! I tried and failed at this, and I've decided it's impossible. Without using type families, classes introduce no new type axioms -- even with equality superclasses. Without any axioms, the proof of progress of FC is quite straightforward and has no surprises. Thus, any program with an implementation of `unsafeCoerce` must fail to be well-typed in FC. So, barring Core Lint errors, this trick shouldn't be possible. So, I maintain my earlier position: what we have now is sound, but perhaps unpredictable in extreme cases. I ''do'' think we should make the class overlap check echo the type family overlap check, but I don't think there's a soundness issue here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler