#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): comment:13 is asking for injectivity from result with ''either'' argument to the other. Notice the O.P. for `AddTF` only considers result & first argument `->` second arg. I see a problem. In instances {{{ type family xs :++: ys = r | r xs -> ys, r ys -> xs where -- both injectivities '[] :++: ys = ys (x ': xs) :++: ys = x ': (xs :++: ys) }}} Under the injection `r ys -> xs`, I think GHC will not be able to see the 'apartness' in the two equations. That is, it won't be able to disprove `ys ~ (x ': (xs :++: ys))`. Yes we know they can't unify, but GHC sees `:++:` as a Type Function, not a (proto-)constructor. Speculative remedy [https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness-guards.rst#injective- type-families proposed here], for the `AddTF` example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler