TcSimplify.lhs 37 KB
 simonm committed Jan 08, 1998 1 \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 2 3 4 5 6 module TcSimplify( simplifyInfer, simplifySuperClass, simplifyDefault, simplifyDeriv, simplifyBracket, simplifyRule, simplifyTop, simplifyInteractive ) where  partain committed Jan 08, 1996 7   simonm committed Jan 08, 1998 8 #include "HsVersions.h"  partain committed Mar 19, 1996 9   simonpj@microsoft.com committed Sep 13, 2010 10 import HsSyn  simonpj committed Sep 13, 2002 11 import TcRnMonad  simonpj@microsoft.com committed Sep 13, 2010 12 13 import TcErrors import TcCanonical  simonpj@microsoft.com committed Jan 02, 2007 14 import TcMType  simonpj@microsoft.com committed Sep 13, 2010 15 16 17 18 import TcType import TcSMonad import TcInteract import Inst  Simon Marlow committed Oct 11, 2006 19 import Var  simonm committed Dec 02, 1998 20 import VarSet  simonpj@microsoft.com committed Sep 13, 2010 21 22 import Name import NameEnv ( emptyNameEnv )  simonmar committed Dec 10, 2003 23 import Bag  Simon Marlow committed Oct 11, 2006 24 25 import ListSetOps import Util  simonpj@microsoft.com committed Sep 13, 2010 26 27 28 29 30 31 import PrelInfo import PrelNames import Class ( classKey ) import BasicTypes ( RuleName ) import Data.List ( partition ) import Outputable  Ian Lynagh committed Mar 29, 2008 32 import FastString  partain committed Jan 08, 1996 33 34 35 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 36 37 38 39 40 ********************************************************************************* * * * External interface * * * *********************************************************************************  simonpj committed Jan 25, 2001 41   simonpj@microsoft.com committed Sep 13, 2010 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 \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 simplifyTop wanteds = simplifyCheck SimplCheck wanteds ------------------ simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind) simplifyInteractive wanteds = simplifyCheck SimplInteractive wanteds ------------------ 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 ; return () } \end{code}  simonpj committed Jan 25, 2001 66   simonpj@microsoft.com committed Sep 13, 2010 67 68 69 70 71 72 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.  simonpj committed Jan 25, 2001 73   simonpj@microsoft.com committed Sep 13, 2010 74 75 76 77 78 79 80 \begin{code} simplifyBracket :: WantedConstraints -> TcM () simplifyBracket wanteds = do { zonked_wanteds <- mapBagM zonkWanted wanteds ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds ; return () } \end{code}  simonpj committed May 03, 2001 81   qrczak committed Jul 17, 2001 82   simonpj@microsoft.com committed Sep 13, 2010 83 84 85 86 87 ********************************************************************************* * * * Deriving * * ***********************************************************************************  simonpj committed May 03, 2001 88   simonpj@microsoft.com committed Sep 13, 2010 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 \begin{code} simplifyDeriv :: CtOrigin -> [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 ; 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] ; traceTc "simlifyDeriv" (ppr tvs $$ppr theta$$ ppr wanted) ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag ; let (good, bad) = partition validDerivPred$ foldrBag ((:) . wantedEvVarPred) [] unsolved -- See Note [Exotic derived instance contexts] subst_skol = zipTopTvSubst tvs_skols $map mkTyVarTy tvs ; reportUnsolvedDeriv bad loc ; return$ substTheta subst_skol good } \end{code}  simonpj committed May 03, 2001 120   simonpj@microsoft.com committed Sep 13, 2010 121 122 123 124 125 126 127 Note [Exotic derived instance contexts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In a 'derived' instance declaration, we *infer* the context. It's a bit unclear what rules we should apply for this; the Haskell report is silent. Obviously, constraints like (Eq a) are fine, but what about data T f a = MkT (f a) deriving( Eq ) where we'd get an Eq (f a) constraint. That's probably fine too.  simonpj committed May 03, 2001 128   simonpj@microsoft.com committed Sep 13, 2010 129 130 131 One could go further: consider data T a b c = MkT (Foo a b c) deriving( Eq ) instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)  simonpj committed Feb 10, 2004 132   simonpj@microsoft.com committed Sep 13, 2010 133 134 Notice that this instance (just) satisfies the Paterson termination conditions. Then we *could* derive an instance decl like this:  simonpj committed Feb 10, 2004 135   simonpj@microsoft.com committed Sep 13, 2010 136 137 138 139  instance (C Int a, Eq b, Eq c) => Eq (T a b c) even though there is no instance for (C Int a), because there just *might* be an instance for, say, (C Int Bool) at a site where we need the equality instance for T's.  simonpj committed Feb 10, 2004 140   simonpj@microsoft.com committed Sep 13, 2010 141 142 143 However, this seems pretty exotic, and it's quite tricky to allow this, and yet give sensible error messages in the (much more common) case where we really want that instance decl for C.  simonpj committed Feb 10, 2004 144   simonpj@microsoft.com committed Sep 13, 2010 145 146 So for now we simply require that the derived instance context should have only type-variable constraints.  simonpj committed Feb 10, 2004 147   simonpj@microsoft.com committed Sep 13, 2010 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 Here is another example: data Fix f = In (f (Fix f)) deriving( Eq ) Here, if we are prepared to allow -XUndecidableInstances we could derive the instance instance Eq (f (Fix f)) => Eq (Fix f) but this is so delicate that I don't think it should happen inside 'deriving'. If you want this, write it yourself! NB: if you want to lift this condition, make sure you still meet the termination conditions! If not, the deriving mechanism generates larger and larger constraints. Example: data Succ a = S a data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show Note the lack of a Show instance for Succ. First we'll generate instance (Show (Succ a), Show a) => Show (Seq a) and then instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) and so on. Instead we want to complain of no instance for (Show (Succ a)). The bottom line ~~~~~~~~~~~~~~~ Allow constraints which consist only of type variables, with no repeats. ********************************************************************************* * * * Inference * * ***********************************************************************************  simonpj committed Feb 10, 2004 177   simonpj@microsoft.com committed Sep 13, 2010 178 179 180 181 182 183 184 185 186 187 \begin{code} simplifyInfer :: Bool -- Apply monomorphism restriction -> TcTyVarSet -- These type variables are free in the -- types to be generalised -> 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  simonpj@microsoft.com committed Oct 06, 2010 188  = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs  simonpj@microsoft.com committed Sep 13, 2010 189 190 191  ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs minusVarSet gbl_tvs)) ; return (qtvs, [], emptyTcEvBinds) }  simonpj committed Feb 10, 2004 192   simonpj@microsoft.com committed Sep 13, 2010 193 194 195 196 197 198 199 200 201 202 203 204  | otherwise = do { zonked_wanted <- mapBagM zonkWanted wanted ; traceTc "simplifyInfer {" $vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr , ptext (sLit "wanted =") <+> ppr zonked_wanted , ptext (sLit "tau_tvs =") <+> ppr tau_tvs ] ; (simple_wanted, tc_binds) <- simplifyAsMuchAsPossible SimplInfer zonked_wanted ; gbl_tvs <- tcGetGlobalTyVars  simonpj@microsoft.com committed Oct 06, 2010 205  ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs  simonpj@microsoft.com committed Sep 13, 2010 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238  ; 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* ; ((unsolved_flats, unsolved_implics), ev_binds) <- runTcS ctxt untch$ simplifyApproxLoop 0 wanteds -- Report any errors  simonpj@microsoft.com committed Sep 19, 2010 239  ; reportUnsolved (emptyBag, unsolved_implics)  simonpj@microsoft.com committed Sep 13, 2010 240 241 242  ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats ; return (final_wanted_evvars, ev_binds) }  simonpj committed Feb 10, 2004 243   simonpj@microsoft.com committed Sep 13, 2010 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308  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 \end{code}  simonpj committed Feb 10, 2004 309   simonpj@microsoft.com committed Sep 13, 2010 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 \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 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 -------------------- quantifyMe :: TyVarSet -- Quantifying over these -> WantedEvVar -> Bool -- True <=> quantify over this wanted quantifyMe qtvs wev | isIPPred pred = True -- Note [Inheriting implicit parameters] | otherwise = tyVarsOfPred pred intersectsVarSet qtvs where pred = wantedEvVarPred wev \end{code}  simonpj committed Jan 25, 2001 341   simonpj@microsoft.com committed Nov 24, 2006 342 343 Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj committed May 03, 2001 344 345 346 Consider this: f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 347   simonpj committed May 03, 2001 348 349 350 where f is *not* a top-level binding. From the RHS of f we'll get the constraint (?y::Int). There are two types we might infer for f:  simonpj committed Jan 25, 2001 351   simonpj committed May 03, 2001 352 353 354  f :: Int -> Int (so we get ?y from the context of f's definition), or  simonpj committed Jan 25, 2001 355 356 357  f :: (?y::Int) => Int -> Int  simonpj committed May 03, 2001 358 359 360 361 362 363 At first you might think the first was better, becuase then ?y behaves like a free variable of the definition, rather than having to be passed at each call site. But of course, the WHOLE IDEA is that ?y should be passed at each call site (that's what dynamic binding means) so we'd better infer the second.  simonpj committed Oct 25, 2001 364 365 BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring.  simonpj committed Jun 25, 2001 366   simonpj committed Oct 25, 2001 367   simonpj@microsoft.com committed Sep 13, 2010 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 ********************************************************************************* * * * 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 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!!  397   simonpj committed Mar 09, 2005 398 \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 399 400 401 402 403 404 405 406 407 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]  dimitris@microsoft.com committed Oct 06, 2010 408  ; let inert = foldlBag updInertSet emptyInert can_self  simonpj@microsoft.com committed Sep 13, 2010 409 410 411 412 413 414  -- No need for solveInteract; we know it's inert ; solveWanteds inert wanteds } ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds ) reportUnsolved unsolved }  simonpj committed Mar 09, 2005 415 416 417 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 418 419 420 421 422 ********************************************************************************* * * * RULES * * * ***********************************************************************************  simonpj committed May 12, 2004 423   simonpj@microsoft.com committed Sep 13, 2010 424 425 426 427 428 429 430 Note [Simplifying RULE lhs constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ On the LHS of transformation rules we only simplify only equalitis, 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 applied.  simonpj committed May 12, 2004 431   simonpj@microsoft.com committed Sep 13, 2010 432 433 434 Implementation: the TcSFlags carried by the TcSMonad controls the amount of simplification, so simplifyRuleLhs just sets the flag appropriately.  simonpj committed May 18, 1999 435   simonpj@microsoft.com committed May 19, 2006 436 437 438 439 440 441 442 443 444 445 Example. Consider the following left-hand side of a rule f (x == y) (y > z) = ... If we typecheck this expression we get constraints d1 :: Ord a, d2 :: Eq a We do NOT want to "simplify" to the LHS forall x::a, y::a, z::a, d1::Ord a. f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ... Instead we want forall x::a, y::a, z::a, d1::Ord a, d2::Eq a. f ((==) d2 x y) ((>) d1 y z) = ...  simonpj committed Jun 28, 1999 446   simonpj@microsoft.com committed May 19, 2006 447 Here is another example:  simonpj committed Feb 28, 2001 448 449  fromIntegral :: (Integral a, Num b) => a -> b {-# RULES "foo" fromIntegral = id :: Int -> Int #-}  simonpj@microsoft.com committed May 19, 2006 450 451 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont* want to get  simonpj committed Feb 28, 2001 452  forall dIntegralInt.  simonpj@microsoft.com committed May 19, 2006 453  fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int  simonpj committed Mar 09, 2005 454 because the scsel will mess up RULE matching. Instead we want  simonpj committed Feb 28, 2001 455  forall dIntegralInt, dNumInt.  simonpj@microsoft.com committed May 19, 2006 456  fromIntegral Int Int dIntegralInt dNumInt = id Int  simonpj committed Feb 28, 2001 457   simonpj@microsoft.com committed May 19, 2006 458 459 460 461 462 463 464 Even if we have g (x == y) (y == z) = .. where the two dictionaries are *identical*, we do NOT WANT forall x::a, y::a, z::a, d1::Eq a f ((==) d1 x y) ((>) d1 y z) = ... because that will only match if the dict args are (visibly) equal. Instead we want to quantify over the dictionaries separately.  simonpj committed May 18, 1999 465   simonpj@microsoft.com committed Sep 13, 2010 466 467 In short, simplifyRuleLhs must *only* squash equalities, leaving all dicts unchanged, with absolutely no sharing.  lewie committed Mar 02, 2000 468   simonpj@microsoft.com committed Sep 13, 2010 469 470 471 472 473 474 475 476 477 HOWEVER, under a nested implication things are different Consider f :: (forall a. Eq a => a->a) -> Bool -> ... {-# RULES "foo" forall (v::forall b. Eq b => b->b). f b True = ... #=} Here we *must* solve the wanted (Eq a) from the given (Eq a) resulting from skolemising the agument type of g. So we revert to SimplCheck when going under an implication.  simonpj committed Sep 13, 2002 478 479  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 simplifyRule :: RuleName -> [TcTyVar] -- Explicit skolems -> WantedConstraints -- Constraints from LHS -> WantedConstraints -- Constraints from RHS -> TcM ([EvVar], -- LHS dicts TcEvBinds, -- Evidence for LHS 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 -- 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 -- Notice that we simplify the RHS with only the explicitly -- introduced skolems, allowing the RHS to constrain any -- unification variables. -- Then, and only then, we call zonkQuantifiedTypeVariables -- Example foo :: Ord a => a -> a -- foo_spec :: Int -> Int -- {-# RULE "foo" foo = foo_spec #-} -- Here, it's the RHS that fixes the type variable -- So we don't want to make untouchable the type -- variables in the envt of the RHS, because they include -- the template variables of the RULE -- 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 $ simonpj@microsoft.com committed Oct 06, 2010 515  Implic { ic_untch = emptyVarSet -- No untouchables  simonpj@microsoft.com committed Sep 13, 2010 516 517 518 519 520 521 522 523 524 525 526 527  , 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 } ; rhs_binds2 <- readTcRef evb_ref ; return ( lhs_dicts , EvBinds lhs_binds , EvBinds (rhs_binds1 unionBags evBindMapBinds rhs_binds2)) }  simonpj committed Sep 13, 2002 528 529 530 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 531 532 533 534 535 ********************************************************************************* * * * Main Simplifier * * * ***********************************************************************************  lewie committed Mar 02, 2000 536 537  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 simplifyCheck :: SimplContext -> WantedConstraints -- Wanted -> TcM (Bag EvBind) -- Solve a single, top-level implication constraint -- e.g. typically one created from a top-level type signature -- f :: forall a. [a] -> [a] -- f x = rhs -- We do this even if the function has no polymorphism: -- g :: Int -> Int -- g y = rhs -- (whereas for *nested* bindings we would not create -- an implication constraint for g at all.) -- -- Fails if can't solve something in the input wanteds simplifyCheck ctxt wanteds = do { wanteds <- mapBagM zonkWanted wanteds ; traceTc "simplifyCheck {" (vcat [ ptext (sLit "wanted =") <+> ppr wanteds ]) ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet$ solveWanteds emptyInert wanteds ; traceTc "simplifyCheck }" $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 ; traceTcS "solveWanteds }"$ vcat [ text "wanteds =" <+> ppr wanteds , text "unsolved_flats =" <+> ppr unsolved_flats , text "unsolved_implics =" <+> ppr unsolved_implics ] ; return (unsolved_flats, unsolved_implics) }  simonpj@microsoft.com committed Nov 10, 2006 589  where  simonpj@microsoft.com committed Sep 13, 2010 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644  simpl_loop :: Int -> CanonicalCts -- May inlude givens (in the recursive call) -> Bag Implication -> TcS (CanonicalCts, Bag Implication) simpl_loop n can_ws implics | n>10 = trace "solveWanteds: loop" $-- Always bleat do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively ; return (can_ws, implics) } | otherwise = do { inert1 <- solveInteract inert can_ws ; let (inert2, unsolved_flats) = extractUnsolved inert1 ; traceTcS "solveWanteds/done flats"$ vcat [ text "inerts =" <+> ppr inert2 , text "unsolved =" <+> ppr unsolved_flats ] -- See Note [Preparing inert set for implications] ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats) ; (implic_eqs, unsolved_implics) <- flatMapBagPairM (solveImplication inert_for_implics) implics -- Apply defaulting rules if and only if there -- no floated equalities. If there are, they may -- solve the remaining wanteds, so don't do defaulting. ; final_eqs <- if not (isEmptyBag implic_eqs) then return implic_eqs else applyDefaultingRules inert2 unsolved_flats -- default_eqs are *givens*, so simpl_loop may -- recurse with givens in the argument ; if isEmptyBag final_eqs then return (unsolved_flats, unsolved_implics) else do { traceTcS ("solveWanteds iteration " ++ show n) $vcat [ text "floated_unsolved_eqs =" <+> ppr final_eqs , text "unsolved_implics = " <+> ppr unsolved_implics ] ; simpl_loop (n+1) (unsolved_flats unionBags final_eqs) unsolved_implics } } solveImplication :: InertSet -- Given -> Implication -- Wanted -> TcS (CanonicalCts, -- Unsolved unification var = type Bag Implication) -- Unsolved rest (always empty or singleton) -- 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  simonpj@microsoft.com committed Oct 06, 2010 645 646 647 648  imp@(Implic { ic_untch = untch , ic_binds = ev_binds , ic_skols = skols , ic_given = givens  simonpj@microsoft.com committed Sep 13, 2010 649  , ic_wanted = wanteds  simonpj@microsoft.com committed Oct 06, 2010 650  , ic_loc = loc })  simonpj@microsoft.com committed Sep 13, 2010 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678  = nestImplicTcS ev_binds untch$ do { traceTcS "solveImplication {" (ppr imp) -- Solve flat givens ; can_givens <- canGivens loc givens ; given_inert <- solveInteract inert can_givens -- Simplify the wanteds ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds ; let (res_flat_free, res_flat_bound) = floatEqualities skols givens unsolved_flats unsolved = mkWantedConstraints res_flat_bound unsolved_implics ; 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 ] ; let res_bag | isEmptyBag unsolved = emptyBag | otherwise = unitBag (imp { ic_wanted = unsolved }) ; return (res_flat_free, res_bag) } floatEqualities :: TcTyVarSet -> [EvVar] -> CanonicalCts -> (CanonicalCts, CanonicalCts) floatEqualities skols can_given wanteds | hasEqualities can_given = (emptyBag, wanteds)  simonpj@microsoft.com committed Sep 17, 2010 679  | otherwise = partitionBag is_floatable wanteds  simonpj committed Jan 25, 2001 680  where  simonpj@microsoft.com committed Sep 13, 2010 681 682 683 684 685  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  lewie committed Mar 02, 2000 686 \end{code}  partain committed Jan 08, 1996 687   simonpj@microsoft.com committed Sep 13, 2010 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 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 on unsolved-wanted error; adding it to the givens prevents any consequential errors from showing uop b) More importantly, in inference mode, we are going to quantify over this constraint, and we *don't* want to quantify over any constraints that are deducible from it. 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: Original inert set = (d :_g D a) /\ (co :_w a ~ [beta]) 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 ********************************************************************************* * * * Defaulting and disamgiguation * * * ********************************************************************************* Basic plan behind applyDefaulting rules:  716   simonpj@microsoft.com committed Sep 13, 2010 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742  Step 1: Split wanteds into defaultable groups, groups' and the rest rest_wanted' For each defaultable group, do: For each possible substitution for [alpha |-> tau] where alpha' is the group's variable, do: 1) Make up new TcEvBinds 2) Extend TcS with (groupVariable 3) given_inert <- solveOne inert (given : a ~ tau) 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints) 5) if unsolved == empty then sneakyUnify a |-> tau write the evidence bins return (final_inert ++ group_constraints,[]) -- will contain the info (alpha |-> tau)!! goto next defaultable group if unsolved <> empty then throw away evidence binds try next substitution If you've run out of substitutions for this group, too bad, you failed return (inert,group) goto next defaultable group Step 2: Collect all the (canonical-cts, wanteds) gathered this way. - Do a solveGiven over the canonical-cts to make sure they are inert ------------------------------------------------------------------------------------------  chak@cse.unsw.edu.au. committed Oct 01, 2008 743   simonm committed Jan 08, 1998 744 745  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 746 747 748 749 750 751 752 753 754 applyDefaultingRules :: InertSet -> CanonicalCts -- All wanteds -> TcS CanonicalCts -- Return some *extra* givens, which express the -- type-class-default choice applyDefaultingRules inert wanteds | isEmptyBag wanteds = return emptyBag  simonpj committed Dec 18, 1998 755  | otherwise  simonpj@microsoft.com committed Sep 13, 2010 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778  = do { untch <- getUntouchablesTcS ; tv_cts <- mapM (defaultTyVar untch)$ varSetElems (tyVarsOfCanonicals wanteds) ; info@(_, default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info untch wanteds ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts , text "Type defaults =" <+> ppr deflt_cts]) ; return (unionManyBags deflt_cts andCCan unionManyBags tv_cts) } ------------------ defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts -- defaultTyVar 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 -- instance Show (a->b) -- foo x = show (\_ -> True) -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), -- and that won't match the typeKind (*) in the instance decl. -- See test tc217.  chak@cse.unsw.edu.au. committed Sep 06, 2007 779 --  simonpj@microsoft.com committed Sep 13, 2010 780 781 782 783 784 785 786 787 788 789 -- We look only at touchable type variables. No further constraints -- are going to affect these type variables, so it's time to do it by -- hand. However we aren't ready to default them fully to () or -- whatever, because the type-class defaulting rules have yet to run. defaultTyVar untch the_tv | isMetaTyVar the_tv , not (the_tv elemVarSet untch) , not (k eqKind default_k) = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k  simonpj@microsoft.com committed Sep 17, 2010 790 791  ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk -- 'DefaultOrigin' is strictly the declaration, but it's convenient  simonpj@microsoft.com committed Sep 13, 2010 792 793 794 795 796 797 798 799  wanted_eq = CTyEqCan { cc_id = ev , cc_flavor = Wanted loc , cc_tyvar = the_tv , cc_rhs = better_ty } ; return (unitBag wanted_eq) } | otherwise = return emptyCCan -- The common case  chak@cse.unsw.edu.au. committed Sep 06, 2007 800  where  simonpj@microsoft.com committed Sep 13, 2010 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817  k = tyVarKind the_tv default_k = defaultKind k ---------------- findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules) -> TcTyVarSet -- Untouchable -> CanonicalCts -- Unsolved -> [[(CanonicalCt,TcTyVar)]] findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) untch wanteds | not (performDefaulting ctxt) = [] | null default_tys = [] | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)  simonpj committed Mar 09, 2005 818  where  simonpj@microsoft.com committed Sep 13, 2010 819  unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints  simonpj@microsoft.com committed Sep 13, 2010 820  non_unaries :: [CanonicalCt] -- and *other* constraints  simonpj@microsoft.com committed Sep 13, 2010 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891  (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds) -- Finds unary type-class constraints find_unary cc@(CDictCan { cc_tyargs = [ty] }) | Just tv <- tcGetTyVar_maybe ty = Left (cc, tv) find_unary cc = Right cc -- Non unary or non dictionary bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries cmp_tv (_,tv1) (_,tv2) = tv1 compare tv2 is_defaultable_group ds@((_,tv):_) = isTyConableTyVar tv -- Note [Avoiding spurious errors] && not (tv elemVarSet bad_tvs) && not (tv elemVarSet untch) -- Non untouchable && defaultable_classes [cc_class cc | (cc,_) <- ds] is_defaultable_group [] = panic "defaultable_group" defaultable_classes clss | extended_defaults = any isInteractiveClass clss | otherwise = all is_std_class clss && (any is_num_class clss) -- In interactive mode, or with -XExtendedDefaultRules, -- we default Show a to Show () to avoid graututious errors on "show []" isInteractiveClass cls = is_num_class cls || (classKey cls elem [showClassKey, eqClassKey, ordClassKey]) is_num_class cls = isNumericClass cls || (ovl_strings && (cls hasKey isStringClassKey)) -- is_num_class adds IsString to the standard numeric classes, -- when -foverloaded-strings is enabled is_std_class cls = isStandardClass cls || (ovl_strings && (cls hasKey isStringClassKey)) -- Similarly is_std_class ------------------------------ disambigGroup :: [Type] -- The default types -> TcTyVarSet -- Untouchables -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable -> TcS CanonicalCts disambigGroup [] _inert _untch _grp = return emptyBag disambigGroup (default_ty:default_tys) untch 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) } ; 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) } False -> -- Failure: try with the next type do { traceTcS "disambigGoup succeeded" (ppr default_ty) ; disambigGroup default_tys untch inert group } }  simonpj@microsoft.com committed Mar 15, 2007 892  where  simonpj@microsoft.com committed Sep 13, 2010 893 894 895  ((the_ct,the_tv):_) = group wanteds = map fst group wanted_ev_vars = map deCanonicaliseWanted wanteds  partain committed Mar 19, 1996 896 897 \end{code}  simonpj@microsoft.com committed Nov 10, 2006 898 899 900 901 902 903 904 905 906 907 908 909 Note [Avoiding spurious errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When doing the unification for defaulting, we check for skolem type variables, and simply don't default them. For example: f = (*) -- Monomorphic g :: Num a => a -> a g x = f x x Here, we get a complaint when checking the type signature for g, that g isn't polymorphic enough; but then we get another one when 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  partain committed Mar 19, 1996 910  ` simonpj committed Jan 25, 2001 911