[GHC] #11207: GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on user-defined Nat kind

[GHC]

#11207: GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat,
but can for equivalent type family operating on user-defined Nat kind
-------------------------------------+-------------------------------------
        Reporter:  duairc            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.11
      Resolution:                    |             Keywords:
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):

 Type-level pattern synonyms would be great. But no one is working on that,
 I'm afraid. The way that type patterns are implemented now would make this
 difficult, but I'm planning on refactoring it in the near future (next
 month, probably). Once that is done, I don't imagine it would be hard to
 have type-level pattern synonyms. And then we might be able to provide the
 pattern-matching on `TypeLits` that we all want.

 I do think that generalized injectivity is the fastest way toward what you
 want, though.

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