#12057: TypeFamilyDependencies on GHC.Generic's `Rep` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective 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 Iceland_jack): `Rep1` also -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12057: TypeFamilyDependencies on GHC.Generic's `Rep` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective 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 RyanGlScott): `Rep` definitely isn't injective. Counterexample: `Rep (Proxy Int)` = `Rep (Proxy Char)`, but `Int` is not `Char`. `Not` can certainly be made injective though, and this would be simple to do and useful. Would you care to make a patch for it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12057: TypeFamilyDependencies on Data.Type.Bool's `Not` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective, newcomer 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 Iceland_jack): Replying to [comment:3 RyanGlScott]:

`Rep` definitely isn't injective. Counterexample: `Rep (Proxy Int)` = `Rep (Proxy Char)`, but `Int` is not `Char`.

Interesting, thank you. Would this be covered by the weaker [https://ghc.haskell.org/trac/ghc/ticket/6018#comment:48 ‘head’-injectivity]? Is there any benefit from adding this distinguishing information/kind information to the metadata (since `Proxy` is polykinded)? I am perversely working backwards from the perspective of injectivity but there may be a use for `TypeRep`s in the `Rep`.

`Not` can certainly be made injective though, and this would be simple to do and useful. Would you care to make a patch for it?

Sure, it can be kept open for more injective type families in base. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12057: TypeFamilyDependencies on Data.Type.Bool's `Not` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective, newcomer 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 RyanGlScott): Replying to [comment:5 Iceland_jack]:

Interesting, thank you. Would this be covered by the weaker [https://ghc.haskell.org/trac/ghc/ticket/6018#comment:48 ‘head’-injectivity]?

In principle, it should be. Ever since we added [https://ghc.haskell.org/trac/ghc/ticket/10030 packageName] to the generics metadata, every `Rep` instance should be uniquely identified by the package, module, and datatype name of the underlying datatype, so I think `Rep`s are unique modulo type variables. I say "in principle" because although most `Generic` instances (and hence `Rep` instances) are derived, a devilish programmer //could// handwrite a `Rep` instance that violates injectivity. However, it's strongly discouraged to do such a thing (for instance, you can't handwrite `Generic` instances in `Safe` code), so I don't know if that would even be an issue in practice.

Is there any benefit from adding this distinguishing information/kind information to the metadata (since `Proxy` is polykinded)?

I am perversely working backwards from the perspective of injectivity but there may be a use for `TypeRep`s in the `Rep`.

Well, I've never found myself wanting to put `TypeRep` in `Rep` precisely because `Typeable`'s a whole 'nother can of worms, and it does feel perverse to jam more stuff into an already cluttered `Rep`. Furthermore, I don't think this would solve the problem of making it injective, since `TypeRep` values represent monomorphic types.

Sure, it can be kept open for more injective type families in base.

Out of curiosity, are there any other type families in `base` besides `Not` that can be injective? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12057: TypeFamilyDependencies on Data.Type.Bool's `Not` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective, newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): 2268 Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * differential: D2268 => 2268 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I say "in principle" because although most `Generic` instances (and hence `Rep` instances) are derived, a devilish programmer //could// handwrite a `Rep` instance that violates injectivity. That could be checked if GHC ends up adding support for head-injectivity,

#12057: TypeFamilyDependencies on Data.Type.Bool's `Not` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.0.1 Resolution: | Keywords: TypeFamilies, | Injective, newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2268 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:7 RyanGlScott]: there may be use cases for an injective `Rep`.

Out of curiosity, are there any other type families in `base` besides `Not` that can be injective? I can sift through `base` and see if there are others, posting them here.

-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12057: TypeFamilyDependencies on Data.Type.Bool's `Not` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: closed Priority: normal | Milestone: 8.2.1 Component: libraries/base | Version: 8.0.1 Resolution: fixed | Keywords: TypeFamilies, | Injective, newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2268 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed * milestone: => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12057#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler