import Inst
import Var
import VarSet
+import VarEnv ( varEnvElts )
+
import Name
import NameEnv ( emptyNameEnv )
import Bag
TcEvBinds) -- ... binding these evidence variables
simplifyInfer apply_mr tau_tvs wanted
| isEmptyBag wanted -- Trivial case is quite common
- = do { zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
; return (qtvs, [], emptyTcEvBinds) }
, ptext (sLit "tau_tvs =") <+> ppr tau_tvs
]
- ; (simple_wanted, tc_binds)
- <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
+ -- Make a guess at the quantified type variables
+ -- Then split the constraints on the baisis of those tyvars
+ -- to avoid unnecessarily simplifying a class constraint
+ -- See Note [Avoid unecessary constraint simplification]
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
+ ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
+ zonked_tau_tvs `minusVarSet` gbl_tvs
+ (perhaps_bound, surely_free)
+ = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
+
+ ; emitConstraints surely_free
+ ; traceTc "sinf" $ vcat
+ [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
+ , ptext (sLit "surely_free =") <+> ppr surely_free
+ ]
+
+ -- Now simplify the possibly-bound constraints
+ ; (simplified_perhaps_bound, tc_binds)
+ <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
+ -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
+ -- may have done some unification
; gbl_tvs <- tcGetGlobalTyVars
- ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
- ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
- (bound, free) | apply_mr = (emptyBag, zonked_simples)
- | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
+ ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
+ ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
+ ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
+ mr_qtvs = init_tvs `minusVarSet` constrained_tvs
+ constrained_tvs = tyVarsOfWantedEvVars zonked_simples
+ qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
+ (final_qtvs, (bound, free))
+ | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
+ | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
; traceTc "end simplifyInfer }" $
vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
, text "wanted = " <+> ppr zonked_wanted
- , text "qtvs = " <+> ppr qtvs
+ , text "qtvs = " <+> ppr final_qtvs
, text "free = " <+> ppr free
, text "bound = " <+> ppr bound ]
-- Turn the quantified meta-type variables into real type variables
; emitConstraints (mapBag WcEvVar free)
- ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
+ ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
-- We use this function when inferring the type of a function
-- The wanted constraints are already zonked
simplifyAsMuchAsPossible ctxt wanteds
- = do { let untch = emptyVarSet
+ = do { let untch = NoUntouchables
-- We allow ourselves to unify environment
-- variables; hence *no untouchables*
simplifyApproxLoop 0 wanteds
-- Report any errors
- ; mapBagM_ reportUnsolvedImplication unsolved_implics
+ ; reportUnsolved (emptyBag, unsolved_implics)
; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
; return (final_wanted_evvars, ev_binds) }
\end{code}
\begin{code}
-findQuantifiedTyVars :: Bool -- Apply the MR
- -> Bag WantedEvVar -- Simplified constraints from RHS
- -> TyVarSet -- Free in tau-type of definition
- -> TyVarSet -- Free in the envt
- -> TyVarSet -- Quantify over these
-
-findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
- | isEmptyBag wanteds = init_tvs
- | apply_mr = init_tvs `minusVarSet` constrained_tvs
- | otherwise = fixVarSet mk_next init_tvs
+growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
+growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
+growWanteds gbl_tvs ws tvs
+ | isEmptyBag ws = tvs
+ | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
+growWantedEVs gbl_tvs ws tvs
+ | isEmptyBag ws = tvs
+ | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
+
+growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
+growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
+growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
+-- (growX gbls wanted tvs) grows a seed 'tvs' against the
+-- X-constraint 'wanted', nuking the 'gbls' at each stage
+
+growEvVar gbl_tvs ev tvs
+ = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
where
- init_tvs = tau_tvs `minusVarSet` gbl_tvs
- mk_next tvs = foldrBag grow_one tvs wanteds
+ ev_tvs = growPredTyVars (evVarPred ev) tvs
- grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
- where
- extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
+growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
- constrained_tvs = tyVarsOfWantedEvVars wanteds
+growWanted gbl_tvs (WcEvVar wev) tvs
+ = growWantedEV gbl_tvs wev tvs
+growWanted gbl_tvs (WcImplic implic) tvs
+ = foldrBag (growWanted inner_gbl_tvs)
+ (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
+ -- Must grow over inner givens too
+ (ic_wanted implic)
+ where
+ inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
--------------------
quantifyMe :: TyVarSet -- Quantifying over these
| otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
where
pred = wantedEvVarPred wev
+
+quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
+-- False => we can *definitely* float the WantedConstraint out
+quantifyMeWC qtvs (WcImplic implic)
+ = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
+ || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
+ where
+ inner_qtvs = qtvs `minusVarSet` ic_skols implic
+
+quantifyMeWC qtvs (WcEvVar wev)
+ = quantifyMe qtvs wev
\end{code}
+Note [Avoid unecessary constraint simplification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When inferring the type of a let-binding, with simplifyInfer,
+try to avoid unnecessariliy simplifying class constraints.
+Doing so aids sharing, but it also helps with delicate
+situations like
+ instance C t => C [t] where ..
+ f :: C [t] => ....
+ f x = let g y = ...(constraint C [t])...
+ in ...
+When inferring a type for 'g', we don't want to apply the
+instance decl, because then we can't satisfy (C t). So we
+just notice that g isn't quantified over 't' and partition
+the contraints before simplifying.
+
+This only half-works, but then let-generalisation only half-works.
+
+
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
= do { wanteds <- mapBagM zonkWanted wanteds
; loc <- getCtLoc NoScSkol
; (unsolved, ev_binds)
- <- runTcS SimplCheck emptyVarSet $
+ <- runTcS SimplCheck NoUntouchables $
do { can_self <- canGivens loc [self]
- ; let inert = foldlBag extendInertSet emptyInert can_self
+ ; let inert = foldlBag updInertSet emptyInert can_self
-- No need for solveInteract; we know it's inert
; solveWanteds inert wanteds }
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
; loc <- getCtLoc (RuleSkol name)
; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
- Implic { ic_env_tvs = emptyVarSet -- No untouchables
+ Implic { ic_untch = NoUntouchables
, ic_env = emptyNameEnv
, ic_skols = mkVarSet tv_bndrs
, ic_scoped = panic "emitImplication"
; traceTc "simplifyCheck {" (vcat
[ ptext (sLit "wanted =") <+> ppr wanteds ])
- ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
+ ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
solveWanteds emptyInert wanteds
; traceTc "simplifyCheck }" $
, text "inert =" <+> ppr inert ]
; (unsolved_flats, unsolved_implics)
<- simpl_loop 1 can_flats implic_wanteds
+ ; bb <- getTcEvBindsBag
; traceTcS "solveWanteds }" $
vcat [ text "wanteds =" <+> ppr wanteds
, text "unsolved_flats =" <+> ppr unsolved_flats
- , text "unsolved_implics =" <+> ppr unsolved_implics ]
+ , text "unsolved_implics =" <+> ppr unsolved_implics
+ , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
+ ]
; return (unsolved_flats, unsolved_implics) }
where
simpl_loop :: Int
--
-- Precondition: everything is zonked by now
solveImplication inert
- imp@(Implic { ic_env_tvs = untch
- , ic_binds = ev_binds
- , ic_skols = skols
- , ic_given = givens
+ imp@(Implic { ic_untch = untch
+ , ic_binds = ev_binds
+ , ic_skols = skols
+ , ic_given = givens
, ic_wanted = wanteds
- , ic_loc = loc })
+ , ic_loc = loc })
= nestImplicTcS ev_binds untch $
+ recoverTcS (return (emptyBag, emptyBag)) $
+ -- Recover from nested failures. Even the top level is
+ -- just a bunch of implications, so failing at the first
+ -- one is bad
do { traceTcS "solveImplication {" (ppr imp)
-- Solve flat givens
| isEmptyBag wanteds
= return emptyBag
| otherwise
- = do { untch <- getUntouchablesTcS
+ = do { untch <- getUntouchables
; tv_cts <- mapM (defaultTyVar untch) $
- varSetElems (tyVarsOfCanonicals wanteds)
+ varSetElems (tyVarsOfCDicts wanteds)
; info@(_, default_tys, _) <- getDefaultInfo
; let groups = findDefaultableGroups info untch wanteds
- ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
+ ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
, text "Type defaults =" <+> ppr deflt_cts])
; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
------------------
-defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
+defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
-- defaultTyVar is used on any un-instantiated meta type variables to
-- default the kind of ? and ?? etc to *. This is important to ensure
-- that instance declarations match. For example consider
-- whatever, because the type-class defaulting rules have yet to run.
defaultTyVar untch the_tv
- | isMetaTyVar the_tv
- , not (the_tv `elemVarSet` untch)
+ | isTouchableMetaTyVar_InRange untch the_tv
, not (k `eqKind` default_k)
- = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
+ = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
-- 'DefaultOrigin' is strictly the declaration, but it's convenient
wanted_eq = CTyEqCan { cc_id = ev
:: ( SimplContext
, [Type]
, (Bool,Bool) ) -- (Overloaded strings, extended default rules)
- -> TcTyVarSet -- Untouchable
+ -> Untouchables -- Untouchable
-> CanonicalCts -- Unsolved
-> [[(CanonicalCt,TcTyVar)]]
findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
is_defaultable_group ds@((_,tv):_)
= isTyConableTyVar tv -- Note [Avoiding spurious errors]
&& not (tv `elemVarSet` bad_tvs)
- && not (tv `elemVarSet` untch) -- Non untouchable
+ && isTouchableMetaTyVar_InRange untch tv
&& defaultable_classes [cc_class cc | (cc,_) <- ds]
is_defaultable_group [] = panic "defaultable_group"
------------------------------
disambigGroup :: [Type] -- The default types
- -> TcTyVarSet -- Untouchables
-> InertSet -- Given inert
-> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
-- sharing same type variable
-> TcS CanonicalCts
-disambigGroup [] _inert _untch _grp
+disambigGroup [] _inert _grp
= return emptyBag
-disambigGroup (default_ty:default_tys) untch inert group
+disambigGroup (default_ty:default_tys) inert group
= do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
-- We know this equality is canonical,
, cc_tyvar = the_tv
, cc_rhs = default_ty }
- ; success <- tryTcS (extendVarSet untch the_tv) $
+ ; success <- tryTcS $
do { given_inert <- solveOne inert given_eq
; final_inert <- solveInteract given_inert (listToBag wanteds)
; let (_, unsolved) = extractUnsolved final_inert
; return (unitBag given_eq) }
False -> -- Failure: try with the next type
do { traceTcS "disambigGoup succeeded" (ppr default_ty)
- ; disambigGroup default_tys untch inert group } }
+ ; disambigGroup default_tys inert group } }
where
((the_ct,the_tv):_) = group
wanteds = map fst group