[GHC] #9082: Unexpected behavior involving closed type families and repeat occurrences of variables

[GHC]

#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