[GHC] #11511: Type family producing infinite type accepted as injective

[GHC]

#11511: Type family producing infinite type accepted as injective
-------------------------------------+-------------------------------------
        Reporter:  jstolarek         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  Injective
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Perhaps this counterexample is why I could never finish that proof. I
 don't believe I ever reached for an assumption of finite types, probably
 conflating the notion of finite types with terminating type families.

 What bothers me is that we have no guarantee that FC types are indeed
 finite. On paper, we just define types inductively and are done with it.
 But how does this play out in the implementation? Recall that infinite
 types have led to segfaults before: #8162.

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