[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 haasn):

 Thanks for the feedback.

 As I understand it, {{{G}}} breaks this because it actually expands to an
 infinite type, and hence breaks my assumption that {{{f a ~ a}}} is
 impossible. This is also the reason why it requires
 {{{UndecidableInstances}}}.

 However, it is also my understanding that this type of infinite type
 family expansion is actually undecidable, in that answering {{{:k! Bad (G
 Int) (G Int)}}} actually fails to terminate.

 Do you know if there's an example of such a similarly ill-behaved {{{G}}}
 that either doesn't require {{{UndecidableInstances}}} or otherwise
 terminates with an incorrect result/breaks the type system if resolving
 {{{Bad}}} according to the reasoning outlined earlier?

 As of now, I don't grok why this would be an actual problem. I'll probably
 have to look at the papers involved and also #8162 to answer this myself,
 but I thought I'd quickly ask here first.

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