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

 > I think the right solution here would be to drop equation (7) from our
 algorithm in the paper.

 On a second thought I don't think this would be good idea.  Doing this
 would mean that using any type family in the RHS is prohibited for
 injective type families and we definitely don't want that for generalized
 injectivity.

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