[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:
----------------------------------------------+----------------------------

Comment (by goldfire):

 I'm confident that any ill-behaved `G` ''would'' require
 `UndecidableInstances`. But, note that while that extension is needed in
 order to ''define'' `G`, it is not needed in order to ''use'' `G`. So,
 even if you do not have `UndecidableInstances` in your module, you are
 still under threat from such an attack.

 Looking at the example in #8162, the problem would be exactly the same if
 the family `F` (the equivalent to your `Bad`) were a closed type family.
 Open type families `LA` and `LB` are used to expose the crash, but the
 family with the overlap could be made closed, as all of its instances are
 declared together. Note that `F` is defined ''without''
 `UndecidableInstances`.

 There is the possibility that some very clever analysis (and restrictions
 on things like `G` and/or `UndecidableInstances`) could allow `Bad` to
 behave as you might like. Indeed, we haven't actually proved type safety
 in the presence of non-linear (i.e., with a repeated variable on the LHS)
 and non-terminating type families, even taking infinite unification into
 account. That proof seems to require a solution to a recognized
 [http://www.win.tue.nl/rtaloop/problems/79.html open problem]. This lack
 of a proof actually extends to ''open'' type families as well -- the
 published proofs about non-terminating open type families implicitly (and
 very subtly) assumed linear patterns. After spending a Long Time working
 on this proof and failing to either find a proof or a counterexample, we
 (the authors of the "Closed Type Families" paper) were happy enough to
 conjecture type safety and keep non-linear patterns in the language.

 All of this does add up to a slightly bumpy surface area for the closed
 type families feature. I'm quite aware of this and am somewhat
 disappointed about it. But, my thought is not to let the great become the
 enemy of the good here -- most uses of closed type families work in an
 intuitive way and are really helpful to people. Then, some uses work in a
 really unintuitive way, and people get confused. I still think it's a good
 trade-off.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9082#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler