-\section{Normalisation of wanteds constraints}
-%* *
-%************************************************************************
-
-\begin{code}
-normaliseWanteds :: [Inst] -> TcM [Inst]
-normaliseWanteds insts
- = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
- ; result <- liftM fst $ rewriteToFixedPoint Nothing
- [ ("(Occurs)", noChange $ occursCheckInsts)
- , ("(ZONK)", dontRerun $ zonkInsts)
- , ("(TRIVIAL)", trivialInsts)
- -- no `swapInsts'; it messes up error messages and should
- -- not be necessary -=chak
- , ("(DECOMP)", decompInsts)
- , ("(TOP)", topInsts)
- , ("(SUBST)", substInsts)
- , ("(UNIFY)", unifyInsts)
- ] insts
- ; traceTc (text "normaliseWanteds ->" <+> ppr result)
- ; return result
- }
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{Normalisation of givens constraints}
-%* *
-%************************************************************************
-
-\begin{code}
-normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
-normaliseGivens givens
- = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
- ; (result, deSkolem) <-
- rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
- [ ("(Occurs)", noChange $ occursCheckInsts)
- , ("(ZONK)", dontRerun $ zonkInsts)
- , ("(TRIVIAL)", trivialInsts)
- , ("(SWAP)", swapInsts)
- , ("(DECOMP)", decompInsts)
- , ("(TOP)", topInsts)
- , ("(SUBST)", substInsts)
- ] givens
- ; traceTc (text "normaliseGivens ->" <+> ppr result)
- ; return (result, deSkolem)
- }
-
--- An explanation of what this does would be helpful! -=chak
-skolemOccurs :: PrecondRule
-skolemOccurs [] = return ([], return ())
-skolemOccurs (inst@(EqInst {}):insts)
- = do { (insts',actions) <- skolemOccurs insts
- -- check whether the current inst co :: ty1 ~ ty2 suffers
- -- from the occurs check issue: F ty1 \in ty2
- ; let occurs = go False ty2
- ; if occurs
- then
- -- if it does generate two new coercions:
- do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
- ; let skolem_ty = TyVarTy skolem_var
- -- ty1 :: ty1 ~ b
- ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
- -- sym co :: ty2 ~ b
- ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
- -- to replace the old one
- -- the corresponding action is
- -- b := ty1
- ; let action = writeMetaTyVar skolem_var ty1
- ; return (inst1:inst2:insts', action >> actions)
- }
- else
- return (inst:insts', actions)
- }
- where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
- co = eqInstCoercion inst
- check :: Bool -> TcType -> Bool
- check flag ty
- = if flag && ty1 `tcEqType` ty
- then True
- else go flag ty
-
- go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
- go flag (FunTy arg res) = or $ map (check flag) [arg,res]
- go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
- go _ _ = False
-skolemOccurs _ = panic "TcTyFuns.skolemOccurs: not EqInst"
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{Solving of wanted constraints with respect to a given set}
-%* *
-%************************************************************************
-
-\begin{code}
-solveWanteds :: [Inst] -- givens
- -> [Inst] -- wanteds
- -> TcM [Inst] -- irreducible wanteds
-solveWanteds givens wanteds
- = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
- ppr givens
- ; result <- liftM fst $ rewriteToFixedPoint Nothing
- [ ("(Occurs)", noChange $ occursCheckInsts)
- , ("(TRIVIAL)", trivialInsts)
- , ("(DECOMP)", decompInsts)
- , ("(TOP)", topInsts)
- , ("(GIVEN)", givenInsts givens)
- , ("(UNIFY)", unifyInsts)
- ] wanteds
- ; traceTc (text "solveWanteds ->" <+> ppr result)
- ; return result
- }
- where
- -- Use `substInst' with every given on all the wanteds.
- givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
- givenInsts [] wanteds = return (wanteds,False)
- givenInsts (g:gs) wanteds
- = do { (wanteds1, changed1) <- givenInsts gs wanteds
- ; (wanteds2, changed2) <- substInst g wanteds1
- ; return (wanteds2, changed1 || changed2)
- }
-\end{code}
-
-
-%************************************************************************
-%* *