Commit cfda0421 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

TcSimplify.reduceImplication: clean up

- This cleans up some of the mess in reduceImplication and documents the
  precondition on the form of wanted equalities properly.
- I also made the back off test a bit smarter by allowing to back off in the
  presence of wanted equalities as long as none of them got solved in the
  attempt.  (That should save generating some superfluous bindings.)

  MERGE TO 6.10
parent 1add6282
......@@ -40,15 +40,11 @@ module Inst (
InstOrigin(..), InstLoc, pprInstLoc,
mkWantedCo, mkGivenCo,
isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType,
mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo,
mkRightTransEqInstCo, mkAppEqInstCo,
isValidWantedEqInst,
eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
wantedToLocalEqInst, finalizeEqInst,
eqInstType, updateEqInstCoercion,
eqInstCoercion, eqInstTys
mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo,
mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo,
wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst,
wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion,
eqInstTys
) where
#include "HsVersions.h"
......@@ -121,8 +117,11 @@ instToVar (Dict {tci_name = nm, tci_pred = pred})
instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= mkLocalId nm (mkImplicTy tvs givens wanteds)
instToVar i@(EqInst {})
= eitherEqInst i id (\(TyVarTy covar) -> covar)
instToVar inst@(EqInst {})
= eitherEqInst inst id assertCoVar
where
assertCoVar (TyVarTy cotv) = cotv
assertCoVar coty = pprPanic "Inst.instToVar" (ppr coty)
instType :: Inst -> Type
instType (LitInst {tci_ty = ty}) = ty
......@@ -970,15 +969,6 @@ isWantedCo :: EqInstCo -> Bool
isWantedCo (Left _) = True
isWantedCo _ = False
fromGivenCo :: EqInstCo -> Coercion
fromGivenCo (Right co) = co
fromGivenCo _ = panic "fromGivenCo: not a wanted coercion"
fromWantedCo :: String -> EqInstCo -> TcTyVar
fromWantedCo _ (Left covar) = covar
fromWantedCo msg _ =
panic ("fromWantedCo: not a wanted coercion: " ++ msg)
eqInstCoType :: EqInstCo -> TcType
eqInstCoType (Left cotv) = mkTyVarTy cotv
eqInstCoType (Right co) = co
......@@ -1050,12 +1040,12 @@ mkAppEqInstCo (Right co) _ _
Operations on entire EqInst.
\begin{code}
-- For debugging, make sure the cotv of a wanted is not filled.
-- |A wanted equality is unsolved as long as its cotv is unfilled.
--
isValidWantedEqInst :: Inst -> TcM Bool
isValidWantedEqInst (EqInst {tci_co = Left cotv})
wantedEqInstIsUnsolved :: Inst -> TcM Bool
wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
= liftM not $ isFilledMetaTyVar cotv
isValidWantedEqInst _ = return True
wantedEqInstIsUnsolved _ = return True
eitherEqInst :: Inst -- given or wanted EqInst
-> (TcTyVar -> a) -- result if wanted
......@@ -1067,9 +1057,6 @@ eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
Right co -> withGiven co
eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
mkEqInsts :: [PredType] -> [EqInstCo] -> TcM [Inst]
mkEqInsts preds cos = zipWithM mkEqInst preds cos
mkEqInst :: PredType -> EqInstCo -> TcM Inst
mkEqInst (EqPred ty1 ty2) co
= do { uniq <- newUnique
......@@ -1112,11 +1099,11 @@ wantedToLocalEqInst eq = eq
--
finalizeEqInst :: Inst -- wanted
-> TcM Inst -- given
finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, tci_name = name})
finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2,
tci_name = name, tci_co = Left cotv})
= do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
-- fill the coercion hole
; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
; writeMetaTyVar cotv (TyVarTy var)
-- set the new coercion
......@@ -1134,7 +1121,4 @@ eqInstCoercion = tci_co
eqInstTys :: Inst -> (TcType, TcType)
eqInstTys inst = (tci_left inst, tci_right inst)
updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst
updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
\end{code}
......@@ -971,17 +971,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar]
-> [Inst] -> [Inst]
-> TcM ([Inst], TcDictBinds)
-- Make a binding that binds 'irreds', by generating an implication
-- constraint for them, *and* throwing the constraint into the LIE
-- constraint for them.
--
-- The binding looks like
-- (ir1, .., irn) = f qtvs givens
-- where f is (evidence for) the new implication constraint
-- f :: forall qtvs. {reft} givens => (ir1, .., irn)
-- qtvs includes coercion variables
-- f :: forall qtvs. givens => (ir1, .., irn)
-- qtvs includes coercion variables.
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs
givens -- Guaranteed all Dicts
-- or EqInsts
givens -- Guaranteed all Dicts or EqInsts
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
......@@ -989,28 +989,38 @@ makeImplicationBind loc all_tvs
= do { uniq <- newUnique
; span <- getSrcSpanM
; let (eq_givens, dict_givens) = partition isEqInst givens
eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
-- Urgh! See line 2187 or thereabouts. I believe that all these
-- 'givens' must be a simple CoVar. This MUST be cleaned up.
; let name = mkInternalName uniq (mkVarOcc "ic") span
-- extract equality binders
eq_cotvs = map eqInstType eq_givens
-- make the implication constraint instance
name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
; let -- only create binder for dict_irreds
(_, dict_irreds) = partition isEqInst irreds
-- same order as binders
tci_wanted = irreds,
tci_loc = loc }
-- create binders for the irreducible dictionaries
dict_irreds = filter (not . isEqInst) irreds
dict_irred_ids = map instToId dict_irreds
lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
co = mkWpApps (map instToId dict_givens)
<.> mkWpTyApps eq_tyvar_cos
<.> mkWpTyApps (mkTyVarTys all_tvs)
bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
| otherwise = PatBind { pat_lhs = lpat,
pat_rhs = unguardedGRHSs rhs,
pat_rhs_ty = hsLPatType lpat,
bind_fvs = placeHolderNames }
-- create the binding
rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
co = mkWpApps (map instToId dict_givens)
<.> mkWpTyApps eq_cotvs
<.> mkWpTyApps (mkTyVarTys all_tvs)
bind | [dict_irred_id] <- dict_irred_ids
= VarBind dict_irred_id rhs
| otherwise
= PatBind { pat_lhs = lpat
, pat_rhs = unguardedGRHSs rhs
, pat_rhs_ty = hsLPatType lpat
, bind_fvs = placeHolderNames
}
; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
; return ([implic_inst], unitBag (L span bind))
}
......@@ -2200,19 +2210,30 @@ Note that
--
-- Note on coercion variables:
--
-- The extra given coercion variables are bound at two different sites:
-- The extra given coercion variables are bound at two different
-- sites:
--
-- -) in the creation context of the implication constraint
-- the solved equational constraints use these binders
--
-- -) at the solving site of the implication constraint
-- the solved dictionaries use these binders
-- the solved dictionaries use these binders;
-- these binders are generated by reduceImplication
--
-- Note [Binders for equalities]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- To reuse the binders of local/given equalities in the binders of
-- implication constraints, it is crucial that these given equalities
-- always have the form
-- cotv :: t1 ~ t2
-- where cotv is a simple coercion type variable (and not a more
-- complex coercion term). We require that the extra_givens always
-- have this form and exploit the special form when generating binders.
reduceImplication env
orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
tci_tyvars = tvs,
tci_given = extra_givens, tci_wanted = wanteds
})
})
= do { -- Solve the sub-problem
; let try_me _ = ReduceMe -- Note [Freeness and implications]
env' = env { red_givens = extra_givens ++ red_givens env
......@@ -2239,15 +2260,17 @@ reduceImplication env
-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
-- Then we must iterate the outer loop too!
; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
-- we solve wanted eqs by side effect!
-- Progress is no longer measered by the number of bindings
-- If there are any irreds, but no bindings and no solved
-- equalities, we back off and do nothing
; let backOff = isEmptyLHsBinds binds && -- no new bindings
(not $ null irreds) && -- but still some irreds
all (not . isEqInst) wanteds
-- we may have instantiated a cotv
-- => must make a new implication constraint!
didntSolveWantedEqs -- no instantiated cotv
-- Progress is no longer measered by the number of bindings
; if backOff then -- No progress
-- If there are any irreds, we back off and do nothing
return (emptyBag, [orig_implic])
else do
{ (simpler_implic_insts, bind)
......@@ -2257,35 +2280,29 @@ reduceImplication env
-- case. After all, we only try hard to reduce at top level, or
-- when inferring types.
; let dict_wanteds = filter (not . isEqInst) wanteds
-- TOMDO: given equational constraints bug!
-- we need a different evidence for given
-- equations depending on whether we solve
-- dictionary constraints or equational constraints
(extra_eq_givens, extra_dict_givens)
= partition isEqInst extra_givens
-- SLPJ Sept 07: I think this is bogus; currently
-- there are no Eqinsts in extra_givens
dict_ids = map instToId extra_dict_givens
-- Note [Reducing implication constraints]
-- Tom -- update note, put somewhere!
; let eq_tyvars = varSetElems $ tyVarsOfTypes $
map eqInstType extra_eq_givens
-- SLPJ Sept07: this looks Utterly Wrong to me, but I think
-- that current extra_givens has no EqInsts, so
-- it makes no difference
co = wrap_inline -- Note [Always inline implication constraints]
<.> mkWpTyLams tvs
<.> mkWpTyLams eq_tyvars
<.> mkWpLams dict_ids
<.> WpLet (binds `unionBags` bind)
wrap_inline | null dict_ids = idHsWrapper
| otherwise = WpInline
rhs = mkLHsWrap co payload
loc = instLocSpan inst_loc
payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
; let -- extract Id binders for dicts and CoTyVar binders for eqs;
-- see Note [Binders for equalities]
(extra_eq_givens, extra_dict_givens) = partition isEqInst
extra_givens
eq_cotvs = map instToVar extra_eq_givens
dict_ids = map instToId extra_dict_givens
-- Note [Always inline implication constraints]
wrap_inline | null dict_ids = idHsWrapper
| otherwise = WpInline
co = wrap_inline
<.> mkWpTyLams tvs
<.> mkWpTyLams eq_cotvs
<.> mkWpLams dict_ids
<.> WpLet (binds `unionBags` bind)
rhs = mkLHsWrap co payload
loc = instLocSpan inst_loc
-- wanted equalities are solved by updating their
-- cotv; we don't generate bindings for them
dict_bndrs = map (L loc . HsVar . instToId)
. filter (not . isEqInst)
$ wanteds
payload = mkBigLHsTup dict_bndrs
; traceTc (vcat [text "reduceImplication" <+> ppr name,
......
......@@ -286,7 +286,7 @@ no further propoagation is possible.
--
normaliseEqs :: [Inst] -> TcM EqConfig
normaliseEqs eqs
= do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
= do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
; traceTc $ ptext (sLit "Entering normaliseEqs")
; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
......@@ -352,7 +352,7 @@ finaliseEqsAndDicts (EqConfig { eqs = eqs
-- Assert that all cotvs of wanted equalities are still unfilled, and
-- zonk all final insts, to make any improvement visible
; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
; zonked_locals <- zonkInsts locals'
; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
; return (zonked_locals, zonked_wanteds, final_binds, improved)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment