\begin{code}
-{-# OPTIONS -w #-}
--- 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/Commentary/CodingStyle#Warnings
--- for details
-
-module TcTyFuns(
+module TcTyFuns (
tcNormalizeFamInst,
normaliseGivens, normaliseGivenDicts,
import TcRnMonad
import TcEnv
import Inst
-import FamInstEnv
import TcType
import TcMType
import Coercion
import TypeRep ( Type(..) )
import TyCon
-import Var ( mkCoVar, isTcTyVar )
+import Var ( isTcTyVar )
import Type
-import HscTypes ( ExternalPackageState(..) )
import Bag
import Outputable
import SrcLoc ( Located(..) )
import Maybes
import Data.List
+import Control.Monad (liftM)
\end{code}
| not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
= return Nothing
| otherwise
- = do { maybeFamInst <- tcLookupFamInst tycon tys
+ = do { -- we only use the indexing arguments for matching,
+ -- not the additional ones
+ ; maybeFamInst <- tcLookupFamInst tycon idxTys
; case maybeFamInst of
Nothing -> return Nothing
- Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
- mkTyConApp coe_tc rep_tys)
+ Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
+ mkTyConApp coe_tc tys')
where
+ tys' = rep_tys ++ restTys
coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
(tyConFamilyCoercion_maybe rep_tc)
}
+ where
+ n = tyConArity tycon
+ (idxTys, restTys) = splitAt n tys
tcUnfoldSynFamInst _other = return Nothing
\end{code}
-> TcM (CoercionI, Type) -- (coercion, new type)
tcGenericNormalizeFamInst fun ty
| Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
-tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
+tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
= do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
; let tycon_coi = mkTyConAppCoI tyCon ntys cois
; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
-- we do not do anything
Nothing -> return (tycon_coi, TyConApp tyCon ntys)
}
-tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
+tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
+tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
+tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
}
-tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
+tcGenericNormalizeFamInst fun (NoteTy note ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkNoteTyCoI note coi,NoteTy note nty1)
}
%************************************************************************
%* *
-\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 (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 flag ty = False
+ go _ _ = False
+skolemOccurs _ = panic "TcTyFuns.skolemOccurs: not EqInst"
\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.
-simple_rewrite_check ::
- ([Inst] -> TcM ()) ->
- ([Inst] -> TcM ([Inst],Bool))
-simple_rewrite_check check insts
- = check insts >> return (insts,False)
-
+(3) Idempotent normalisation rules that never require re-running the rule set.
+(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 >> 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}
-- >-->
-- g1 := t
--
-trivialInsts ::
- [Inst] -> -- equations
- TcM ([Inst],Bool) -- remaining equations, any changes?
+trivialInsts :: RewriteRule
trivialInsts []
= return ([],False)
trivialInsts (i@(EqInst {}):is)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-swapInsts :: [Inst] -> TcM ([Inst],Bool)
+swapInsts :: RewriteRule
-- All the inputs and outputs are equalities
swapInsts insts
= do { (insts', changeds) <- mapAndUnzipM swapInst insts
-- g2 : Fd ~ c
-- g1 := sym g2
--
+ -- This is not all, is it? Td ~ c is also rewritten to c ~ Td!
+swapInst :: Inst -> TcM (Inst, Bool)
swapInst i@(EqInst {})
= go ty1 ty2
where
; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
; return (new_inst,True)
}
+swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-decompInsts :: [Inst] -> TcM ([Inst],Bool)
+decompInsts :: RewriteRule
decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
; return (concat insts,or bs)
}
; failWithTcM (env2, hang msg 2 extra)
}
where
- n = tyConArity con1
- (idxTys1, tys1') = splitAt n tys1
- (idxTys2, tys2') = splitAt n tys2
- identicalHead = not (isOpenSynTyCon con1) ||
- idxTys1 `tcEqTypes` idxTys2
+ n = tyConArity con1
+ (idxTys1, _) = splitAt n tys1
+ (idxTys2, _) = splitAt n tys2
+ identicalHead = not (isOpenSynTyCon con1) ||
+ idxTys1 `tcEqTypes` idxTys2
go _ _ = return ([i], False)
+decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-topInsts :: [Inst] -> TcM ([Inst],Bool)
+topInsts :: RewriteRule
topInsts insts
= do { (insts,bs) <- mapAndUnzipM topInst insts
; return (insts,or bs)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+topInst _ = panic "TcTyFuns.topInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-substInsts :: [Inst] -> TcM ([Inst],Bool)
+substInsts :: RewriteRule
substInsts insts = substInstsWorker insts []
+substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
substInstsWorker [] acc
= return (acc,False)
substInstsWorker (i:is) acc
-- >-->
-- g2 : s1{t} ~ s2{t}
-- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
-substInst inst []
+substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
+substInst _inst []
= return ([],False)
substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
= do { (is',changed) <- substInst inst is
where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
coercion = eitherEqInst inst TyVarTy id
+substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
+
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-unifyInsts
- :: [Inst] -- wanted equations
- -> TcM ([Inst],Bool)
+unifyInsts :: RewriteRule
unifyInsts insts
= do { (insts',changeds) <- mapAndUnzipM unifyInst insts
; return (concat insts',or changeds)
-- g := t
--
-- TOMDO: you should only do this for certain `meta' type variables
+unifyInst :: Inst -> TcM ([Inst], Bool)
unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
| TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
| TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
; writeMetaTyVar cotv ty -- g := t
; return ([],True)
}
+unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-occursCheckInsts :: [Inst] -> TcM ()
+occursCheckInsts :: CheckRule
occursCheckInsts insts = mappM_ occursCheckInst insts
-- fail
--
occursCheckInst :: Inst -> TcM ()
-occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
+occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
= go ty2
where
check ty = if ty `tcEqType` ty1
; failWithTcM (env2, hang msg 2 extra)
}
where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
+occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
\end{code}
Normalises a set of dictionaries relative to a set of given equalities (which
}
where
normaliseOneInst isWanted fun
- dict@(Dict {tci_name = name,
- tci_pred = pred,
+ dict@(Dict {tci_pred = pred,
tci_loc = loc})
= do { traceTc (text "genericNormaliseInst 1")
; (coi, pred') <- fun pred
}
-- TOMDO: treat other insts appropriately
- normaliseOneInst isWanted fun inst
+ normaliseOneInst _isWanted _fun inst
= do { inst' <- zonkInst inst
; return (inst', emptyBag)
}
+addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
addBind binds inst rhs = binds `unionBags` mkBind inst rhs
+mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
mkBind inst rhs = unitBag (L (instSpan inst)
(VarBind (instToId inst) rhs))
\end{code}
projects / ghc-hetmet.git / blobdiff