[GHC] #15691: Marking Pred(S n) = n as injective

[GHC]

#15691: Marking Pred(S n) = n as injective
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.6.1
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:  invalid           |  InjectiveFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by monoidal):

 * status:  new => closed
 * cc: goldfire (added)
 * resolution:   => invalid


Comment:

 Yes, it's a known limitation. See
 [http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-
 jones_eisenberg_injectivity.pdf "Injective Type Families for Haskell"],
 section 4.1, "Awkward Case 2".

 By definition of `Pred` we have `Pred (S (Pred Zero)) ~ Pred Zero`. If
 `Pred` is recognized as injective, then `Zero ~ S (Pred Zero)`, which is a
 contradiction. The problem is that `Pred Zero` is a valid type, even
 though it's outside of the domain of `Pred`. See also #9636.

 The
 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs
 Constrained Type Families] paper resolves this by representing the domain
 of the type function as a constraint. I don't know if there are plans to
 implement it.

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