Mark result kind variable as injective

[jstolarek]

If I say

type family F (a :: k1) = (r :: k2) | r -> a

then a and k1 are marked as injective. But k2 is also the input parameter to F and so it seems to make sense to mark it as injective as well. Thus my idea is to mark the result kind variable as injective when the user provides injectivity annotation for a type family with polymorphic return kind. Not sure what to do if there is no injectivity annotation but the result is polymorphic. Normally in this situation the corresponding field in FamilyTyCon is Nothing. In theory if there is a return kind marking it as injective should be always possible (?). Then again I'm not sure if there is any benefit other than consistency.

[jstolarek]

Doing this seems very tricky. The right place for this is getInjectivityList. The problem is that the input data to that function provides: a) a list of type variables that the type family takes as arguments (tyConTyVars); b) name of the result variable. The difficulty is that there is no information whether the list of type variables contains the result kind variable. So the callers of getInjectivityList would have to pass in some extra argument that says whether the type family has polymorphic return kind (there are only two callers, so the extra argument by itself is not an issue). That extra argument could be FamilyResultSig because it is available to the callers. If it contained result kind variable then we could replace the first argument in the injectivity list with True. This rests on the assumption that the return kind is always first. That solution is ugly because if the invariant changes the code would break. Probably this should be done differently but I suspect that solution might be more complicated than it's worth it. Closing as wontfix.

[jstolarek]

There's another reason for not doing this. If somehow we come up with an example where this dependency is important it should probably be made explicit by listing the kind variable in the injectivity list.