\begin{code}
module TcSimplify(
- simplifyInfer, simplifySuperClass,
- simplifyDefault, simplifyDeriv, simplifyBracket,
+ simplifyInfer,
+ simplifyDefault, simplifyDeriv,
simplifyRule, simplifyTop, simplifyInteractive
) where
import HsSyn
import TcRnMonad
import TcErrors
-import TcCanonical
import TcMType
import TcType
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 NameEnv ( emptyNameEnv )
import Bag
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}
\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
+ = 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)
+
+ ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
- ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
- ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
+ ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
+ ; (residual_wanted, _binds)
+ <- runTcS (SimplInfer doc) NoUntouchables $
+ solveWanteds emptyInert (mkFlatWC wanted)
- ; let (good, bad) = partition validDerivPred $
- foldrBag ((:) . wantedEvVarPred) [] unsolved
- -- See Note [Exotic derived instance contexts]
- subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+ ; 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
- ; reportUnsolvedDeriv bad loc
- ; return $ substTheta subst_skol good }
+ ; 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 (varSetElems 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
]
- ; (simple_wanted, tc_binds)
- <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
-
- ; gbl_tvs <- tcGetGlobalTyVars
- ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
- ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
- (bound, free) | apply_mr = (emptyBag, zonked_simples)
- | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
-
- ; traceTc "end simplifyInfer }" $
- vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
- , text "wanted = " <+> ppr zonked_wanted
- , text "qtvs = " <+> ppr 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)
- ; 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 = emptyVarSet
- -- We allow ourselves to unify environment
- -- variables; hence *no untouchables*
+ -- 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]
+ ; 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 (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
+ ]
- ; ((unsolved_flats, unsolved_implics), ev_binds)
- <- runTcS ctxt untch $
- simplifyApproxLoop 0 wanteds
+ ; emitFlats surely_free
+ ; traceTc "sinf" $ vcat
+ [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
+ , ptext (sLit "surely_free =") <+> ppr surely_free
+ ]
- -- Report any errors
- ; reportUnsolved (emptyBag, unsolved_implics)
+ -- 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 = 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}
- ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
- ; return (final_wanted_evvars, ev_binds) }
+Note [Minimize by Superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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.
+
+\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 (CanonicalCts, 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
- = mkWantedConstraints unsolved_flats 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}
-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
+-- (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
+
+growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
+growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
+
+growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
+growWantedEVs gbl_tvs ws tvs
+ | isEmptyBag ws = tvs
+ | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
+
+-------- 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
- init_tvs = tau_tvs `minusVarSet` gbl_tvs
- mk_next tvs = foldrBag grow_one tvs wanteds
-
- grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
- where
- extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
-
- constrained_tvs = tyVarsOfWantedEvVars wanteds
+ 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
+ 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
+ pred = evVarOfPred 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:
*********************************************************************************
* *
-* 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 emptyVarSet $
- do { can_self <- canGivens loc [self]
- ; let inert = foldlBag extendInertSet 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
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_env_tvs = emptyVarSet -- No untouchables
- , 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, ev_binds) <- runTcS ctxt emptyVarSet $
+ ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
solveWanteds emptyInert wanteds
; traceTc "simplifyCheck }" $
- ptext (sLit "unsolved =") <+> ppr unsolved
+ ptext (sLit "unsolved =") <+> ppr unsolved
; reportUnsolved unsolved
; return ev_binds }
----------------
-solveWanteds :: InertSet -- Given
- -> WantedConstraints -- Wanted
- -> TcS (CanonicalCts, -- Unsolved flats
- 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
+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 "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))
+ ]
+
+ ; (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
- -> CanonicalCts -- May inlude givens (in the recursive call)
+ simpl_loop :: Int
+ -> InertSet
-> Bag Implication
- -> TcS (CanonicalCts, Bag Implication)
- simpl_loop n can_ws implics
+ -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
+ simpl_loop n inert 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) }
+ ; let (_, unsolved_cans) = extractUnsolved inert
+ ; return (unsolved_cans, implics) }
| otherwise
- = do { inert1 <- solveInteract inert can_ws
- ; let (inert2, unsolved_flats) = extractUnsolved inert1
-
- ; traceTcS "solveWanteds/done flats" $
- vcat [ text "inerts =" <+> ppr inert2
- , text "unsolved =" <+> ppr unsolved_flats ]
+ = do { traceTcS "solveWanteds: simpl_loop start {" $
+ vcat [ text "n =" <+> ppr n
+ , text "implics =" <+> ppr implics
+ , text "inert =" <+> ppr inert ]
+
+ ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
+ -- unsolved_cans contains either Wanted or Derived!
- -- See Note [Preparing inert set for implications]
- ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
; (implic_eqs, unsolved_implics)
- <- flatMapBagPairM (solveImplication inert_for_implics) implics
+ <- solveNestedImplications just_given_inert unsolved_cans 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
-
- ; if isEmptyBag final_eqs then
- return (unsolved_flats, unsolved_implics)
+ ; 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 "improve_eqs =" <+> ppr improve_eqs
+ , text "unsolved_flats =" <+> ppr unsolved_cans
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
+ ; (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
- 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) inert_with_improvement
+ -- Contain unsolved_cans and the improve_eqs
+ 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]
+ -- Push the unsolved wanteds inwards, but as givens
+
+ ; simpl_ctx <- getTcSContext
+
+ ; 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 ]
+
+ ; (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 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
-- 2. Maybe a unsolved implication, empty if entirely solved!
--
-- Precondition: everything is zonked by now
-solveImplication inert
- imp@(Implic { ic_env_tvs = untch
- , ic_binds = ev_binds
- , ic_skols = skols
- , ic_given = givens
+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 $
+ , ic_loc = loc })
+ = 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
+ ; 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 = mkWantedConstraints res_flat_bound 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]
- -> CanonicalCts -> (CanonicalCts, CanonicalCts)
-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
+ -> 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 wantders
+
+
+ where is_floatable :: FlavoredEvVar -> Bool
+ is_floatable (EvVarX cv _fl)
+ | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
+ is_floatable _flev = 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 [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
+ 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:
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.
+
+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):
+
+ (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.
+
+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 -> 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
+ = do { untch <- getUntouchables
+ ; let (unsolved_can_cts, (ni_subst, cv_binds))
+ = getSolvableCTyFunEqs untch cts
+ ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
+ , ppr ni_subst, ppr cv_binds
+ ])
+ ; 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 or Derived!
+ -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
+getSolvableCTyFunEqs untch cts
+ = 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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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 FlavoredEvVar) -- 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 :: 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
-- 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 (mkEvVarX ev (Wanted 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
+ -> TcsUntouchables -- 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 FlavoredEvVar)
-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) }
-
+ ; 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
+ ; 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 { 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 derived_eq) }
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
+ wanteds = map fst group
+ 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]
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
projects / ghc-hetmet.git / blobdiff