-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/CodingStyle#Warnings
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
-- for details
module TcTyFuns(
- finalizeEqInst,
- partitionWantedEqInsts, partitionGivenEqInsts,
-
tcNormalizeFamInst,
normaliseGivens, normaliseGivenDicts,
import Maybes
import Data.List
-\end{code}
-
-%************************************************************************
-%* *
-\section{Eq Insts}
-%* *
-%************************************************************************
-
-%************************************************************************
-%* *
-\section{Utility Code}
-%* *
-%************************************************************************
-
-\begin{code}
-partitionWantedEqInsts
- :: [Inst] -- wanted insts
- -> ([Inst],[Inst]) -- (wanted equations,wanted dicts)
-partitionWantedEqInsts = partitionEqInsts True
-
-partitionGivenEqInsts
- :: [Inst] -- given insts
- -> ([Inst],[Inst]) -- (given equations,given dicts)
-partitionGivenEqInsts = partitionEqInsts False
-
-
-partitionEqInsts
- :: Bool -- <=> wanted
- -> [Inst] -- insts
- -> ([Inst],[Inst]) -- (equations,dicts)
-partitionEqInsts wanted []
- = ([],[])
-partitionEqInsts wanted (i:is)
- | isEqInst i
- = (i:es,ds)
- | otherwise
- = (es,i:ds)
- where (es,ds) = partitionEqInsts wanted is
-
-isEqDict :: Inst -> Bool
-isEqDict (Dict {tci_pred = EqPred _ _}) = True
-isEqDict _ = False
-
+import Control.Monad (liftM)
\end{code}
%************************************************************************
%* *
-\section{Normalisation of Wanteds}
+\section{Normalisation of wanteds constraints}
%* *
%************************************************************************
\begin{code}
normaliseWanteds :: [Inst] -> TcM [Inst]
normaliseWanteds insts
- = do { traceTc (text "normaliseWanteds" <+> ppr insts)
- ; result <- eq_rewrite
- [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
- , ("(ZONK)", simple_rewrite $ zonkInsts)
+ = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
+ ; result <- liftM fst $ rewriteToFixedPoint Nothing
+ [ ("(Occurs)", noChange $ occursCheckInsts)
+ , ("(ZONK)", dontRerun $ zonkInsts)
, ("(TRIVIAL)", trivialInsts)
- , ("(SWAP)", swapInsts)
+ -- no `swapInsts'; it messes up error messages and should
+ -- not be necessary -=chak
, ("(DECOMP)", decompInsts)
, ("(TOP)", topInsts)
, ("(SUBST)", substInsts)
}
\end{code}
+
%************************************************************************
%* *
-\section{Normalisation of Givens}
+\section{Normalisation of givens constraints}
%* *
%************************************************************************
\begin{code}
-
-normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
-normaliseGivens givens =
- do { traceTc (text "normaliseGivens <-" <+> ppr givens)
- ; (result,action) <- given_eq_rewrite
- ("(SkolemOccurs)", skolemOccurs)
- (return ())
- [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
- ("(ZONK)", simple_rewrite $ zonkInsts),
- ("(TRIVIAL)", trivialInsts),
- ("(SWAP)", swapInsts),
- ("(DECOMP)", decompInsts),
- ("(TOP)", topInsts),
- ("(SUBST)", substInsts)]
- givens
- ; traceTc (text "normaliseGivens ->" <+> ppr result)
- ; return (result,action)
- }
-
-skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
-skolemOccurs [] = return ([], return ())
+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
go flag ty = False
\end{code}
+
%************************************************************************
%* *
-\section{Solving of Wanteds}
+\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 <- eq_rewrite
- [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
- ("(TRIVIAL)", trivialInsts),
- ("(DECOMP)", decompInsts),
- ("(TOP)", topInsts),
- ("(GIVEN)", givenInsts givens),
- ("(UNIFY)", unifyInsts)]
- wanteds
- ; traceTc (text "solveWanteds ->" <+> ppr result)
- ; return result
+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}
-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)
- }
+%************************************************************************
+%* *
+\section{Normalisation rules and iterative rule application}
+%* *
+%************************************************************************
+We have four kinds of normalising rewrite rules:
+(1) Normalisation rules that rewrite a set of insts and return a flag indicating
+ whether any changes occurred during rewriting that necessitate re-running
+ the current rule set.
- -- fixpoint computation
- -- of a number of rewrites of equalities
-eq_rewrite ::
- [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
- [Inst] -> -- initial equations
- TcM [Inst] -- final equations (at fixed point)
-eq_rewrite rewrites insts
- = go rewrites insts
- where
- go _ [] -- return quickly when there's nothing to be done
- = return []
- go [] insts
- = return insts
- go ((desc,r):rs) insts
- = do { (insts',changed) <- r insts
- ; traceTc (text desc <+> ppr insts')
- ; if changed
- then loop insts'
- else go rs insts'
- }
- loop = eq_rewrite rewrites
-
- -- fixpoint computation
- -- of a number of rewrites of equalities
-given_eq_rewrite ::
-
- (String,[Inst] -> TcM ([Inst],TcM ())) ->
- (TcM ()) ->
- [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
- [Inst] -> -- initial equations
- TcM ([Inst],TcM ()) -- final equations (at fixed point)
-given_eq_rewrite p@(desc,start) acc rewrites insts
- = do { (insts',acc') <- start insts
- ; go (acc >> acc') rewrites insts'
- }
- where
- go acc _ [] -- return quickly when there's nothing to be done
- = return ([],acc)
- go acc [] insts
- = return (insts,acc)
- go acc ((desc,r):rs) insts
- = do { (insts',changed) <- r insts
- ; traceTc (text desc <+> ppr insts')
- ; if changed
- then loop acc insts'
- else go acc rs insts'
- }
- loop acc = given_eq_rewrite p acc rewrites
-
-simple_rewrite ::
- ([Inst] -> TcM [Inst]) ->
- ([Inst] -> TcM ([Inst],Bool))
-simple_rewrite r insts
- = do { insts' <- r insts
- ; return (insts',False)
- }
+(2) Precondition rules that rewrite a set of insts and return a monadic action
+ that reverts the effect of preconditioning.
+
+(3) Idempotent normalisation rules that never require re-running the rule set.
-simple_rewrite_check ::
- ([Inst] -> TcM ()) ->
- ([Inst] -> TcM ([Inst],Bool))
-simple_rewrite_check check insts
- = check insts >> return (insts,False)
-
+(4) Checking rule that does not alter the set of insts.
+\begin{code}
+type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
+type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
+type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
+type CheckRule = [Inst] -> TcM () -- check
+
+type NamedRule = (String, RewriteRule) -- rule with description
+type NamedPreRule = (String, PrecondRule) -- precond with desc
\end{code}
+Templates lifting idempotent and checking rules to full rules (which can be put
+into a rule set).
+
+\begin{code}
+dontRerun :: IdemRewriteRule -> RewriteRule
+dontRerun rule insts = liftM addFalse $ rule insts
+ where
+ addFalse x = (x, False)
+
+noChange :: CheckRule -> RewriteRule
+noChange rule insts = rule insts >> return (insts, False)
+\end{code}
+
+The following function applies a set of rewrite rules until a fixed point is
+reached; i.e., none of the `RewriteRule's require re-running the rule set.
+Optionally, there may be a pre-conditing rule that is applied before any other
+rules are applied and before the rule set is re-run.
+
+The result is the set of rewritten (i.e., normalised) insts and, in case of a
+pre-conditing rule, a monadic action that reverts the effects of
+pre-conditioning - specifically, this is removing introduced skolems.
+
+\begin{code}
+rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
+ -> [NamedRule] -- rule set
+ -> [Inst] -- insts to rewrite
+ -> TcM ([Inst], TcM ())
+rewriteToFixedPoint precondRule rules insts
+ = completeRewrite (return ()) precondRule insts
+ where
+ completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
+ -> TcM ([Inst], TcM ())
+ completeRewrite dePrecond (Just (precondName, precond)) insts
+ = do { (insts', dePrecond') <- precond insts
+ ; traceTc $ text precondName <+> ppr insts'
+ ; tryRules dePrecond rules insts'
+ }
+ completeRewrite dePrecond Nothing insts
+ = tryRules dePrecond rules insts
+
+ tryRules dePrecond _ [] = return ([] , dePrecond)
+ tryRules dePrecond [] insts = return (insts, dePrecond)
+ tryRules dePrecond ((name, rule):rules) insts
+ = do { (insts', rerun) <- rule insts
+ ; traceTc $ text name <+> ppr insts'
+ ; if rerun then completeRewrite dePrecond precondRule insts'
+ else tryRules dePrecond rules insts'
+ }
+\end{code}
+
+
%************************************************************************
%* *
\section{Different forms of Inst rewritings}
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
swapInsts :: [Inst] -> TcM ([Inst],Bool)
-- All the inputs and outputs are equalities
-swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds)
-
+swapInsts insts
+ = do { (insts', changeds) <- mapAndUnzipM swapInst insts
+ ; return (insts', or changeds)
+ }
-- (Swap)
-- g1 : c ~ Fd
-- g2 : Fd ~ c
-- g1 := sym g2
--
+ -- This is not all, is it? Td ~ c is also rewritten to c ~ Td!
swapInst i@(EqInst {})
= go ty1 ty2
where
-- we should swap!
go ty1 ty2@(TyConApp tyCon _)
| isOpenSynTyCon tyCon
- = do { wg_co <- eitherEqInst i
+ = actual_swap ty1 ty2
+ go ty1@(TyConApp _ _) ty2@(TyVarTy _)
+ = actual_swap ty1 ty2
+ go _ _ = return (i,False)
+
+ actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
-- old_co := sym new_co
(\old_covar ->
do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
; return (new_inst,True)
}
- go _ _ = return (i,False)
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
decompInsts :: [Inst] -> TcM ([Inst],Bool)
do { cotvs <- zipWithM (\t1 t2 ->
newMetaTyVar TauTv
(mkCoKind t1 t2))
- tys1' tys2'
+ tys1 tys2
; let cos = map TyVarTy cotvs
; writeMetaTyVar old_covar (TyConApp con1 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
- ; return (insts, not $ null insts)
+ mkRightCoercions (length tys1) old_co)
+ ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
+ ; traceTc (text "decomp identicalHead" <+> ppr insts)
+ ; return (insts, not $ null insts)
}
| con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
-- not matching data constructors (of any flavour) are bad news
= do { env0 <- tcInitTidyEnv
- ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
- (env2, tidy_ty2) = tidyOpenType env1 ty2
- extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
- msg = ptext SLIT("Couldn't match expected type against inferred type")
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
+ (env2, tidy_ty2) = tidyOpenType env1 ty2
+ extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
+ msg =
+ ptext SLIT("Unsolvable equality constraint:")
; failWithTcM (env2, hang msg 2 extra)
}
where
projects / ghc-hetmet.git / blobdiff