X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=e5a562cfba0f3f43d9a936dc30f2420283ce72cc;hb=5f0eea10d6a29f3b2a3faf112279a3c98679c9f8;hp=141afb1a87a15a2cca0c6f5585b9c3c8f9148eb2;hpb=ad94d40948668032189ad22a0ad741ac1f645f50;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 141afb1..e5a562c 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -1,16 +1,6 @@ \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/CodingStyle#Warnings --- for details - -module TcTyFuns( - finalizeEqInst, - partitionWantedEqInsts, partitionGivenEqInsts, - +module TcTyFuns ( tcNormalizeFamInst, normaliseGivens, normaliseGivenDicts, @@ -29,64 +19,20 @@ import HsSyn 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 -\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} @@ -113,15 +59,21 @@ tcUnfoldSynFamInst (TyConApp tycon tys) | 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} @@ -161,7 +113,7 @@ tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion))) -> 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! @@ -177,21 +129,21 @@ tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys) -- 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) } @@ -273,19 +225,20 @@ normalise_dicts given_eqs dicts is_wanted %************************************************************************ %* * -\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) @@ -296,34 +249,34 @@ normaliseWanteds insts } \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 @@ -360,112 +313,127 @@ skolemOccurs (inst@(EqInst {}):insts) 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. + +(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} -simple_rewrite_check :: - ([Inst] -> TcM ()) -> - ([Inst] -> TcM ([Inst],Bool)) -simple_rewrite_check check insts - = check insts >> return (insts,False) - +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} @@ -481,9 +449,7 @@ Rewrite schemata applied by way of eq_rewrite and friends. -- >--> -- g1 := t -- -trivialInsts :: - [Inst] -> -- equations - TcM ([Inst],Bool) -- remaining equations, any changes? +trivialInsts :: RewriteRule trivialInsts [] = return ([],False) trivialInsts (i@(EqInst {}):is) @@ -499,12 +465,15 @@ 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 = 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 @@ -512,6 +481,8 @@ swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return ( -- 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 @@ -526,7 +497,12 @@ swapInst i@(EqInst {}) -- 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) @@ -539,10 +515,10 @@ swapInst i@(EqInst {}) ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co ; return (new_inst,True) } - go _ _ = return (i,False) +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) } @@ -576,7 +552,7 @@ decompInst i@(EqInst {}) 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 @@ -584,30 +560,33 @@ decompInst i@(EqInst {}) -- 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 - 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) @@ -644,11 +623,13 @@ topInst i@(EqInst {}) 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 @@ -667,7 +648,8 @@ 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 @@ -695,10 +677,10 @@ substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci 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) @@ -711,6 +693,7 @@ unifyInsts insts -- 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 @@ -721,9 +704,10 @@ unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2}) ; writeMetaTyVar cotv ty -- g := t ; return ([],True) } +unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst" -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -occursCheckInsts :: [Inst] -> TcM () +occursCheckInsts :: CheckRule occursCheckInsts insts = mappM_ occursCheckInst insts @@ -733,7 +717,7 @@ 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 @@ -752,6 +736,7 @@ occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2}) ; 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 @@ -827,8 +812,7 @@ genericNormaliseInsts isWanted fun insts } 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 @@ -862,13 +846,15 @@ genericNormaliseInsts isWanted fun insts } -- 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}