#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