- -- look through synonyms
- go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
- go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
-
- -- rewrite type family applications
- go ty1@(TyConApp con _) ty2 co
- | isOpenSynTyCon con
- = substEquality (ty1, ty2, co) insts
-
- -- rewrite skolems
- go ty1@(TyVarTy tv) ty2 co
- | isSkolemTyVar tv
- = substEquality (ty1, ty2, co) insts
-
- -- rewrite type family applications from right-to-left, only after
- -- having checked whether we can work left-to-right
- go ty1 ty2@(TyConApp con _) co
- | isOpenSynTyCon con
- = substEquality (ty2, ty1, mkSymCoercion co) insts
-
- -- rewrite skolems from right-to-left, only after having checked
- -- whether we can work left-to-right
- go ty1 ty2@(TyVarTy tv) co
- | isSkolemTyVar tv
- = substEquality (ty2, ty1, mkSymCoercion co) insts
-
- go _ _ _ = return (insts, False)
-
- substEquality :: (TcType, -- rewrite rule lhs
- TcType, -- rewrite rule rhs
- TcType) -- coercion witnessing the rewrite rule
- -> [Inst] -- insts to rewrite