#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | 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 jstolarek):
I think the right solution here would be to drop equation (7) from our algorithm in the paper.
On a second thought I don't think this would be good idea. Doing this would mean that using any type family in the RHS is prohibited for injective type families and we definitely don't want that for generalized injectivity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler