+ -- We have, co ::^w F t1..tn ~ tv
+ -- => apply [F t1..tn/tv] to eq2
+ -- (but only if tv actually occurs in eq2
+ -- and eq2 is a wanted equality
+ -- and we are either in checking mode or eq2 is a family equality)
+ substEq (RewriteFam {rwi_args = args, rwi_right = ty})
+ coSubst tySubst eq2
+ | Just tv <- tcGetTyVar_maybe ty
+ , tv `elemVarSet` tyVarsOfRewriteInst eq2
+ , isWantedRewriteInst eq2
+ , checkingMode || not (isRewriteVar eq2)
+ = do { -- substitute into the right-hand side
+ ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
+ right2' = substTy tySubst (rwi_right eq2)
+ left2 = case eq2 of
+ RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
+ RewriteFam {rwi_fam = fam,
+ rwi_args = args} -> mkTyConApp fam args
+ ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
+ ; case eq2 of
+ RewriteVar {rwi_var = tv2}
+ -- variable equality: perform an occurs check
+ | tv2 `elemVarSet` tyVarsOfTypes args
+ -> occurCheckErr left2 right2'
+ | otherwise
+ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
+ RewriteFam {rwi_fam = fam}
+ -- family equality: substitute also into the left-hand side
+ -> do { let co1Subst = substTy coSubst left2
+ args2' = substTys tySubst (rwi_args eq2)
+ left2' = mkTyConApp fam args2'
+ ; co2'' <- mkRightTransEqInstCo co2' co1Subst
+ (left2', right2')
+ ; return $ eq2 {rwi_args = args2', rwi_right = right2',
+ rwi_co = co2''}
+ }
+ }
+