[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
#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.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following does not work: {{{#!hs {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-} import GHC.TypeLits (Nat, type (-)) type family Replicate (n :: Nat) (a :: k) = (r :: [k]) | r -> n where Replicate 0 a = '[] Replicate n a = a ': Replicate (n - 1) a }}} It fails to compile with the following error: {{{ error: • Type family equation violates injectivity annotation. Type variable ‘n’ cannot be inferred from the right-hand side. In the type family equation: forall (k :: BOX) (n :: Nat) (a :: k). Replicate n a = a : Replicate (n - 1) a • In the equations for closed type family ‘Replicate’ In the type family declaration for ‘Replicate’ Failed, modules loaded: none. }}} However, the following does: {{{#!hs {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-} data Nat = Zero | Succ Nat type family Replicate (n :: Nat) (a :: k) = (r :: [k]) | r -> n where Replicate Zero a = '[] Replicate (Succ n) a = a ': Replicate n a }}} Sure GHC.TypeLits' built-in Nat type is isomorphic to the one defined above, and thus GHC should be able to infer injectivity for Replicate? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 duairc): * version: 7.10.2 => 7.11 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 duairc): You're right, they are subtley different. But I can't "pattern-match" on (n + 1) on the LHS with GHC's TypeLits, because + is a type family and not a constructor. If there was some other way I could accomplish this then I would be satisfied with that for now. But obviously if we could get generalised injectivity that we be awesome. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): You're absolutely right -- there is no way to fix the `TypeLits` style, until we have generalized injectivity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 duairc): Could it not be possible to introduce some way of pattern-matching on {{{GHC.TypeLits}}}'s {{{Nat}}}s independently of generalised injectivity? Maybe it's a question that would involve a lot of bikeshedding... but surely the compiler ultimately has enough information to prove that {{{Replicate}}} is injective, I just can't destructure type-level {{{Nat}}}s. Could there be a magic built-in pattern synonym {{{Succ}}} for {{{Nat}}}s? Can pattern synonyms work on the type level? I don't really know much about the internals to know how to implement that, but there must be a way. Like if full generalised injectivity is just around the corner, then maybe we should just wait for that, but from what I've read it sounds like there are still a lot of kinks that need to be worked out first and it might turn out to be too difficult altogether? Right now pretty much every package that does type-level stuff defines its own {{{Nat}}} type, and I'd imagine the lack of the ability to pattern match on {{{GHC.TypeLits}}}'s {{{Nat}}} is a big part of the reason for that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 jstolarek): Replying to [comment:6 goldfire]:
I do think that generalized injectivity is the fastest way toward what you want, though. Note however, that generalized injectivity will not make it into 8.0 (unless miracle happens), which means over a year of waiting until it makes it into next stable release.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11207#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC