Use injective type families (decomposition) when dealing with givens

Consider this code:

type family Id a = r | r -> a

id :: (Id a ~ Id b) => a -> b
id x = x

GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints.

And yet Coercion has a form for representing such coercions, namely "nth" (written SelCo in GHC). We could say

    co : F s1..sn ~ F t1..tn
    F is injective in its i'th argument
   -----------------------------------
   SelCo (Tc i) co : si ~ ti

Indeed Lint already accepts such SelCos:

lintCoercion the_co@(SelCo cs co)
  = do { co' <- lintCoercion co
       ; let (Pair s t, co_role) = coercionKindRole co'

       ; if -- forall (both TyVar and CoVar)
            ...

            -- TyCon
            | Just (tc_s, tys_s) <- splitTyConApp_maybe s
            , Just (tc_t, tys_t) <- splitTyConApp_maybe t
            , tc_s == tc_t
            , SelTyCon n r0 <- cs
            , isInjectiveTyCon tc_s co_role
                -- see Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
            , tys_s `equalLength` tys_t
            , tys_s `lengthExceeds` n
            -> do { lintRole the_co (tyConRole co_role tc_s n) r0
                  ; return (SelCo cs co') }

Note that isInjectiveTyCon! An injective type family is accepted here. (But only if it is injective in all arguments, which is stronger than we need.)

Allowing this would be user facing change, hence needing a GHC proposal. But it'd be very simple to implement.

@rae any views on how this might impact soundness?

Trac metadata

Trac field	Value
Version	7.10.2
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#6018 (closed)
Blocking
CC
Operating system
Architecture