#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.4.1 Resolution: | Keywords: Operating System: Unknown/Multiple | TypeFamilies, Injective Type of failure: None/Unknown | Architecture: Blocked By: | Unknown/Multiple Related Tickets: #4259 | Test Case: | Blocking: | Differential Revisions: Phab:D202 -------------------------------------+------------------------------------- Comment (by dfeuer): I don't see the problem with letting injective families call other type families as long as there is no recursion—can't GHC follow all paths to the end when necessary, and use injectivity "lemmas" when possible for efficiency? Or does this end up not being useful/efficient/possible for some reason? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:106 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler