#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: As far as I can tell, GHC is doing the right thing here, but "the right thing" is subtle, indeed. We're at the intersection of closed type families, non-linear patterns, and infinite types, and that is a strange place indeed. I encourage you to read Section 6 of [http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf the closed type families paper]. I will try to apply the logic there to your situation. Let's focus on your first (simpler) example, as I think the reasoning there extends to the more complicated one in your most recent comment: {{{ type family Bad a b where Bad (f a) a = False Bad a a = True }}} Now, consider the following beast: {{{ type family G a where G a = Maybe (G a) }}} How can we reduce the target `Bad (G Int) (G Int)`? The first equation doesn't seem to match, and the second does. But, now we must do the apartness check with the first equation... is it ever possible for the first one to match? Sure it is, if the first `(G Int)` steps to `(Maybe (G Int))` (with `f |-> Maybe` and `a |-> G Int`). So, the first equation isn't apart from our target, so the second equation can't be used. Perhaps GHC will be clever enough to reduce the first `(G Int)` and then apply the first equation, but I wouldn't hold my breath. How does this affect you, without such a `G`? If we try to reduce a target `Bad x x`, GHC will be stuck. The first equation clearly doesn't match, and the second equation does. But, the first equation is ''not'' apart from `Bad x x`, because of the possibility that someone will define `G` and then instantiate `x` with `G Int`. This case is ''subtle'', and it took years of living with type families before we realized that this bizarre situation can actually cause a crash with open type families. See #8162. Though that bug deals with open families, I can imagine an adaptation that would cause a crash with closed ones. An ideal world would produce an error report with a link to the paper, etc., in your situation, but detecting the situation is hard -- I believe we would have to run both the infinite unification algorithm as well as a normal unification algorithm, notice that the results are different, and then know we are in this place. I'm happy to see suggestions for a better way. If you do have suggestions, do please reopen. Or, perhaps it's worth putting in a feature request for a better error message, even without a way to achieve that goal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler