#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