import Inst
import Var
import VarSet
+import VarEnv
+import TypeRep
+
import Name
import NameEnv ( emptyNameEnv )
import Bag
, 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 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_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*
- ; ((unsolved_flats, unsolved_implics), ev_binds)
+ ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
<- runTcS ctxt untch $
simplifyApproxLoop 0 wanteds
-- Report any errors
- ; reportUnsolved (emptyBag, unsolved_implics)
+ ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
- ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
- ; return (final_wanted_evvars, ev_binds) }
+ ; return (unsolved_flats, ev_binds) }
where
simplifyApproxLoop :: Int -> WantedConstraints
- -> TcS (CanonicalCts, Bag Implication)
+ -> TcS (Bag WantedEvVar, Bag Implication)
simplifyApproxLoop n wanteds
| n > 10
= pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
; let (extra_flats, thiner_unsolved_implics)
= approximateImplications unsolved_implics
unsolved
- = mkWantedConstraints unsolved_flats thiner_unsolved_implics
+ = Bag.mapBag WcEvVar unsolved_flats `unionBags`
+ Bag.mapBag WcImplic thiner_unsolved_implics
- ;-- If no new work was produced then we are done with simplifyApproxLoop
+ ; -- If no new work was produced then we are done with simplifyApproxLoop
if isEmptyBag extra_flats
then do { traceTcS "simplifyApproxLoopRes" (vcat
[ ptext (sLit "Wanted = ") <+> ppr wanteds
\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:
simplifySuperClass self wanteds
= do { wanteds <- mapBagM zonkWanted wanteds
; loc <- getCtLoc NoScSkol
- ; (unsolved, ev_binds)
- <- runTcS SimplCheck emptyVarSet $
+ ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
+ <- runTcS SimplCheck NoUntouchables $
do { can_self <- canGivens loc [self]
; let inert = foldlBag updInertSet emptyInert can_self
-- No need for solveInteract; we know it's inert
; solveWanteds inert wanteds }
; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
- reportUnsolved unsolved }
+ reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
\end{code}
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
; loc <- getCtLoc (RuleSkol name)
; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
- Implic { ic_untch = 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 $
- solveWanteds emptyInert wanteds
+ ; (unsolved, frozen_errors, ev_binds)
+ <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
; traceTc "simplifyCheck }" $
ptext (sLit "unsolved =") <+> ppr unsolved
- ; reportUnsolved unsolved
+ ; reportUnsolved unsolved frozen_errors
; return ev_binds }
----------------
-solveWanteds :: InertSet -- Given
- -> WantedConstraints -- Wanted
- -> TcS (CanonicalCts, -- Unsolved flats
- Bag Implication) -- Unsolved implications
+solveWanteds :: InertSet -- Given
+ -> WantedConstraints -- Wanted
+ -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why
+ -- they are WantedConstraints and not CanonicalCts
+ Bag Implication) -- Unsolved implications
-- solveWanteds iterates when it is able to float equalities
-- out of one or more of the implications
solveWanteds inert wanteds
vcat [ text "wanteds =" <+> ppr wanteds
, text "inert =" <+> ppr inert ]
; (unsolved_flats, unsolved_implics)
- <- simpl_loop 1 can_flats implic_wanteds
+ <- simpl_loop 1 inert can_flats implic_wanteds
+ ; bb <- getTcEvBindsBag
+ ; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
- vcat [ text "wanteds =" <+> ppr wanteds
- , text "unsolved_flats =" <+> ppr unsolved_flats
- , text "unsolved_implics =" <+> ppr unsolved_implics ]
- ; return (unsolved_flats, unsolved_implics) }
+ vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
+ , text "unsolved_implics =" <+> ppr unsolved_implics
+ , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
+ , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
+ ]
+
+ ; solveCTyFunEqs unsolved_flats unsolved_implics
+ -- See Note [Solving Family Equations]
+ }
where
simpl_loop :: Int
+ -> InertSet
-> CanonicalCts -- May inlude givens (in the recursive call)
-> Bag Implication
-> TcS (CanonicalCts, Bag Implication)
- simpl_loop n can_ws implics
+ simpl_loop n inert can_ws implics
| n>10
= trace "solveWanteds: loop" $ -- Always bleat
do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
; return (can_ws, implics) }
| otherwise
- = do { inert1 <- solveInteract inert can_ws
+ = do { traceTcS "solveWanteds: simpl_loop start {" $
+ vcat [ text "n =" <+> ppr n
+ , text "can_ws =" <+> ppr can_ws
+ , text "implics =" <+> ppr implics
+ , text "inert =" <+> ppr inert ]
+ ; inert1 <- solveInteract inert can_ws
; let (inert2, unsolved_flats) = extractUnsolved inert1
- ; traceTcS "solveWanteds/done flats" $
+ -- 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 ]
-- See Note [Preparing inert set for implications]
; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
- ; (implic_eqs, unsolved_implics)
+ ; traceTcS "solveWanteds: doing nested implications {" $
+ vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
+ , text "implics =" <+> ppr implics ]
+ ; (implic_eqs, unsolved_implics)
<- flatMapBagPairM (solveImplication inert_for_implics) implics
- -- Apply defaulting rules if and only if there
+ ; traceTcS "solveWanteds: done nested implications }" $
+ vcat [ text "implic_eqs =" <+> ppr implic_eqs
+ , text "unsolved_implics =" <+> ppr unsolved_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
+ ; traceTcS "solveWanteds: simpl_loop end }" $
+ vcat [ text "final_eqs =" <+> ppr final_eqs
+ , text "unsolved_flats =" <+> ppr unsolved_flats
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
; if isEmptyBag final_eqs then
return (unsolved_flats, unsolved_implics)
else
- do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
- [ text "floated_unsolved_eqs =" <+> ppr final_eqs
- , text "unsolved_implics = " <+> ppr unsolved_implics ]
- ; simpl_loop (n+1)
- (unsolved_flats `unionBags` final_eqs)
- unsolved_implics
- } }
-
-solveImplication :: InertSet -- Given
- -> Implication -- Wanted
- -> TcS (CanonicalCts, -- Unsolved unification var = type
- Bag Implication) -- Unsolved rest (always empty or singleton)
+ 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
+ -- 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
+ } }
+
+solveImplication :: InertSet -- Given
+ -> Implication -- Wanted
+ -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
+ Bag Implication) -- Unsolved rest (always empty or singleton)
-- Returns:
-- 1. A bag of floatable wanted constraints, not mentioning any skolems,
-- that are of the form unification var = type
, ic_wanted = wanteds
, 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
; let (res_flat_free, res_flat_bound)
= floatEqualities skols givens unsolved_flats
- unsolved = mkWantedConstraints res_flat_bound unsolved_implics
+ unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
+ Bag.mapBag WcImplic unsolved_implics
; traceTcS "solveImplication end }" $ vcat
[ text "res_flat_free =" <+> ppr res_flat_free
; return (res_flat_free, res_bag) }
-floatEqualities :: TcTyVarSet -> [EvVar]
- -> CanonicalCts -> (CanonicalCts, CanonicalCts)
+floatEqualities :: TcTyVarSet -> [EvVar]
+ -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
+ -- The CanonicalCts will be floated out to be used later, whereas
+ -- the remaining WantedEvVars will remain inside the implication.
floatEqualities skols can_given wanteds
| hasEqualities can_given = (emptyBag, wanteds)
- | otherwise = partitionBag is_floatable wanteds
- where
- is_floatable :: CanonicalCt -> Bool
- is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
- | isMetaTyVar tv || isMetaTyVarTy ty
- = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
- is_floatable _ = False
+ -- Note [Float Equalities out of Implications]
+ | otherwise = partitionBag is_floatable wanteds
+ where is_floatable :: WantedEvVar -> Bool
+ is_floatable (WantedEvVar cv _)
+ | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
+ is_floatable _wv = False
+
+ tvs_under_fsks :: Type -> TyVarSet
+ -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
+ tvs_under_fsks (TyVarTy tv)
+ | not (isTcTyVar tv) = unitVarSet tv
+ | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
+ | otherwise = unitVarSet tv
+ tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
+ tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
+ tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
+ tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
+ tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
+ -- can mention type variables!
+ | isTyVar tv = inner_tvs `delVarSet` tv
+ | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
+ inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
+ where
+ inner_tvs = tvs_under_fsks ty
+
+ predTvs_under_fsks :: PredType -> TyVarSet
+ predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
+ predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
+ predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
+
+
+
+
\end{code}
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to float equalities out of vanilla existentials, but *not* out
+of GADT pattern matches.
+
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we convert any unsolved flat wanteds
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first
+\begin{code}
+
+solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
+-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
+-- See Note [Solving Family Equations]
+-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
+-- where the newly generated equalities (alpha := F xi) have been substituted through.
+solveCTyFunEqs cts implics
+ = do { untch <- getUntouchables
+ ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
+ ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
+ , ppr funeq_bnds
+ ])
+ ; mapM_ solve_one funeq_bnds
+
+ -- Apply the substitution through to eliminate the flatten
+ -- unification variables we substituted both in the unsolved flats and implics
+ ; let final_unsolved
+ = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
+ final_implics
+ = Bag.mapBag (subst_impl funeq_bnds) implics
+
+ ; return (final_unsolved, final_implics) }
+
+ where solve_one (tv,(ty,cv,fl))
+ | not (typeKind ty `isSubKind` tyVarKind tv)
+ = addErrorTcS KindError fl (mkTyVarTy tv) ty
+ -- Must do a small kind check since TcCanonical invariants
+ -- on family equations only impose compatibility, not subkinding
+ | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
+
+ subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
+ subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
+ subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
+
+ subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
+ subst_wevar funeq_bnds (WantedEvVar v loc)
+ = let orig_ty = varType v
+ new_ty = substFunEqBnds funeq_bnds orig_ty
+ in WantedEvVar (setVarType v new_ty) loc
+
+ subst_impl :: FunEqBinds -> Implication -> Implication
+ subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
+ = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
+
+
+type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
+-- Invariant: if it contains:
+-- [... a -> (ta,...) ... b -> (tb,...) ... ]
+-- then 'ta' cannot mention 'b'
+
+getSolvableCTyFunEqs :: Untouchables
+ -> CanonicalCts -- Precondition: all wanteds
+ -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
+getSolvableCTyFunEqs untch cts
+ = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
+ where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
+ , cc_flavor = fl
+ , cc_fun = tc
+ , cc_tyargs = xis
+ , cc_rhs = xi })
+ | Just tv <- tcGetTyVar_maybe xi
+ , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
+ , Nothing <- lookup tv extra_binds -- or in extra_binds
+ -- See Note [Solving Family Equations], Point 1
+ = ASSERT ( isWanted fl )
+ let ty_orig = mkTyConApp tc xis
+ ty_bind = substFunEqBnds extra_binds ty_orig
+ in if tv `elemVarSet` tyVarsOfType ty_bind
+ then (cts_in `extendCCans` ct, extra_binds)
+ -- See Note [Solving Family Equations], Point 2
+ else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
+ -- Postcondition met because extra_binds is already applied to ty_bind
+
+ dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
+
+substFunEqBnds :: FunEqBinds -> TcType -> TcType
+substFunEqBnds bnds ty
+ = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
+ -- foldr works because of the FunEqBinds invariant
+
+
+\end{code}
+
+Note [Solving Family Equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+After we are done with simplification we may be left with constraints of the form:
+ [Wanted] F xis ~ beta
+If 'beta' is a touchable unification variable not already bound in the TyBinds
+then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
+
+When is it ok to do so?
+ 1) 'beta' must not already be defaulted to something. Example:
+
+ [Wanted] F Int ~ beta <~ Will default [beta := F Int]
+ [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
+ have to report this as unsolved.
+
+ 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
+ set [beta := F xis] only if beta is not among the free variables of xis.
+
+ 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
+ of type family equations. See Inert Set invariants in TcInteract.
+
+
*********************************************************************************
* *
* Defaulting and disamgiguation *
\begin{code}
applyDefaultingRules :: InertSet
- -> CanonicalCts -- All wanteds
- -> TcS CanonicalCts
+ -> CanonicalCts -- All wanteds
+ -> TcS (Bag WantedEvVar) -- All wanteds again!
-- Return some *extra* givens, which express the
-- type-class-default choice
| 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) }
+ ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
------------------
-defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
+defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar)
-- 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 <- 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
- , cc_flavor = Wanted loc
- , cc_tyvar = the_tv
- , cc_rhs = better_ty }
- ; return (unitBag wanted_eq) }
-
+ ; return (unitBag (WantedEvVar ev loc)) }
| otherwise
- = return emptyCCan -- The common case
+ = return emptyBag -- The common case
where
k = tyVarKind the_tv
default_k = defaultKind k
:: ( 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
+ -> TcS (Bag WantedEvVar)
-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,
- -- so we directly construct it as such
- ; let given_eq = CTyEqCan { cc_id = ev
- , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
- , cc_tyvar = the_tv
- , cc_rhs = default_ty }
-
- ; success <- tryTcS (extendVarSet untch the_tv) $
- do { given_inert <- solveOne inert given_eq
- ; final_inert <- solveInteract given_inert (listToBag wanteds)
- ; let (_, unsolved) = extractUnsolved final_inert
- ; return (isEmptyBag unsolved) }
+ ; 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
+ ; return (isEmptyBag unsolved && isEmptyBag errs) }
; case success of
- True -> -- Success: record the type variable binding, and return
- do { setWantedTyBind the_tv default_ty
- ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
- ; traceTcS "disambigGoup succeeded" (ppr default_ty)
- ; return (unitBag given_eq) }
+ True -> -- Success: record the type variable binding, and return
+ do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
+ ; traceTcS "disambigGroup succeeded" (ppr default_ty)
+ ; return (unitBag $ WantedEvVar ev ct_loc) }
False -> -- Failure: try with the next type
- do { traceTcS "disambigGoup succeeded" (ppr default_ty)
- ; disambigGroup default_tys untch inert group } }
+ do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
+ ; disambigGroup default_tys inert group } }
where
((the_ct,the_tv):_) = group
wanteds = map fst group
wanted_ev_vars = map deCanonicaliseWanted wanteds
+
+ get_ct_loc (Wanted l) = l
+ get_ct_loc _ = panic "Asked to disambiguate given or derived!"
+
+
\end{code}
Note [Avoiding spurious errors]
dealing with the (Num a) context arising from f's definition;
we try to unify a with Int (to default it), but find that it's
already been unified with the rigid variable from g's type sig
-
-
projects / ghc-hetmet.git / blobdiff