\begin{code}
module TcSimplify(
simplifyInfer,
- simplifyDefault, simplifyDeriv, simplifyBracket,
+ simplifyDefault, simplifyDeriv,
simplifyRule, simplifyTop, simplifyInteractive
) where
import TcSMonad
import TcInteract
import Inst
+import Id ( evVarPred )
+import Unify ( niFixTvSubst, niSubstTvSet )
import Var
import VarSet
import VarEnv
+import Coercion
import TypeRep
import Name
import PrelInfo
import PrelNames
import Class ( classKey )
-import BasicTypes ( RuleName )
-import Data.List ( partition )
+import BasicTypes ( RuleName, TopLevelFlag, isTopLevel )
+import Control.Monad ( when )
import Outputable
import FastString
\end{code}
-- 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
+ = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
simplifyDefault :: ThetaType -- Wanted; has no type variables in it
-> TcM () -- Succeeds iff the constraint is soluble
simplifyDefault theta
- = do { loc <- getCtLoc DefaultOrigin
- ; wanted <- newWantedEvVars theta
- ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
- ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
+ = do { wanted <- newFlatWanteds DefaultOrigin theta
+ ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults")))
+ (mkFlatWC wanted)
; return () }
\end{code}
-simplifyBracket is used when simplifying the constraints arising from
-a Template Haskell bracket [| ... |]. We want to check that there aren't
-any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
-Show instance), but we aren't otherwise interested in the results.
-Nor do we care about ambiguous dictionaries etc. We will type check
-this bracket again at its usage site.
-
-\begin{code}
-simplifyBracket :: WantedConstraints -> TcM ()
-simplifyBracket wanteds
- = do { zonked_wanteds <- mapBagM zonkWanted wanteds
- ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
- ; return () }
-\end{code}
*********************************************************************************
\begin{code}
simplifyDeriv :: CtOrigin
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
+ -> PredType
+ -> [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possibles
-simplifyDeriv orig tvs theta
- = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
- -- One reason is that the constraint solving machinery
- -- expects *TcTyVars* not TyVars. Another is that
- -- when looking up instances we don't want overlap
- -- of type variables
+-- Fail if not possible
+simplifyDeriv orig pred tvs theta
+ = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
+ -- The constraint solving machinery
+ -- expects *TcTyVars* not TyVars.
+ -- We use *non-overlappable* (vanilla) skolems
+ -- See Note [Overlap and deriving]
; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
-
- ; loc <- getCtLoc orig
- ; wanted <- newWantedEvVars (substTheta skol_subst theta)
- ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
+ subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+ doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
- ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
- ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
+ ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
- ; let (good, bad) = partition validDerivPred $
- foldrBag ((:) . wantedEvVarPred) [] unsolved
- -- See Note [Exotic derived instance contexts]
- subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+ ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
+ ; (residual_wanted, _binds)
+ <- runTcS (SimplInfer doc) NoUntouchables $
+ solveWanteds emptyInert (mkFlatWC wanted)
- ; reportUnsolvedDeriv bad loc
- ; return $ substTheta subst_skol good }
+ ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
+ -- See Note [Exotic derived instance contexts]
+ get_good :: WantedEvVar -> Either PredType WantedEvVar
+ get_good wev | validDerivPred p = Left p
+ | otherwise = Right wev
+ where p = evVarOfPred wev
+
+ ; reportUnsolved (residual_wanted { wc_flat = bad })
+
+ ; let min_theta = mkMinimalBySCs (bagToList good)
+ ; return (substTheta subst_skol min_theta) }
\end{code}
+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+ data Show a => Show [a] where ..
+ data Show [Char] where ...
+
+Now a data type with deriving:
+ data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+ instance Show [a] => Show (T a) where...
+and NOT
+ instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+ f x = show [x]
+and we want to infer
+ f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+ the context for the derived instance.
+ Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context. It's a
***********************************************************************************
\begin{code}
-simplifyInfer :: Bool -- Apply monomorphism restriction
- -> TcTyVarSet -- These type variables are free in the
- -- types to be generalised
+simplifyInfer :: TopLevelFlag
+ -> Bool -- Apply monomorphism restriction
+ -> [(Name, TcTauType)] -- Variables to be generalised,
+ -- and their tau-types
-> WantedConstraints
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints
TcEvBinds) -- ... binding these evidence variables
-simplifyInfer apply_mr tau_tvs wanted
- | isEmptyBag wanted -- Trivial case is quite common
- = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
- ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
- ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
+simplifyInfer top_lvl apply_mr name_taus wanteds
+ | isEmptyWC wanteds
+ = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
+ ; zonked_taus <- zonkTcTypes (map snd name_taus)
+ ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
+ ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
; return (qtvs, [], emptyTcEvBinds) }
| otherwise
- = do { zonked_wanted <- mapBagM zonkWanted wanted
+ = do { zonked_wanteds <- zonkWC wanteds
+ ; zonked_taus <- zonkTcTypes (map snd name_taus)
+ ; gbl_tvs <- tcGetGlobalTyVars
+
; traceTc "simplifyInfer {" $ vcat
[ ptext (sLit "apply_mr =") <+> ppr apply_mr
- , ptext (sLit "wanted =") <+> ppr zonked_wanted
- , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
+ , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
+ , ptext (sLit "wanted =") <+> ppr zonked_wanteds
]
- -- Make a guess at the quantified type variables
+ -- Step 1
+ -- 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 $
+ ; let zonked_tau_tvs = get_tau_tvs zonked_taus
+ proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
zonked_tau_tvs `minusVarSet` gbl_tvs
- (perhaps_bound, surely_free)
- = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
-
- ; emitConstraints surely_free
+ (perhaps_bound, surely_free)
+ = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
+
+ ; traceTc "simplifyInfer proto" $ vcat
+ [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
+ , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
+ , ptext (sLit "surely_fref =") <+> ppr surely_free
+ ]
+
+ ; emitFlats 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 simplified_perhaps_bound
+ -- Step 2
+ -- Now simplify the possibly-bound constraints
+ ; (simpl_results, tc_binds0)
+ <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
+ simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
+
+ ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
+ (do { reportUnsolved simpl_results; failM })
+
+ -- Step 3
+ -- Split again simplified_perhaps_bound, because some unifications
+ -- may have happened, and emit the free constraints.
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
+ ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
mr_qtvs = init_tvs `minusVarSet` constrained_tvs
- constrained_tvs = tyVarsOfWantedEvVars zonked_simples
+ constrained_tvs = tyVarsOfEvVarXs 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)
+ ; emitFlats free
+
+ ; if isEmptyVarSet final_qtvs && isEmptyBag bound
+ then ASSERT( isEmptyBag (wc_insol simpl_results) )
+ do { traceTc "} simplifyInfer/no quantification" empty
+ ; emitImplications (wc_impl simpl_results)
+ ; return ([], [], EvBinds tc_binds0) }
+ else do
+
+ -- Step 4, zonk quantified variables
+ { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
+ ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
+ | (name, ty) <- name_taus ]
+ -- Don't add the quantified variables here, because
+ -- they are also bound in ic_skols and we want them to be
+ -- tidied uniformly
+ skol_info = InferSkol poly_ids
+
+ ; gloc <- getCtLoc skol_info
+ ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
+
+ -- Step 5
+ -- Minimize `bound' and emit an implication
+ ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
+ ; ev_binds_var <- newTcEvBinds
+ ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
+ ; lcl_env <- getLclTypeEnv
+ ; let implic = Implic { ic_untch = NoUntouchables
+ , ic_env = lcl_env
+ , ic_skols = mkVarSet qtvs_to_return
+ , ic_given = minimal_bound_ev_vars
+ , ic_wanted = simpl_results { wc_flat = bound }
+ , ic_insol = False
+ , ic_binds = ev_binds_var
+ , ic_loc = gloc }
+ ; emitImplication implic
+ ; traceTc "} simplifyInfer/produced residual implication for quantification" $
+ vcat [ ptext (sLit "implic =") <+> ppr implic
+ -- ic_skols, ic_given give rest of result
+ , ptext (sLit "qtvs =") <+> ppr final_qtvs
+ , ptext (sLit "spb =") <+> ppr zonked_simples
+ , ptext (sLit "bound =") <+> ppr bound ]
+
+
+
+ ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
+ where
+ get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
+ | otherwise = exactTyVarsOfTypes
+ -- See Note [Silly type synonym] in TcType
+\end{code}
- ; traceTc "end simplifyInfer }" $
- vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
- , text "wanted = " <+> ppr zonked_wanted
- , 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 final_qtvs)
- ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
- ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
-
-------------------------
-simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
- -> TcM (Bag WantedEvVar, Bag EvBind)
--- We use this function when inferring the type of a function
--- The wanted constraints are already zonked
-simplifyAsMuchAsPossible ctxt wanteds
- = do { let untch = NoUntouchables
- -- We allow ourselves to unify environment
- -- variables; hence *no untouchables*
- ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
- <- runTcS ctxt untch $
- simplifyApproxLoop 0 wanteds
+Note [Minimize by Superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- -- Report any errors
- ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
+When we quantify over a constraint, in simplifyInfer we need to
+quantify over a constraint that is minimal in some sense: For
+instance, if the final wanted constraint is (Eq alpha, Ord alpha),
+we'd like to quantify over Ord alpha, because we can just get Eq alpha
+from superclass selection from Ord alpha. This minimization is what
+mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
+to check the original wanted.
- ; return (unsolved_flats, ev_binds) }
+\begin{code}
+simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
+simplifyWithApprox wanted
+ = do { traceTcS "simplifyApproxLoop" (ppr wanted)
+ ; results <- solveWanteds emptyInert wanted
+
+ ; let (residual_implics, floats) = approximateImplications (wc_impl results)
+
+ -- If no new work was produced then we are done with simplifyApproxLoop
+ ; if insolubleWC results || isEmptyBag floats
+ then return results
+
+ else solveWanteds emptyInert
+ (WC { wc_flat = floats `unionBags` wc_flat results
+ , wc_impl = residual_implics
+ , wc_insol = emptyBag }) }
+
+approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
+-- Extracts any nested constraints that don't mention the skolems
+approximateImplications impls
+ = do_bag (float_implic emptyVarSet) impls
where
- simplifyApproxLoop :: Int -> WantedConstraints
- -> TcS (Bag WantedEvVar, Bag Implication)
- simplifyApproxLoop n wanteds
- | n > 10
- = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
- | otherwise
- = do { traceTcS "simplifyApproxLoop" (vcat
- [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
- ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
-
- ; let (extra_flats, thiner_unsolved_implics)
- = approximateImplications unsolved_implics
- unsolved
- = 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 isEmptyBag extra_flats
- then do { traceTcS "simplifyApproxLoopRes" (vcat
- [ ptext (sLit "Wanted = ") <+> ppr wanteds
- , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
- ; return (unsolved_flats, unsolved_implics) }
-
- else -- Produced new flat work wanteds, go round the loop
- simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
- }
-
-approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
--- (wc1, impls2) <- approximateImplications impls
--- splits 'impls' into two parts
--- wc1: a bag of constraints that do not mention any skolems
--- impls2: a bag of *thiner* implication constraints
-approximateImplications impls
- = splitBag (do_implic emptyVarSet) impls
- where
- ------------------
- do_wanted :: TcTyVarSet -> WantedConstraint
- -> (WantedConstraints, WantedConstraints)
- do_wanted skols (WcImplic impl)
- = let (fl_w, mb_impl) = do_implic skols impl
- in (fl_w, mapBag WcImplic mb_impl)
- do_wanted skols wc@(WcEvVar wev)
- | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
- | otherwise = (emptyBag, unitBag wc)
-
- ------------------
- do_implic :: TcTyVarSet -> Implication
- -> (WantedConstraints, Bag Implication)
- do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
- = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
- else unitBag impl{ ic_wanted = rest_wanted } )
- where
- (floatable_wanted, rest_wanted)
- = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
-
- ------------------
- splitBag :: (a -> (WantedConstraints, Bag a))
- -> Bag a -> (WantedConstraints, Bag a)
- splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
- where
- do_one x (b1,b2)
- = (wcs `unionBags` b1, imps `unionBags` b2)
- where
- (wcs, imps) = f x
+ do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
+ do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
+ plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
+ plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
+
+ float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
+ float_implic skols imp
+ = (unitBag (imp { ic_wanted = wanted' }), floats)
+ where
+ (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
+
+ float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
+ = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
+ where
+ (flat', floats1) = do_bag (float_flat skols) flat
+ (implic', floats2) = do_bag (float_implic skols) implic
+
+ float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
+ float_flat skols wev
+ | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
+ | otherwise = (unitBag wev, emptyBag)
\end{code}
\begin{code}
-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
+-- It's conservative in that if the seed could *possibly*
+-- grow to include a type variable, then it does
-growEvVar gbl_tvs ev tvs
- = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
- where
- ev_tvs = growPredTyVars (evVarPred ev) tvs
+growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
+growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
-growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
+growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
+growWantedEVs gbl_tvs ws tvs
+ | isEmptyBag ws = tvs
+ | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
-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)
+-------- Helper functions, do not do fixpoint ------------------------
+growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
+growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
+ growPreds gbl_tvs evVarOfPred (wc_flat wc) .
+ growPreds gbl_tvs evVarOfPred (wc_insol wc)
+
+growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
+growImplics gbl_tvs implics tvs
+ = foldrBag grow_implic tvs implics
+ where
+ grow_implic implic tvs
+ = grow tvs `minusVarSet` ic_skols implic
+ where
+ grow = growWC gbl_tvs (ic_wanted implic) .
+ growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
+ -- We must grow from givens too; see test IPRun
+
+growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
+growPreds gbl_tvs get_pred items tvs
+ = foldrBag extend tvs items
where
- inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
+ extend item tvs = tvs `unionVarSet`
+ (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
--------------------
quantifyMe :: TyVarSet -- Quantifying over these
| isIPPred pred = True -- Note [Inheriting implicit parameters]
| 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
+ pred = evVarOfPred wev
\end{code}
Note [Avoid unecessary constraint simplification]
TcEvBinds) -- Evidence for RHS
-- See Note [Simplifying RULE lhs constraints]
simplifyRule name tv_bndrs lhs_wanted rhs_wanted
- = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
- ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
+ = do { loc <- getCtLoc (RuleSkol name)
+ ; zonked_lhs <- zonkWC lhs_wanted
+ ; let untch = NoUntouchables
+ -- We allow ourselves to unify environment
+ -- variables; hence *no untouchables*
+
+ ; (lhs_results, lhs_binds)
+ <- runTcS (SimplRuleLhs name) untch $
+ solveWanteds emptyInert zonked_lhs
+
+ ; traceTc "simplifyRule" $
+ vcat [ text "zonked_lhs" <+> ppr zonked_lhs
+ , text "lhs_results" <+> ppr lhs_results
+ , text "lhs_binds" <+> ppr lhs_binds
+ , text "rhs_wanted" <+> ppr rhs_wanted ]
+
-- Don't quantify over equalities (judgement call here)
- ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
- lhs_dicts = map wantedEvVarToVar (bagToList dicts)
- -- Dicts and implicit parameters
- ; reportUnsolvedWantedEvVars eqs
+ ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
+ (wc_flat lhs_results)
+ lhs_dicts = map evVarOf (bagToList dicts)
+ -- Dicts and implicit parameters
+
+ -- Fail if we have not got down to unsolved flats
+ ; ev_binds_var <- newTcEvBinds
+ ; emitImplication $ Implic { ic_untch = untch
+ , ic_env = emptyNameEnv
+ , ic_skols = mkVarSet tv_bndrs
+ , ic_given = lhs_dicts
+ , ic_wanted = lhs_results { wc_flat = eqs }
+ , ic_insol = insolubleWC lhs_results
+ , ic_binds = ev_binds_var
+ , ic_loc = loc }
-- Notice that we simplify the RHS with only the explicitly
-- introduced skolems, allowing the RHS to constrain any
-- Hence the rather painful ad-hoc treatement here
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
- ; loc <- getCtLoc (RuleSkol name)
- ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
- Implic { ic_untch = NoUntouchables
- , ic_env = emptyNameEnv
- , ic_skols = mkVarSet tv_bndrs
- , ic_scoped = panic "emitImplication"
- , ic_given = lhs_dicts
- , ic_wanted = rhs_wanted
- , ic_binds = rhs_binds_var
- , ic_loc = loc }
+ ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
+ ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
+ WC { wc_flat = emptyBag
+ , wc_insol = emptyBag
+ , wc_impl = unitBag $
+ Implic { ic_untch = NoUntouchables
+ , ic_env = emptyNameEnv
+ , ic_skols = mkVarSet tv_bndrs
+ , ic_given = lhs_dicts
+ , ic_wanted = rhs_wanted
+ , ic_insol = insolubleWC rhs_wanted
+ , ic_binds = rhs_binds_var
+ , ic_loc = loc } }
; rhs_binds2 <- readTcRef evb_ref
; return ( lhs_dicts
--
-- Fails if can't solve something in the input wanteds
simplifyCheck ctxt wanteds
- = do { wanteds <- mapBagM zonkWanted wanteds
+ = do { wanteds <- zonkWC wanteds
; traceTc "simplifyCheck {" (vcat
[ ptext (sLit "wanted =") <+> ppr wanteds ])
- ; (unsolved, frozen_errors, ev_binds)
- <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
+ ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
+ solveWanteds emptyInert wanteds
; traceTc "simplifyCheck }" $
- ptext (sLit "unsolved =") <+> ppr unsolved
+ ptext (sLit "unsolved =") <+> ppr unsolved
- ; reportUnsolved unsolved frozen_errors
+ ; reportUnsolved unsolved
; return ev_binds }
----------------
-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
- ; traceTcS "solveWanteds {" $
- vcat [ text "wanteds =" <+> ppr wanteds
- , text "inert =" <+> ppr inert ]
- ; (unsolved_flats, unsolved_implics)
- <- simpl_loop 1 inert flat_wanteds implic_wanteds
+solveWanteds :: InertSet -- Given
+ -> WantedConstraints
+ -> TcS WantedConstraints
+solveWanteds inert wanted
+ = do { (unsolved_flats, unsolved_implics, insols)
+ <- solve_wanteds inert wanted
+ ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived
+ , wc_impl = unsolved_implics
+ , wc_insol = insols }) }
+
+solve_wanteds :: InertSet -- Given
+ -> WantedConstraints
+ -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
+-- solve_wanteds iterates when it is able to float equalities
+-- out of one or more of the implications
+solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
+ = do { traceTcS "solveWanteds {" (ppr wanted)
+
+ -- Try the flat bit
+ -- Discard from insols all the derived/given constraints
+ -- because they will show up again when we try to solve
+ -- everything else. Solving them a second time is a bit
+ -- of a waste, but the code is simple, and the program is
+ -- wrong anyway!
+ ; let all_flats = flats `unionBags` keepWanted insols
+ ; inert1 <- solveInteractWanted inert (bagToList all_flats)
+
+ ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
+
; bb <- getTcEvBindsBag
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
vcat [ 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))
, text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
]
- ; solveCTyFunEqs unsolved_flats unsolved_implics
+ ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
-- See Note [Solving Family Equations]
- }
+ -- NB: remaining_flats has already had subst applied
+
+ ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
+
+ ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
+ , mapBag (substImplication subst) unsolved_implics
+ , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
+
where
- simpl_loop :: Int
- -> InertSet
- -> Bag WantedEvVar
+ simpl_loop :: Int
+ -> InertSet
-> Bag Implication
- -> TcS (CanonicalCts, Bag Implication)
- simpl_loop n inert work_items implics
+ -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
+ simpl_loop n inert implics
| n>10
= trace "solveWanteds: loop" $ -- Always bleat
do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
-
- -- 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
+ ; let (_, unsolved_cans) = extractUnsolved inert
; return (unsolved_cans, implics) }
| 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_cans ]
-
- -- Go inside each implication
+ , text "inert =" <+> ppr inert ]
+
+ ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
+ -- unsolved_cans contains either Wanted or Derived!
+
; (implic_eqs, unsolved_implics)
- <- solveNestedImplications inert2 unsolved_wevvars implics
+ <- solveNestedImplications just_given_inert unsolved_cans 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_cans
+ ; improve_eqs <- if not (isEmptyBag implic_eqs)
+ then return implic_eqs
+ else applyDefaultingRules just_given_inert unsolved_cans
; traceTcS "solveWanteds: simpl_loop end }" $
- vcat [ text "final_eqs =" <+> ppr final_eqs
- , text "unsolved_flats =" <+> ppr unsolved_cans
+ vcat [ text "improve_eqs =" <+> ppr improve_eqs
+ , text "unsolved_flats =" <+> ppr unsolved_cans
, text "unsolved_implics =" <+> ppr unsolved_implics ]
- ; if isEmptyBag final_eqs then
+ ; (improve_eqs_already_in_inert, inert_with_improvement)
+ <- solveInteract inert improve_eqs
+
+ ; if improve_eqs_already_in_inert then
return (unsolved_cans, unsolved_implics)
else
- 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
+ simpl_loop (n+1) inert_with_improvement
+ -- Contain unsolved_cans and the improve_eqs
+ unsolved_implics
}
-solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
- -> TcS (Bag WantedEvVar, Bag Implication)
-solveNestedImplications inerts unsolved implics
+givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
+-- Extract the Wanted ones from CanonicalCts and conver to
+-- Givens; not Given/Solved, see Note [Preparing inert set for implications]
+givensFromWanteds _ctxt = foldrBag getWanted emptyBag
+ where
+ getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
+ getWanted cc givens
+ | pushable_wanted cc
+ = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
+ in given `consBag` givens -- and not mkSolvedFlavor,
+ -- see Note [Preparing inert set for implications]
+ | otherwise = givens
+
+ pushable_wanted :: CanonicalCt -> Bool
+ pushable_wanted cc
+ | not (isCFrozenErr cc)
+ , isWantedCt cc
+ = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
+ | otherwise = False
+
+solveNestedImplications :: InertSet -> CanonicalCts
+ -> Bag Implication
+ -> TcS (Bag FlavoredEvVar, Bag Implication)
+solveNestedImplications just_given_inert unsolved_cans 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
+ = do { -- See Note [Preparing inert set for implications]
+ -- Push the unsolved wanteds inwards, but as givens
+
+ ; simpl_ctx <- getTcSContext
- ; traceTcS "solveWanteds: doing nested implications {" $
+ ; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans
+ tcs_untouchables = filterVarSet isFlexiTcsTv $
+ tyVarsOfEvVarXs pushed_givens
+ -- See Note [Extra TcsTv untouchables]
+
+ ; traceTcS "solveWanteds: preparing inerts for implications {"
+ (vcat [ppr tcs_untouchables, ppr pushed_givens])
+
+ ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
+
+ ; traceTcS "solveWanteds: } now 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
; 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)
+solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
+ -> InertSet -- Given
+ -> Implication -- Wanted
+ -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: 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
do { traceTcS "solveImplication {" (ppr imp)
-- Solve flat givens
--- ; can_givens <- canGivens loc givens
--- ; let given_fl = Given loc
- ; given_inert <- solveInteract inert $
- mapBag (\c -> (Given loc,c)) (listToBag givens)
+ ; given_inert <- solveInteractGiven inert loc givens
-- Simplify the wanteds
- ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
+ ; (unsolved_flats, unsolved_implics, insols)
+ <- solve_wanteds given_inert wanteds
- ; let (res_flat_free, res_flat_bound)
- = floatEqualities skols givens unsolved_flats
- unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
- Bag.mapBag WcImplic unsolved_implics
+ ; let (res_flat_free, res_flat_bound)
+ = floatEqualities skols givens unsolved_flats
+ final_flat = keepWanted res_flat_bound
+
+ ; let res_wanted = WC { wc_flat = final_flat
+ , wc_impl = unsolved_implics
+ , wc_insol = insols }
+ res_implic = unitImplication $
+ imp { ic_wanted = res_wanted
+ , ic_insol = insolubleWC res_wanted }
; traceTcS "solveImplication end }" $ vcat
[ text "res_flat_free =" <+> ppr res_flat_free
- , text "res_flat_bound =" <+> ppr res_flat_bound
- , text "unsolved_implics =" <+> ppr unsolved_implics ]
+ , text "res_implic =" <+> ppr res_implic ]
- ; let res_bag | isEmptyBag unsolved = emptyBag
- | otherwise = unitBag (imp { ic_wanted = unsolved })
+ ; return (res_flat_free, res_implic) }
- ; return (res_flat_free, res_bag) }
-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)
+floatEqualities :: TcTyVarSet -> [EvVar]
+ -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
+-- Post: The returned FlavoredEvVar's are only Wanted or Derived
+-- and come from the input wanted ev vars or deriveds
+floatEqualities skols can_given wantders
+ | hasEqualities can_given = (emptyBag, wantders)
-- Note [Float Equalities out of Implications]
- | otherwise = partitionBag is_floatable wanteds
- where is_floatable :: WantedEvVar -> Bool
- is_floatable (WantedEvVar cv _)
+ | otherwise = partitionBag is_floatable wantders
+
+
+ where is_floatable :: FlavoredEvVar -> Bool
+ is_floatable (EvVarX cv _fl)
| isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
- is_floatable _wv = False
+ is_floatable _flev = False
tvs_under_fsks :: Type -> TyVarSet
-- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
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
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
+ consequential errors from showing up
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.
+ c) Flattened type-family equalities must be exposed to the nested
+ constraints. Consider
+ F b ~ alpha, (forall c. F b ~ alpha)
+ Obviously this is soluble with [alpha := F b]. But the
+ unification is only done by solveCTyFunEqs, right at the end of
+ solveWanteds, and if we aren't careful we'll end up with an
+ unsolved goal inside the implication. We need to "push" the
+ as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
+ can be used to solve the inner (F b
+ ~ alpha). See Trac #4935.
+
+ d) There are other cases where interactions between wanteds that can help
+ to solve a constraint. For example
+
+ class C a b | a -> b
+
+ (C Int alpha), (forall d. C d blah => C Int a)
+
+ If we push the (C Int alpha) inwards, as a given, it can produce
+ a fundep (alpha~a) and this can float out again and be used to
+ fix alpha. (In general we can't float class constraints out just
+ in case (C d blah) might help to solve (C Int a).)
+
The unsolved wanteds are *canonical* but they may not be *inert*,
because when made into a given they might interact with other givens.
Hence the call to solveInteract. Example:
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first.
+Finally, note that we convert them to [Given] and NOT [Given/Solved].
+The reason is that Given/Solved are weaker than Givens and may be discarded.
+As an example consider the inference case, where we may have, the following
+original constraints:
+ [Wanted] F Int ~ Int
+ (F Int ~ a => F Int ~ a)
+If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next
+given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting
+the (F Int ~ a) insoluble. Hence we should really convert the residual
+wanteds to plain old Given.
+
+We need only push in unsolved equalities both in checking mode and inference mode:
+
+ (1) In checking mode we should not push given dictionaries in because of
+example LongWayOverlapping.hs, where we might get strange overlap
+errors between far-away constraints in the program. But even in
+checking mode, we must still push type family equations. Consider:
+
+ type instance F True a b = a
+ type instance F False a b = b
+
+ [w] F c a b ~ gamma
+ (c ~ True) => a ~ gamma
+ (c ~ False) => b ~ gamma
+
+Since solveCTyFunEqs happens at the very end of solving, the only way to solve
+the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not
+merely Given/Solved because it has to interact with the top-level instance
+environment) and push it inside the implications. Now, when we come out again at
+the end, having solved the implications solveCTyFunEqs will solve this equality.
+
+ (2) In inference mode, we recheck the final constraint in checking mode and
+hence we will be able to solve inner implications from top-level quantified
+constraints nonetheless.
+
+
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):
+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
+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).
+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.
-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.
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to float equalities out of vanilla existentials, but *not* out
+of GADT pattern matches.
\begin{code}
-solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
+solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
-- 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
+solveCTyFunEqs cts
= do { untch <- getUntouchables
- ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
+ ; let (unsolved_can_cts, (ni_subst, cv_binds))
+ = getSolvableCTyFunEqs untch cts
; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
- , ppr funeq_bnds
+ , ppr ni_subst, ppr cv_binds
])
- ; 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'
+ ; mapM_ solve_one cv_binds
+ ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
+ where
+ solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
+ ; setCoBind cv (mkReflCo ty) }
+
+------------
+type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
+ -- The TvSubstEnv is not idempotent, but is loop-free
+ -- See Note [Non-idempotent substitution] in Unify
+emptyFunEqBinds :: FunEqBinds
+emptyFunEqBinds = (emptyVarEnv, [])
+
+extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds (tv_subst, cv_binds) cv tv ty
+ = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
+
+------------
getSolvableCTyFunEqs :: TcsUntouchables
- -> CanonicalCts -- Precondition: all wanteds
+ -> CanonicalCts -- Precondition: all Wanteds or Derived!
-> (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
-
-
+ = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
+ where
+ dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
+ -> (CanonicalCts, FunEqBinds)
+ dflt_funeq (cts_in, feb@(tv_subst, _))
+ (CFunEqCan { cc_id = cv
+ , cc_flavor = fl
+ , cc_fun = tc
+ , cc_tyargs = xis
+ , cc_rhs = xi })
+ | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
+
+ , isTouchableMetaTyVar_InRange untch tv
+ -- And it's a *touchable* unification variable
+
+ , typeKind xi `isSubKind` tyVarKind tv
+ -- Must do a small kind check since TcCanonical invariants
+ -- on family equations only impose compatibility, not subkinding
+
+ , not (tv `elemVarEnv` tv_subst)
+ -- Check not in extra_binds
+ -- See Note [Solving Family Equations], Point 1
+
+ , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
+ -- Occurs check: see Note [Solving Family Equations], Point 2
+ = ASSERT ( not (isGivenOrSolved fl) )
+ (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
+
+ dflt_funeq (cts_in, fun_eq_binds) ct
+ = (cts_in `extendCCans` ct, fun_eq_binds)
\end{code}
Note [Solving Family Equations]
\begin{code}
applyDefaultingRules :: InertSet
- -> CanonicalCts -- All wanteds
- -> TcS (Bag WantedEvVar) -- All wanteds again!
+ -> CanonicalCts -- All wanteds
+ -> TcS (Bag FlavoredEvVar) -- All wanteds again!
-- Return some *extra* givens, which express the
-- type-class-default choice
; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
------------------
-defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar)
+defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
-- 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
, not (k `eqKind` default_k)
= do { ev <- TcSMonad.newKindConstraint the_tv default_k
; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
- ; return (unitBag (WantedEvVar ev loc)) }
+ ; return (unitBag (mkEvVarX ev (Wanted loc))) }
| otherwise
= return emptyBag -- The common case
where
-> InertSet -- Given inert
-> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
-- sharing same type variable
- -> TcS (Bag WantedEvVar)
+ -> TcS (Bag FlavoredEvVar)
disambigGroup [] _inert _grp
= return emptyBag
disambigGroup (default_ty:default_tys) inert group
= 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
- ; success <- tryTcS $
- do { final_inert <- solveInteract inert $
- consBag (Wanted ct_loc, ev) wanted_to_solve
+ ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
+ ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
+ derived_eq = mkEvVarX ev der_flav
+
+ ; success <- tryTcS $
+ do { (_,final_inert) <- solveInteract inert $ listToBag $
+ derived_eq : wanted_ev_vars
; let (_, unsolved) = extractUnsolved final_inert
- ; errs <- getTcSErrorsBag
- ; return (isEmptyBag unsolved && isEmptyBag errs) }
+ ; let wanted_unsolved = filterBag isWantedCt unsolved
+ -- Don't care about Derived's
+ ; return (isEmptyBag wanted_unsolved) }
; case success of
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) }
+ ; return (unitBag derived_eq) }
False -> -- Failure: try with the next type
- do { traceTcS "disambigGroup failed, will try other default types" (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
- 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!"
-
+ wanted_ev_vars :: [FlavoredEvVar]
+ wanted_ev_vars = map deCanonicalise wanteds
+ mk_derived_flavor :: CtFlavor -> CtFlavor
+ mk_derived_flavor (Wanted loc) = Derived loc
+ mk_derived_flavor _ = 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
+
+
+
+*********************************************************************************
+* *
+* Utility functions
+* *
+*********************************************************************************
+
+\begin{code}
+newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
+newFlatWanteds orig theta
+ = do { loc <- getCtLoc orig
+ ; evs <- newWantedEvVars theta
+ ; return (listToBag [EvVarX w loc | w <- evs]) }
+\end{code}
\ No newline at end of file