#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Good question. I have not considered such case earlier. Here are some thoughts: Currently your `Map` function will work only for type constructors because unsaturated type families are not allowed. These are certainly injective. First step in my current outline of the algorithm that decides whether a type family is injective or not says: "If a RHS contains a call to a type family we conclude that the type family is not injective. I am not certain if this extends to self-recursion -- see discussion below." This would lead to conclusion that `Map` is not injective because `Map` calls itself. Now let's say I manage to find a way to allow self-recursion (see discussion on the wiki page). I'm left with the problematic call to `f`. As stated earlier currently this must be an injective type constructor. So it seems that declaring `Map` injective should be safe because type constructors are generative and it seems possible to deduce `f`, `a` and `b` from `Map f [a, b] ~ [Maybe Int, Maybe Char]`. At the moment I have no idea how to formulate an algorithm for such a deduction. Could this be done by the current constraint solver? What if we were allowed to have partially applied type families (say, because we've implemented ideas from singletons) and `f` could be a type family? Would knowing that `f` is injective allow us to declare `Map` as injective? Injectivity says you can deduce LHS from RHS but I think that it would not be a good idea to try to solve `Map f [a, b] ~ [Int, Char]`. And so the restriction on not having calls to type families on the RHS would rightly declare `Map` as not injective. So if we had partially applied type families and thus `f` was allowed to be either a type constructor a type family we should declare `Map` as not injective. This contrasts with earlier paragraph, where knowing that `f` must be a type constructor allowed us to declare `Map` as injective. Does that make sense? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:75 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler