+
+Decomposition of data type constructors: decompRule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whenever, the same *data* constructors occurs on both sides of an equality, we
+can decompose as in standard unification.
+
+ (Decomp)
+ g1 : T cs ~ T ds
+ >-->
+ g21 : c1 ~ d1, ..., g2n : cn ~ dn
+ g1 := T g2s
+
+Works also for the case where T is actually an application of a type family
+constructor to a set of types, provided the applications on both sides of the
+~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
+
+We guarantee to raise an error for any inconsistent equalities;
+cf Note [Inconsistencies in equality constraints].
+
+\begin{code}
+decompRule :: RewriteRule
+decompRule insts
+ = do { (insts, changed) <- mapAndUnzipM decomp insts
+ ; return (concat insts, or changed)
+ }
+ where
+ decomp inst
+ = ASSERT( isEqInst inst )
+ go (eqInstLeftTy inst) (eqInstRightTy inst)
+ where
+ go ty1 ty2
+ | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+ go (TyConApp con1 tys1) (TyConApp con2 tys2)
+ | con1 == con2 && identicalHead
+ = mkArgInsts (mkTyConApp con1) tys1 tys2
+
+ | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
+ -- not matching data constructors (of any flavour) are bad news
+ = eqInstMisMatch inst
+ where
+ n = tyConArity con1
+ (idxTys1, _) = splitAt n tys1
+ (idxTys2, _) = splitAt n tys2
+ identicalHead = not (isOpenSynTyCon con1) ||
+ idxTys1 `tcEqTypes` idxTys2
+
+ go (FunTy fun1 arg1) (FunTy fun2 arg2)
+ = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
+ [fun2, arg2]
+
+ -- Applications need a bit of care!
+ -- They can match FunTy and TyConApp, so use splitAppTy_maybe
+ go (AppTy s1 t1) ty2
+ | Just (s2, t2) <- tcSplitAppTy_maybe ty2
+ = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
+
+ -- Symmetric case
+ go ty1 (AppTy s2 t2)
+ | Just (s1, t1) <- tcSplitAppTy_maybe ty1
+ = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
+
+ -- We already covered all the consistent cases of rigid types on both
+ -- sides; so, if we see two rigid types here, we discovered an
+ -- inconsistency.
+ go ty1 ty2
+ | isRigid ty1 && isRigid ty2
+ = eqInstMisMatch inst
+
+ -- We can neither assert consistency nor inconsistency => defer
+ go _ _ = return ([inst], False)
+
+ isRigid (TyConApp con _) = not (isOpenSynTyCon con)
+ isRigid (FunTy _ _) = True
+ isRigid (AppTy _ _) = True
+ isRigid _ = False
+
+ -- Create insts for matching argument positions (ie, the bit after
+ -- '>-->' in the rule description above)
+ mkArgInsts con tys1 tys2
+ = do { cos <- eitherEqInst inst
+ -- old_co := Con1 cos
+ (\old_covar ->
+ do { cotvs <- zipWithM newMetaCoVar tys1 tys2
+ ; let cos = map mkTyVarTy cotvs
+ ; writeMetaTyVar old_covar (con cos)
+ ; return $ map mkWantedCo cotvs
+ })
+ -- co_i := Con_i old_co
+ (\old_co ->
+ return $ map mkGivenCo $
+ mkRightCoercions (length tys1) old_co)
+ ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
+ ; traceTc (text "decomp identicalHead" <+> ppr insts)
+ ; return (insts, not $ null insts)
+ }
+\end{code}
+
+
+Rewriting with type instances: topRule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use (toplevel) type instances to normalise both sides of equalities.
+
+ (Top)
+ g1 : t ~ s
+ >--> co1 :: t ~ t' / co2 :: s ~ s'
+ g2 : t' ~ s'
+ g1 := co1 * g2 * sym co2
+
+\begin{code}
+topRule :: RewriteRule
+topRule insts
+ = do { (insts, changed) <- mapAndUnzipM top insts
+ ; return (insts, or changed)
+ }
+ where
+ top inst
+ = ASSERT( isEqInst inst )
+ do { (coi1, ty1') <- tcNormaliseFamInst ty1
+ ; (coi2, ty2') <- tcNormaliseFamInst ty2
+ ; case (coi1, coi2) of
+ (IdCo, IdCo) -> return (inst, False)
+ _ ->
+ do { wg_co <-
+ eitherEqInst inst
+ -- old_co = co1 * new_co * sym co2
+ (\old_covar ->
+ do { new_cotv <- newMetaCoVar ty1' ty2'
+ ; let new_co = mkTyVarTy new_cotv
+ old_coi = coi1 `mkTransCoI`
+ ACo new_co `mkTransCoI`
+ (mkSymCoI coi2)
+ ; writeMetaTyVar old_covar (fromACo old_coi)
+ ; return $ mkWantedCo new_cotv
+ })
+ -- new_co = sym co1 * old_co * co2
+ (\old_co ->
+ return $
+ mkGivenCo $
+ fromACo $
+ mkSymCoI coi1 `mkTransCoI`
+ ACo old_co `mkTransCoI` coi2)
+ ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
+ ; return (new_inst, True)
+ }