#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies 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 carter): I've hit needing this feature for what I was hoping would be pretty elementary code :( {{{ type family ReverseTC (a :: [ k ]) (res :: [ k ] ) = result where ReverseTC '[] res = res ReverseTC (a ': bs ) res = ReverseTC bs (a ': res) type family Reverse (a :: [k]) = (result :: [k]) where Reverse a = ReverseTC a '[] }}} I would like to explain to GHC that if i know a and result , or res and result, i know the remaining variable, so that my "stack safe" Reverse computation can also be treated as Injective (which it is! ) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler