Good question. I have not considered such case earlier. Here are some

#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 goldfire): Replying to [comment:75 jstolarek]: 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? This should just work with the algorithm already stated. (Except for the self-recursion bit, which I responded to on the wiki page.) Unification should do the work for you.

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?

No. Under the singletons work, we gave a different kind to non-injective functions, so Gabor's kind -- using `->`, not any other arrow -- requires an injective argument. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:80 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler