- applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
-
- -- rewrite in case of an exact match
- matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
- | otherwise = Nothing
-
- -- (2) Given equality has the wrong form: ignore
- rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
- = return (dictInsts, dictBinds)
-\end{code}
-
-
-Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
-type-function equations, where
-
- (norm_insts, binds) = normaliseInsts is_wanted insts
+ isFree (tv, _) = tv `elemVarSet` freeFlexibles
+
+ -- co :: alpha ~ t or co :: a ~ alpha
+ instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+ = do { flexi_tv1 <- isFlexible tv1
+ ; maybe_flexi_tv2 <- isFlexibleTy ty2
+ ; case (flexi_tv1, maybe_flexi_tv2) of
+ (True, Just tv2)
+ | isSigTyVar tv1 && isSigTyVar tv2
+ -> -- co :: alpha ~ beta, where both a SigTvs
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (True, Nothing)
+ | Just tv2 <- tcGetTyVar_maybe ty2
+ , isSigTyVar tv1
+ , isSkolemTyVar tv2
+ -> -- co :: alpha ~ a, where alpha is a SigTv
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (True, _)
+ | not (isSigTyVar tv1)
+ -> -- co :: alpha ~ t, where alpha is not a SigTv
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (False, Just tv2)
+ | isSigTyVar tv2
+ , isSkolemTyVar tv1
+ -> -- co :: a ~ alpha, where alpha is a SigTv
+ doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+ | not (isSigTyVar tv2)
+ -> -- co :: a ~ alpha, where alpha is not a SigTv
+ -- ('a' may be filled)
+ doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+ _ -> return $ Just eq
+ }
+ instVarEq eq = return $ Just eq
+
+ -- co :: F args ~ alpha,
+ -- and we are either in checking mode or alpha is a skolem flexible that
+ -- doesn't escape
+ instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
+ rwi_right = ty2, rwi_co = co})
+ | Just tv2 <- tcGetTyVar_maybe ty2
+ , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
+ = do { flexi_tv2 <- isFlexible tv2
+ ; if flexi_tv2
+ then
+ doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
+ else
+ return $ Just eq
+ }
+ instFamEq _ eq = return $ Just eq
+
+ -- tv is a meta var, but not a SigTV and not filled
+ isFlexible tv
+ | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
+ | otherwise = return False
+
+ -- type is a tv that is a meta var, but not a SigTV and not filled
+ isFlexibleTy ty
+ | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
+ ; if flexi then return $ Just tv
+ else return Nothing
+ }
+ | otherwise = return Nothing
+
+ doInst _swapped _tv _ty (Right ty) _eq
+ = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
+ doInst swapped tv ty (Left cotv) eq
+ = do { lookupTV <- lookupTcTyVar tv
+ ; bMeta swapped tv lookupTV ty cotv
+ }
+ where
+ -- Try to create a binding for a meta variable. There is *no* need to
+ -- consider reorienting the underlying equality; `checkOrientation'
+ -- makes sure that we get variable-variable equalities only in the
+ -- appropriate orientation.
+ --
+ bMeta :: Bool -- is this a swapped equality?
+ -> TcTyVar -- tyvar to instantiate
+ -> LookupTyVarResult -- lookup result of that tyvar
+ -> TcType -- to to instantiate tyvar with
+ -> TcTyVar -- coercion tyvar of current equality
+ -> TcM (Maybe RewriteInst) -- returns the original equality if
+ -- the tyvar could not be instantiated,
+ -- and hence, the equality must be kept