#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