#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:10 simonpj]:
I conclude from this thread that * `OverlappingInstances` should probably obey the same rules as closed type families, for consistency.
Generally agreed here, with the same reservations that Simon writes.
I suppose that we could lift the restriction (ie strengthen the "surely-
* I believe that the unpredictability only strikes if you have infinite types, via a looping type family. And a programmer might well be willing to guaranteed that will not occur. * In that sense, it's a bit like `-XUndecidableInstances`: the
apart" check) if some flag is set: programmer takes responsibility.
* And, as such it should probably be a per-type-family (or per-closed- type-family) pragma, rather than a global flag. Maybe even `{-# UNDECIDABLE #-}`.
I'm not sure exactly what you mean here (mostly). The `{-# UNDECIDABLE #-}` route is almost surely a good idea, independent of anything else, as it follows the new pattern started by `{-# OVERLAPPABLE #-}` and friends. But, critically, a dangerous use of a strengthened apartness check would happen on a family '''without''' this pragma. For example: {{{ type family Equals a b where Equals a a = True Equals a b = False }}} This clearly has no loops and should compile without `{-# UNDECIDABLE #-}`. Yet, if we use the strengthened apartness check when choosing to reduce by the second equation, we can get into trouble. Specifically, should `Equals x [x]` reduce to `False`, for some skolem `x`? If, in some future module, we introduce `type family Loop where Loop = [Loop]`, then it would be terrible to have reduced `Equals x [x]` to `False`. But, of course, we have no way of knowing if `Loop` will come into being in the future. The nub of the problem, as I see it, is that the safety (for closed type families) or predictability (for class instances) of the system depends on some '''global''' no-looping property. I could see some `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma that could be put on `Equals` that would enable the stronger check and let the programmer bear the safety burden. However, this is a significant departure from other "let the programmer beware" issues in that, for closed type families, you can abuse this ability to implement `unsafeCoerce`. (This would not be the case for class instances.) So, getting back to Simon's proposal: what's your suggested behavior? I see what you want with `{-# UNDECIDABLE #-}`, but I don't see precisely how it would influence the apartness check. If we are going to start treating undecidable instances as different than regular ones, it would be worthwhile to make the termination checker smarter. Right now, a standard Peano multiplication type family requires `-XUndecidableInstances`. I think the assumed safety of that extension (I think folks are OK with a perhaps-looping compiler, as long as the produced binary, if any, is type-safe) allows people to use it without much hesitation, so there has been little (no?) pressure to improve the termination checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler