\begin{code}
module TcSimplify(
- simplifyInfer, simplifySuperClass,
+ simplifyInfer,
simplifyDefault, simplifyDeriv, simplifyBracket,
simplifyRule, simplifyTop, simplifyInteractive
) where
import HsSyn
import TcRnMonad
import TcErrors
-import TcCanonical
import TcMType
import TcType
import TcSMonad
import Data.List ( partition )
import Outputable
import FastString
-import Control.Monad ( unless )
\end{code}
\begin{code}
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
--- Usually these will be implications, when there is
--- nothing to quanitfy we don't wrap in a degenerate implication,
--- so we do that here instead
+-- Usually these will be implications,
+-- but when there is nothing to quantify we don't wrap
+-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
= simplifyCheck SimplCheck wanteds
*********************************************************************************
* *
-* Superclasses *
-* *
-***********************************************************************************
-
-When constructing evidence for superclasses in an instance declaration,
- * we MUST have the "self" dictionary available
-
-Moreover, we must *completely* solve the constraints right now,
-not wrap them in an implication constraint to solve later. Why?
-Because when that implication constraint is solved there may
-be some unrelated other solved top-level constraints that
-recursively depend on the superclass we are building. Consider
- class Ord a => C a where
- instance C [Int] where ...
-Then we get
- dCListInt :: C [Int]
- dCListInt = MkC $cNum ...
-
- $cNum :: Ord [Int] -- The superclass
- $cNum = let self = dCListInt in <solve Ord [Int]>
-
-Now, if there is some *other* top-level constraint solved
-looking like
- foo :: Ord [Int]
- foo = scsel dCInt
-we must not solve the (Ord [Int]) wanted from foo!
-
-Note [Dependencies in self dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Moreover, notice that when solving for a superclass, we record the dependency of
-self on the superclass. This is because this dependency is not evident in the
-EvBind of the self dictionary, which only involves a call to a DFun. Example:
-
-class A a => C a
-instance B a => C a
-
-When we check the instance declaration, we pass in a self dictionary that is merely
- self = dfun b
-But we will be asked to solve that from:
- [Given] d : B a
- [Derived] self : C a
-We can show:
- [Wanted] sc : A a
-The problem is that self *depends* on the sc variable, but that is not apparent in
-the binding self = dfun b. So we record the extra dependency, using the evidence bind:
- EvBind self (EvDFunApp dfun [b] [b,sc])
-It is these dependencies that are the ''true'' dependencies in an EvDFunApp, and those
-that we must chase in function isGoodRecEv (in TcSMonad)
-
-\begin{code}
-simplifySuperClass :: [TyVar]
- -> [EvVar] -- givens
- -> EvVar -- the superclass we must solve for
- -> EvBind -- the 'self' evidence bind
- -> TcM TcEvBinds
--- Post:
--- ev_binds <- simplifySuperClasses tvs inst_givens sc_dict self_ev_bind
--- Then:
--- 1) ev_binds already contains self_ev_bind
--- 2) if successful then ev_binds contains binding for
--- the wanted superclass, sc_dict
-simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev)
- = do { giv_loc <- getCtLoc InstSkol -- For the inst_givens
- ; want_loc <- getCtLoc ScOrigin -- As wanted/derived (for the superclass and self)
- ; lcl_env <- getLclTypeEnv
-
- -- Record the dependency of self_dict to sc_dict, see Note [Dependencies in self dictionaries]
- ; let wanted = unitBag $ WcEvVar $ WantedEvVar sc_dict want_loc
- self_ev_with_dep
- = case self_ev of
- EvDFunApp df tys insts deps -> EvDFunApp df tys insts (sc_dict:deps)
- _ -> panic "Self-dictionary not EvDFunApp!"
-
- -- And solve for it
- ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
- <- runTcS SimplCheck NoUntouchables $
- do { -- Record a binding for self_dict that *depends on sc_dict*
- -- And canonicalise self_dict (which adds its superclasses)
- -- with a Derived origin, which in turn triggers the
- -- goodRecEv recursive-evidence check
- ; setEvBind self_dict self_ev_with_dep
- ; can_selfs <- mkCanonical (Derived want_loc DerSelf) self_dict
-
- -- The rest is just like solveImplication
- ; can_inst_givens <- mkCanonicals (Given giv_loc) inst_givens
- ; inert <- solveInteract emptyInert $
- can_inst_givens `andCCan` can_selfs
- ; solveWanteds inert wanted }
-
- -- For error reporting, conjure up a fake implication,
- -- so that we get decent error messages
- ; let implic = Implic { ic_untch = NoUntouchables
- , ic_env = lcl_env
- , ic_skols = mkVarSet tvs
- , ic_given = inst_givens
- , ic_wanted = mapBag WcEvVar unsolved_flats
- , ic_scoped = panic "super1"
- , ic_binds = panic "super2"
- , ic_loc = giv_loc }
- ; ASSERT (isEmptyBag unsolved_implics) -- Impossible to have any implications!
- unless (isEmptyBag unsolved_flats) $
- reportUnsolved (emptyBag, unitBag implic) frozen_errors
-
- ; return (EvBinds ev_binds) }
-\end{code}
-
-
-*********************************************************************************
-* *
* RULES *
* *
***********************************************************************************
Note [Simplifying RULE lhs constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-On the LHS of transformation rules we only simplify only equalitis,
+On the LHS of transformation rules we only simplify only equalities,
but not dictionaries. We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule. We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
-- out of one or more of the implications
solveWanteds inert wanteds
= do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
- ; can_flats <- canWanteds $ bagToList flat_wanteds
; traceTcS "solveWanteds {" $
vcat [ text "wanteds =" <+> ppr wanteds
, text "inert =" <+> ppr inert ]
; (unsolved_flats, unsolved_implics)
- <- simpl_loop 1 inert can_flats implic_wanteds
+ <- simpl_loop 1 inert flat_wanteds implic_wanteds
; bb <- getTcEvBindsBag
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
where
simpl_loop :: Int
-> InertSet
- -> CanonicalCts -- May inlude givens (in the recursive call)
+ -> Bag WantedEvVar
-> Bag Implication
-> TcS (CanonicalCts, Bag Implication)
- simpl_loop n inert can_ws implics
+ simpl_loop n inert work_items implics
| n>10
- = trace "solveWanteds: loop" $ -- Always bleat
+ = trace "solveWanteds: loop" $ -- Always bleat
do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
- ; return (can_ws, implics) }
+
+ -- We don't want to call the canonicalizer on those wanted ev vars
+ -- so try one last time to solveInteract them
+ ; inert1 <- solveInteract inert $
+ mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
+ ; let (_, unsolved_cans) = extractUnsolved inert1
+ ; return (unsolved_cans, implics) }
| otherwise
= do { traceTcS "solveWanteds: simpl_loop start {" $
vcat [ text "n =" <+> ppr n
- , text "can_ws =" <+> ppr can_ws
+ , text "work_items =" <+> ppr work_items
, text "implics =" <+> ppr implics
, text "inert =" <+> ppr inert ]
- ; inert1 <- solveInteract inert can_ws
- ; let (inert2, unsolved_flats) = extractUnsolved inert1
+ ; inert1 <- solveInteract inert $
+ mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
+ ; let (inert2, unsolved_cans) = extractUnsolved inert1
+ unsolved_wevvars
+ = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
-- NB: Importantly, inerts2 may contain *more* givens than inert
-- because of having solved equalities from can_ws
; traceTcS "solveWanteds: done flats" $
vcat [ text "inerts =" <+> ppr inert2
- , text "unsolved =" <+> ppr unsolved_flats ]
+ , text "unsolved =" <+> ppr unsolved_cans ]
-- Go inside each implication
; (implic_eqs, unsolved_implics)
- <- solveNestedImplications inert2 unsolved_flats implics
+ <- solveNestedImplications inert2 unsolved_wevvars implics
-- Apply defaulting rules if and only if there
-- no floated equalities. If there are, they may
-- solve the remaining wanteds, so don't do defaulting.
; final_eqs <- if not (isEmptyBag implic_eqs)
then return implic_eqs
- else applyDefaultingRules inert2 unsolved_flats
-
- -- default_eqs are *givens*, so simpl_loop may
- -- recurse with givens in the argument
+ else applyDefaultingRules inert2 unsolved_cans
; traceTcS "solveWanteds: simpl_loop end }" $
vcat [ text "final_eqs =" <+> ppr final_eqs
- , text "unsolved_flats =" <+> ppr unsolved_flats
+ , text "unsolved_flats =" <+> ppr unsolved_cans
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag final_eqs then
- return (unsolved_flats, unsolved_implics)
+ return (unsolved_cans, unsolved_implics)
else
- do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
- -- final eqs is *just* a bunch of WantedEvVars
- ; simpl_loop (n+1) inert2
- (can_final_eqs `andCCan` unsolved_flats) unsolved_implics
+ simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
+ (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
-- Important: reiterate with inert2, not plainly inert
-- because inert2 may contain more givens, as the result of solving
- -- some wanteds in the incoming can_ws
- }
+ -- some wanteds in the incoming can_ws
}
-solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication
+solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
-> TcS (Bag WantedEvVar, Bag Implication)
solveNestedImplications inerts unsolved implics
| isEmptyBag implics
do { traceTcS "solveImplication {" (ppr imp)
-- Solve flat givens
- ; can_givens <- canGivens loc givens
- ; given_inert <- solveInteract inert can_givens
+-- ; can_givens <- canGivens loc givens
+-- ; let given_fl = Given loc
+ ; given_inert <- solveInteract inert $
+ mapBag (\c -> (Given loc,c)) (listToBag givens)
-- Simplify the wanteds
; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
\begin{code}
applyDefaultingRules :: InertSet
- -> CanonicalCts -- All wanteds
+ -> CanonicalCts -- All wanteds
-> TcS (Bag WantedEvVar) -- All wanteds again!
-- Return some *extra* givens, which express the
-- type-class-default choice
= do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
; let ct_loc = get_ct_loc (cc_flavor the_ct)
; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
- ; let wanted_eq = CTyEqCan { cc_id = ev
- , cc_flavor = Wanted ct_loc
- , cc_tyvar = the_tv
- , cc_rhs = default_ty }
; success <- tryTcS $
- do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
- ; let (_, unsolved) = extractUnsolved final_inert
- ; errs <- getTcSErrorsBag
+ do { final_inert <- solveInteract inert $
+ consBag (Wanted ct_loc, ev) wanted_to_solve
+ ; let (_, unsolved) = extractUnsolved final_inert
+ ; errs <- getTcSErrorsBag
; return (isEmptyBag unsolved && isEmptyBag errs) }
-
; case success of
True -> -- Success: record the type variable binding, and return
do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
; disambigGroup default_tys inert group } }
where
((the_ct,the_tv):_) = group
- wanteds = map fst group
- wanted_ev_vars = map deCanonicaliseWanted wanteds
+ wanteds = map fst group
+ wanted_ev_vars = map deCanonicaliseWanted wanteds
+ wanted_to_solve = listToBag $
+ map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
get_ct_loc (Wanted l) = l
get_ct_loc _ = panic "Asked to disambiguate given or derived!"
projects / ghc-hetmet.git / blobdiff