\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 Inst
import Var
import VarSet
-import VarEnv ( varEnvElts )
+import VarEnv
+import TypeRep
import Name
import NameEnv ( emptyNameEnv )
\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
-- 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
| 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
-growWantedEV gbl_tvs wev tvs
+
+growEvVar gbl_tvs ev tvs
= tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
where
- ev_tvs = growPredTyVars (wantedEvVarPred wev) tvs
+ ev_tvs = growPredTyVars (evVarPred ev) tvs
+
+growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
growWanted gbl_tvs (WcEvVar wev) tvs
= growWantedEV gbl_tvs wev tvs
growWanted gbl_tvs (WcImplic implic) tvs
- = foldrBag (growWanted (gbl_tvs `unionVarSet` ic_skols implic))
- tvs (ic_wanted implic)
+ = 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
pred = wantedEvVarPred wev
quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
+-- False => we can *definitely* float the WantedConstraint out
quantifyMeWC qtvs (WcImplic implic)
- = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted 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}
*********************************************************************************
* *
-* Superclasses *
-* *
-***********************************************************************************
-
-When constructing evidence for superclasses in an instance declaration,
- * we MUST have the "self" dictionary available, but
- * we must NOT have its superclasses derived from "self"
-
-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!!
-
-\begin{code}
-simplifySuperClass :: EvVar -- The "self" dictionary
- -> WantedConstraints
- -> TcM ()
-simplifySuperClass self wanteds
- = do { wanteds <- mapBagM zonkWanted wanteds
- ; loc <- getCtLoc NoScSkol
- ; (unsolved, 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 }
-\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
; traceTc "simplifyCheck {" (vcat
[ ptext (sLit "wanted =") <+> ppr wanteds ])
- ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
- 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
= 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 can_flats implic_wanteds
- ; bb <- getTcEvBindsBag
+ <- simpl_loop 1 inert flat_wanteds implic_wanteds
+ ; bb <- getTcEvBindsBag
+ ; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
- vcat [ text "wanteds =" <+> ppr wanteds
- , text "unsolved_flats =" <+> ppr unsolved_flats
+ vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
, text "unsolved_implics =" <+> ppr unsolved_implics
- , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
- ]
- ; return (unsolved_flats, 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
- -> CanonicalCts -- May inlude givens (in the recursive call)
+ -> InertSet
+ -> Bag WantedEvVar
-> Bag Implication
-> TcS (CanonicalCts, Bag Implication)
- simpl_loop n 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) }
- | otherwise
- = do { inert1 <- solveInteract inert can_ws
- ; let (inert2, unsolved_flats) = extractUnsolved inert1
+ -- 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) }
- ; traceTcS "solveWanteds/done flats" $
+ | otherwise
+ = do { traceTcS "solveWanteds: simpl_loop start {" $
+ vcat [ text "n =" <+> ppr n
+ , text "work_items =" <+> ppr work_items
+ , text "implics =" <+> ppr implics
+ , text "inert =" <+> ppr inert ]
+ ; 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 ]
- -- See Note [Preparing inert set for implications]
- ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
+ -- Go inside each implication
; (implic_eqs, unsolved_implics)
- <- flatMapBagPairM (solveImplication inert_for_implics) implics
+ <- solveNestedImplications inert2 unsolved_wevvars implics
- -- Apply defaulting rules if and only if there
+ -- 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_cans
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag final_eqs then
- return (unsolved_flats, unsolved_implics)
+ return (unsolved_cans, 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)
+ 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
+ }
+
+solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
+ -> TcS (Bag WantedEvVar, Bag Implication)
+solveNestedImplications inerts unsolved implics
+ | isEmptyBag implics
+ = return (emptyBag, emptyBag)
+ | otherwise
+ = do { -- See Note [Preparing inert set for implications]
+ traceTcS "solveWanteds: preparing inerts for implications {" empty
+ ; inert_for_implics <- solveInteract inerts (makeGivens unsolved)
+ ; traceTcS "}" empty
+
+ ; traceTcS "solveWanteds: doing nested implications {" $
+ vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
+ , text "implics =" <+> ppr implics ]
+
+ ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
+ tyVarsOfInert inert_for_implics
+ -- See Note [Extra TcsTv untouchables]
+ ; (implic_eqs, unsolved_implics)
+ <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
+
+ ; traceTcS "solveWanteds: done nested implications }" $
+ vcat [ text "implic_eqs =" <+> ppr implic_eqs
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
+ ; return (implic_eqs, unsolved_implics) }
+
+solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
+ -> 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
-- 2. Maybe a unsolved implication, empty if entirely solved!
--
-- Precondition: everything is zonked by now
-solveImplication inert
+solveImplication tcs_untouchables inert
imp@(Implic { ic_untch = untch
, ic_binds = ev_binds
, ic_skols = skols
, ic_given = givens
, ic_wanted = wanteds
, ic_loc = loc })
- = nestImplicTcS ev_binds untch $
+ = nestImplicTcS ev_binds (untch, tcs_untouchables) $
+ 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
- ; 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
; 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
to givens, and add them to the inert set. Reasons:
- a) In checking mode, suppresses unnecessary errors. We already have
+
+ a) In checking mode, suppresses unnecessary errors. We already have
on unsolved-wanted error; adding it to the givens prevents any
consequential errors from showing uop
+
b) More importantly, in inference mode, we are going to quantify over this
constraint, and we *don't* want to quantify over any constraints that
are deducible from it.
We were not able to solve (a ~w [beta]) but we can't just assume it as
given because the resulting set is not inert. Hence we have to do a
-'solveInteract' step first
+'solveInteract' step first.
+
+Note [Extra TcsTv untouchables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
+kind (such as variables from instance that have been applied, or unification flattens). These
+variables must be passed to the implications as extra untouchable variables. Otherwise
+we have the danger of double unifications. Example (from trac ticket #4494):
+
+ (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
+
+In this example, beta is touchable inside the implication. The first solveInteract step
+leaves 'uf' ununified. Then we move inside the implication where a new constraint
+ uf ~ beta
+emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears
+but when we pop out again we are left with (F Int ~ uf) which will be unified by our final
+solveCTyFunEqs stage and uf will get unified *once more* to (F Int).
+
+The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables)
+that are generated when solving the flats, and make them untouchables for the nested
+implication. In the example above uf would become untouchable, so beta would be forced to
+be unified as beta := uf.
+
+NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
+ of an implication becomes now untouchable next time we go inside that implication to
+ solve any residual constraints. In effect, by floating an equality out of the implication
+ we are committing to have it solved in the outside.
+
+
+\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 :: TcsUntouchables
+ -> 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.
+
*********************************************************************************
* *
\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
; 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 :: Untouchables -> TcTyVar -> TcS CanonicalCts
+defaultTyVar :: TcsUntouchables -> 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
defaultTyVar untch the_tv
| isTouchableMetaTyVar_InRange untch the_tv
, not (k `eqKind` default_k)
- = do { (ev, better_ty) <- TcSMonad.newKindConstraint 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)
- -> Untouchables -- Untouchable
+ -> TcsUntouchables -- Untouchable
-> CanonicalCts -- Unsolved
-> [[(CanonicalCt,TcTyVar)]]
findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
-> InertSet -- Given inert
-> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
-- sharing same type variable
- -> TcS CanonicalCts
+ -> TcS (Bag WantedEvVar)
disambigGroup [] _inert _grp
= return emptyBag
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 }
-
+ ; let ct_loc = get_ct_loc (cc_flavor the_ct)
+ ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
; success <- tryTcS $
- do { given_inert <- solveOne inert given_eq
- ; final_inert <- solveInteract given_inert (listToBag wanteds)
- ; let (_, unsolved) = extractUnsolved final_inert
- ; return (isEmptyBag unsolved) }
-
+ 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 { 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)
+ 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
+ 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!"
+
+
\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