#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: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: jstolarek (added) Comment: But your definitions are subtly different. In the !TypeLits case, you're using `-` in the RHS. `-` is not injective. So GHC quite correctly rejects the equation. In the corresponding equation without !TypeLits, there are no function calls on the right; instead, you use pattern-matching on the left to get what you want. If you implement a `-` over your unary `Nat` and write the definitions the same way, GHC will reject the non-!TypeLits definition, too. What this requires is "generalized injectivity", where we could say {{{ type family (a :: Nat) - (b :: Nat) = (r :: Nat) | r a -> b, r b -> a }}} We've considered such a thing, but we have yet to work out all the details, if I recall correctly. In any case, if this existed, then GHC would be able to accept the first definition. Adding in Janek, who is Mr. Injective-Type-Families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler