I'm ambivalent on this design decision (that the variables have to be in

#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): Replying to [comment:79 goldfire]: the same order in the annotation). I suppose it simplifies the implementation. I guess my argument about simpler implementation is not that important. I mean the code is quite simple in both cases. It's more like a choice between linear and quadratic algorithm. I'd went for linear, even if it adds an extra restriction on the user code.

Yes, Simon's comment above is correct -- I was just wrong about the `isDecomposableTyCon` thing.

What works perfectly fine? Not the code you wrote above, because it contains a not-currently-parsed injectivity annotation. I tried it without

OK. Reverting :-) the injectivity annotation, and it does indeed work. Yes, that's what I meant.

But not because of injectivity, at all: it's because GHC is clever enough to figure out that `F` is just an identity function

Right. Still, I wondering how this works. I mean there are probably no special cases in the typechecker that try to guess whether a type family is an identity function?

Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :)

I imagine, given that my source file was 8 lines of code. Still, it's a bit steep learning curve. Replying to [comment:80 goldfire]:

Under the singletons work, we gave a different kind to non-injective functions

I believe this would also have to check that all variables mentioned in

Ah, right. Replying to [wiki:InjectiveTypeFamilies wiki comments]: the LHS are mentioned in the RHS. Or, following along with Simon's idea in comment:76:ticket:6018, those variables that appear in the injectivity annotation must be mentioned in the RHS. I haven't thought about that. I believe you're right.

We have to be careful with the word overlap here. I think we want "overlaps" to be "is subsumed by".

if unification [of the RHSs] succeeds and there are type variables involved we substitute unified type variables on the LHS and check whether

I don't see the difference between "overlaps" and "is subsumed by". :-( Now, in 4c I wrote: this LHS overlaps with any of the previous equations. If it does we proceed to the next equation You replied with this:

you want to know of the equation at hand is reachable, given the LHS substitution. Even if it is reachable, the (substituted) LHS may coincide with the LHS of the earlier equation whose RHS unified with the current RHS.

I don't see the difference between your version and mine.

Even subtler, it's possible that certain values for type variables are excluded if the current LHS is reachable (for example, some variable a couldn't be Int, because if a were Int, then a previous equation would have triggered). Perhaps these exclusions can also be taken into account.

'''RAE:''' But it seems that, under this treatment, any self-recursion would automatically lead to a conclusion of "not injective", just like any other use of a type family. For example:

{{{#!hs type family IdNat n where IdNat Z = Z IdNat (S n) = S (IdNat n) }}}

`IdNat` is injective. But, following the algorithm above, GHC would see

Hm... can you give an example where this would be useful? the recursive use of `IdNat`, not know whether `IdNat` is injective, and then give up, concluding "not injective". Is there a case where the special treatment of self-recursion leads to a conclusion of "injective"? '''End RAE''' This example is just like my `NatToMaybe`. My idea here was that RHSs of these two equations won't unify - first returns `Z`, second returns `S something`. These are distinct constructors that have no chance of being unified. (I assumed that we are able to detect that.) There are no calls to type families other than self-recursion and so we can declare `IdNat` to be injective. I admit I am not 100% certain that allowing self- recursion is safe. It's just that I was unable to come up with an example that would show that my algorithm: a:) declares injective function to be non-injective; b) declares a non-injective function to be injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:82 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler