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

EqInst related clean up

- Remove some unused and some superflous functions
- Add comments regarding ancestor equalities
- Tidied ancestor equality computation
- Replace some incorrect instToId by instToVar (but there are still some
  bad ones around as we still get warnings with -DDEBUG)
- Some cleaned up layout
NB: Code growth is just due to more comments.
parent 0bca9b76
......@@ -979,11 +979,10 @@ fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
fromWantedCo _ (Left covar) = covar
fromWantedCo msg _ = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
eitherEqInst
:: Inst -- given or wanted EqInst
-> (TcTyVar -> a) -- result if wanted
-> (Coercion -> a) -- result if given
-> a
eitherEqInst :: Inst -- given or wanted EqInst
-> (TcTyVar -> a) -- result if wanted
-> (Coercion -> a) -- result if given
-> a
eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
= case either_co of
Left covar -> withWanted covar
......
......@@ -635,6 +635,17 @@ In addition to the basic Haskell variants of 'Inst's, they can now also
represent implication constraints 'forall tvs. (reft, given) => wanted'
and equality constraints 'co :: ty1 ~ ty2'.
NB: Equalities occur in two flavours:
(1) Dict {tci_pred = EqPred ty1 ty2}
(2) EqInst {tci_left = ty1, tci_right = ty2, tci_co = coe}
The former arises from equalities in contexts, whereas the latter is used
whenever the type checker introduces an equality (e.g., during deferring
unification).
I am not convinced that this duplication is necessary or useful! -=chak
\begin{code}
data Inst
= Dict {
......
......@@ -989,17 +989,15 @@ makeImplicationBind loc all_tvs reft
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
; let (eq_givens,dict_givens) = partitionGivenEqInsts givens
; let (eq_givens, dict_givens) = partition isEqInst givens
eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
; let
-- only create binder for dict_irreds
-- we
(eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
; let -- only create binder for dict_irreds
(eq_irreds, dict_irreds) = partition isEqInst irreds
n_dict_irreds = length dict_irreds
dict_irred_ids = map instToId dict_irreds
tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
......@@ -1653,12 +1651,25 @@ data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
-- Note [SUPER-CLASS LOOP 1]
\end{code}
%************************************************************************
%* *
\subsection[reduce]{@reduce@}
%* *
%************************************************************************
Note [Ancestor Equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~
During context reduction, we add to the wanted equalities also those
equalities that (transitively) occur in superclass contexts of wanted
class constraints. Consider the following code
class a ~ Int => C a
instance C Int
If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
substituting Int for a. Hence, we ultimately want (C Int), which we
discharge with the explicit instance.
\begin{code}
reduceContext :: RedEnv
......@@ -1677,35 +1688,32 @@ reduceContext env wanteds
text "----------------------"
]))
; let givens = red_givens env
(given_eqs0, given_dicts0) = partition isEqInst givens
(wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
; let givens = red_givens env
(given_eqs0,given_dicts0) = partitionGivenEqInsts givens
(wanted_eqs0,wanted_dicts) = partitionWantedEqInsts wanteds
-- We want to add as wanted equalities those that (transitively)
-- occur in superclass contexts of wanted class constraints.
-- See Note [Ancestor Equalities]
; ancestor_eqs <- ancestorEqualities wanted_dicts
; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
; wanted_ancestor_eqs <- (mapM wantedAncestorEqualities wanted_dicts >>= \ls -> return (concat ls))
; traceTc (text "test wanted SCs" <+> ppr wanted_ancestor_eqs)
; let wanted_eqs = wanted_ancestor_eqs ++ wanted_eqs0
-- 1. Normalise the *given* *equality* constraints
; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
; -- 1. Normalise the *given* *equality* constraints
(given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0
; -- 2. Normalise the *given* *dictionary* constraints
-- 2. Normalise the *given* *dictionary* constraints
-- wrt. the toplevel and given equations
(given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0
; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
given_dicts0
; -- 3. Solve the *wanted* *equation* constraints
eq_irreds0 <- solveWanteds given_eqs wanted_eqs
-- 3. Solve the *wanted* *equation* constraints
; eq_irreds0 <- solveWanteds given_eqs wanted_eqs
-- 4. Normalise the *wanted* equality constraints with respect to each other
-- 4. Normalise the *wanted* equality constraints with respect to
-- each other
; eq_irreds <- normaliseWanteds eq_irreds0
-- -- Do the real work
-- -- Process non-implication constraints first, so that they are
-- -- available to help solving the implication constraints
-- -- ToDo: seems a bit inefficient and ad-hoc
-- ; let (implics, rest) = partition isImplicInst wanteds
-- ; avails <- reduceList env (rest ++ implics) init_state
-- 5. Build the Avail mapping from "given_dicts"
; init_state <- foldlM addGiven emptyAvails given_dicts
......@@ -1714,18 +1722,18 @@ reduceContext env wanteds
; wanted_dicts' <- zonkInsts wanted_dicts
; avails <- reduceList env wanted_dicts' init_state
; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
; traceTc (text "reduceContext extractresults" <+> vcat
[ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens])
; traceTc $ text "reduceContext extractresults" <+> vcat
[ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
; -- 7. Normalise the *wanted* *dictionary* constraints
-- 7. Normalise the *wanted* *dictionary* constraints
-- wrt. the toplevel and given equations
(irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
; -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
(irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
-- 8. Substitute the wanted *equations* in the wanted *dictionaries*
; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
; -- 9. eliminate the artificial skolem constants introduced in 1.
eliminate_skolems
-- 9. eliminate the artificial skolem constants introduced in 1.
; eliminate_skolems
-- If there was some FD improvement,
-- or new wanted equations have been exposed,
......@@ -1733,7 +1741,7 @@ reduceContext env wanteds
; let improved = availsImproved avails
|| (not $ isEmptyBag normalise_binds1)
|| (not $ isEmptyBag normalise_binds2)
|| (not $ null $ fst $ partitionGivenEqInsts irreds)
|| (any isEqInst irreds)
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
......@@ -1749,7 +1757,13 @@ reduceContext env wanteds
text "----------------------"
]))
; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) }
; return (improved,
given_binds `unionBags` normalise_binds1
`unionBags` normalise_binds2
`unionBags` binds,
irreds ++ eq_irreds,
needed_givens)
}
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
......@@ -2086,7 +2100,7 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
-- when inferring types.
; let dict_wanteds = filter (not . isEqInst) wanteds
(extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens
(extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
dict_ids = map instToId extra_dict_givens
-- TOMDO: given equational constraints bug!
-- we need a different evidence for given
......@@ -2417,7 +2431,7 @@ addAvailAndSCs want_scs avails inst avail
where
is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
-- Note: this compares by *type*, not by Unique
deps = findAllDeps (unitVarSet (instToId inst)) avail
deps = findAllDeps (unitVarSet (instToVar inst)) avail
dep_tys = map idType (varSetElems deps)
findAllDeps :: IdSet -> AvailHow -> IdSet
......@@ -2459,39 +2473,41 @@ addSCs is_loop avails dict
; addSCs is_loop avails' sc_dict }
where
sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
is_given :: Inst -> Bool
is_given sc_dict = case findAvail avails sc_dict of
Just (Given _) -> True -- Given is cheaper than superclass selection
other -> False
wantedAncestorEqualities :: Inst -> TcM [Inst]
wantedAncestorEqualities dict
| isClassDict dict
= mapM mkWantedEqInst $ filter isEqPred $ bagToList $ wantedAncestorEqualities' (dictPred dict) emptyBag
| otherwise
= return []
wantedAncestorEqualities' :: PredType -> Bag PredType -> Bag PredType
wantedAncestorEqualities' pred bag
= ASSERT( isClassPred pred )
let (clas, tys) = getClassPredTys pred
-- From the a set of insts obtain all equalities that (transitively) occur in
-- superclass contexts of class constraints (aka the ancestor equalities).
--
ancestorEqualities :: [Inst] -> TcM [Inst]
ancestorEqualities
= mapM mkWantedEqInst -- turn only equality predicates..
. filter isEqPred -- ..into wanted equality insts
. bagToList
. addAEsToBag emptyBag -- collect the superclass constraints..
. map dictPred -- ..of all predicates in a bag
. filter isClassDict
where
addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
addAEsToBag bag [] = bag
addAEsToBag bag (pred:preds)
| pred `elemBag` bag = addAEsToBag bag preds
| isEqPred pred = addAEsToBag bagWithPred preds
| isClassPred pred = addAEsToBag bagWithPred predsWithSCs
| otherwise = addAEsToBag bag preds
where
bagWithPred = bag `snocBag` pred
predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
--
(tyvars, sc_theta, _, _) = classBigSig clas
sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
add_sc bag sc_pred
| elemBag sc_pred bag = bag
| not (isEqPred sc_pred)
&& not (isClassPred sc_pred)
= bag
| isEqPred sc_pred = consBag sc_pred bag
| otherwise = let bag' = consBag sc_pred bag
in wantedAncestorEqualities' sc_pred bag'
in foldl add_sc bag sc_theta'
(clas, tys) = getClassPredTys pred
\end{code}
%************************************************************************
%* *
\section{tcSimplifyTop: defaulting}
......
......@@ -8,9 +8,6 @@
-- for details
module TcTyFuns(
finalizeEqInst,
partitionWantedEqInsts, partitionGivenEqInsts,
tcNormalizeFamInst,
normaliseGivens, normaliseGivenDicts,
......@@ -46,49 +43,6 @@ 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
\end{code}
%************************************************************************
%* *
......@@ -503,8 +457,10 @@ trivialInsts (i@(EqInst {}):is)
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
......
......@@ -858,8 +858,8 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall
; let
-- The WpLet binds any Insts which came out of the simplification.
dict_ids = map instToId dicts
co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
dict_vars = map instToVar dicts
co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
; returnM (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
......
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