-
-tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
-tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
-\end{code}
-
-An elementary rewrite is a properly oriented equality with associated coercion
-that has one of the following two forms:
-
-(1) co :: F t1..tn ~ t
-(2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
-
-NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
-reqrite rule. Instead, such equalities are solved by unification. This is
-essential; cf Note [skolemOccurs loop].
-
-The following functions takes an equality instance and turns it into an
-elementary rewrite if possible.
-
-\begin{code}
-data Rewrite = Rewrite TcType -- lhs of rewrite rule
- TcType -- rhs of rewrite rule
- TcType -- coercion witnessing the rewrite rule
-
-eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
- -- True iff rewrite swapped equality
-eqInstToRewrite inst
- = ASSERT( isEqInst inst )
- go ty1 ty2 (eqInstType inst)
- where
- (ty1,ty2) = eqInstTys inst
-
- -- 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
-
- -- left-to-right rule with type family head
- go ty1@(TyConApp con _) ty2 co
- | isOpenSynTyCon con
- = Just (Rewrite ty1 ty2 co, False) -- not swapped
-
- -- left-to-right rule with type variable head
- go ty1@(TyVarTy tv) ty2 co
- | isSkolemTyVar tv
- = Just (Rewrite ty1 ty2 co, False) -- not swapped
-
- -- right-to-left rule with type family head, only after
- -- having checked whether we can work left-to-right
- go ty1 ty2@(TyConApp con _) co
- | isOpenSynTyCon con
- = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
-
- -- right-to-left rule with type variable head, only after
- -- having checked whether we can work left-to-right
- go ty1 ty2@(TyVarTy tv) co
- | isSkolemTyVar tv
- = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
-
- -- this equality is not a rewrite rule => ignore
- go _ _ _ = Nothing
-\end{code}
-
-Normalise a type relative to an elementary rewrite implied by an EqInst or an
-explicitly given elementary rewrite.
-
-\begin{code}
--- Rewrite by EqInst
--- Precondition: the EqInst passes the occurs check
-tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
-tcEqInstNormaliseFamInst inst ty
- = case eqInstToRewrite inst of
- Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
- Nothing -> return (IdCo, ty)
-
--- Rewrite by equality rewrite rule
-tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
- -> TcType -- type to rewrite
- -> TcM (CoercionI, -- witnessing coercion
- TcType) -- rewritten type
-tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
- = tcGenericNormaliseFamInst matchEqRule ty
- where
- matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
- | otherwise = return $ Nothing