TcSimplify.lhs 40 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  21 22 import VarEnv ( varEnvElts )  simonpj@microsoft.com committed Sep 13, 2010 23 24 import Name import NameEnv ( emptyNameEnv )  simonmar committed Dec 10, 2003 25 import Bag  Simon Marlow committed Oct 11, 2006 26 27 import ListSetOps import Util  simonpj@microsoft.com committed Sep 13, 2010 28 29 30 31 32 33 import PrelInfo import PrelNames import Class ( classKey ) import BasicTypes ( RuleName ) import Data.List ( partition ) import Outputable  Ian Lynagh committed Mar 29, 2008 34 import FastString  partain committed Jan 08, 1996 35 36 37 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 38 39 40 41 42 ********************************************************************************* * * * External interface * * * *********************************************************************************  simonpj committed Jan 25, 2001 43   simonpj@microsoft.com committed Sep 13, 2010 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 \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 68   simonpj@microsoft.com committed Sep 13, 2010 69 70 71 72 73 74 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 75   simonpj@microsoft.com committed Sep 13, 2010 76 77 78 79 80 81 82 \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 83   qrczak committed Jul 17, 2001 84   simonpj@microsoft.com committed Sep 13, 2010 85 86 87 88 89 ********************************************************************************* * * * Deriving * * ***********************************************************************************  simonpj committed May 03, 2001 90   simonpj@microsoft.com committed Sep 13, 2010 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 120 121 \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 122   simonpj@microsoft.com committed Sep 13, 2010 123 124 125 126 127 128 129 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 130   simonpj@microsoft.com committed Sep 13, 2010 131 132 133 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 134   simonpj@microsoft.com committed Sep 13, 2010 135 136 Notice that this instance (just) satisfies the Paterson termination conditions. Then we *could* derive an instance decl like this:  simonpj committed Feb 10, 2004 137   simonpj@microsoft.com committed Sep 13, 2010 138 139 140 141  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 142   simonpj@microsoft.com committed Sep 13, 2010 143 144 145 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 146   simonpj@microsoft.com committed Sep 13, 2010 147 148 So for now we simply require that the derived instance context should have only type-variable constraints.  simonpj committed Feb 10, 2004 149   simonpj@microsoft.com committed Sep 13, 2010 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 177 178 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 179   simonpj@microsoft.com committed Sep 13, 2010 180 181 182 183 184 185 186 187 188 189 \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 190  = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs  simonpj@microsoft.com committed Sep 13, 2010 191 192 193  ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs minusVarSet gbl_tvs)) ; return (qtvs, [], emptyTcEvBinds) }  simonpj committed Feb 10, 2004 194   simonpj@microsoft.com committed Sep 13, 2010 195 196 197 198 199 200 201 202  | 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 ]  simonpj@microsoft.com committed Oct 08, 2010 203 204 205 206 207 208  -- Make a guess at the quantified type variables -- Then split the constraints on the baisis of those tyvars -- to avoid unnecessarily simplifying a class constraint -- See Note [Avoid unecessary constraint simplification] ; gbl_tvs <- tcGetGlobalTyVars ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs  simonpj@microsoft.com committed Oct 08, 2010 209 210  ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted$ zonked_tau_tvs minusVarSet gbl_tvs  simonpj@microsoft.com committed Oct 08, 2010 211 212  (perhaps_bound, surely_free) = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted  213   simonpj@microsoft.com committed Oct 08, 2010 214  ; emitConstraints surely_free  215 216 217 218  ; traceTc "sinf" $vcat [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound , ptext (sLit "surely_free =") <+> ppr surely_free ]  simonpj@microsoft.com committed Oct 08, 2010 219 220 221 222  -- Now simplify the possibly-bound constraints ; (simplified_perhaps_bound, tc_binds) <- simplifyAsMuchAsPossible SimplInfer perhaps_bound  simonpj@microsoft.com committed Sep 13, 2010 223   simonpj@microsoft.com committed Oct 08, 2010 224 225  -- Sigh: must re-zonk because because simplifyAsMuchAsPossible -- may have done some unification  simonpj@microsoft.com committed Sep 13, 2010 226  ; gbl_tvs <- tcGetGlobalTyVars  simonpj@microsoft.com committed Oct 06, 2010 227  ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs  simonpj@microsoft.com committed Oct 08, 2010 228  ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound  simonpj@microsoft.com committed Oct 08, 2010 229 230 231 232 233 234 235  ; let init_tvs = zonked_tau_tvs minusVarSet gbl_tvs mr_qtvs = init_tvs minusVarSet constrained_tvs constrained_tvs = tyVarsOfWantedEvVars zonked_simples qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs (final_qtvs, (bound, free)) | apply_mr = (mr_qtvs, (emptyBag, zonked_simples)) | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)  simonpj@microsoft.com committed Sep 13, 2010 236 237 238 239  ; traceTc "end simplifyInfer }"$ vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr , text "wanted = " <+> ppr zonked_wanted  simonpj@microsoft.com committed Oct 08, 2010 240  , text "qtvs = " <+> ppr final_qtvs  simonpj@microsoft.com committed Sep 13, 2010 241 242 243 244 245  , text "free = " <+> ppr free , text "bound = " <+> ppr bound ] -- Turn the quantified meta-type variables into real type variables ; emitConstraints (mapBag WcEvVar free)  simonpj@microsoft.com committed Oct 08, 2010 246  ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)  simonpj@microsoft.com committed Sep 13, 2010 247 248 249 250 251 252 253 254 255  ; 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  simonpj@microsoft.com committed Oct 08, 2010 256  = do { let untch = NoUntouchables  simonpj@microsoft.com committed Sep 13, 2010 257 258 259 260 261 262 263 264  -- 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 265  ; reportUnsolved (emptyBag, unsolved_implics)  simonpj@microsoft.com committed Sep 13, 2010 266 267 268  ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats ; return (final_wanted_evvars, ev_binds) }  simonpj committed Feb 10, 2004 269   simonpj@microsoft.com committed Sep 13, 2010 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 309 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  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 335   simonpj@microsoft.com committed Sep 13, 2010 336 \begin{code}  simonpj@microsoft.com committed Oct 08, 2010 337 338 339 340 341 342 343 344 345 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet growWanteds gbl_tvs ws tvs | isEmptyBag ws = tvs | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs growWantedEVs gbl_tvs ws tvs | isEmptyBag ws = tvs | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs  simonpj@microsoft.com committed Oct 19, 2010 346 growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet  simonpj@microsoft.com committed Oct 08, 2010 347 348 349 350 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet -- (growX gbls wanted tvs) grows a seed 'tvs' against the -- X-constraint 'wanted', nuking the 'gbls' at each stage  simonpj@microsoft.com committed Oct 19, 2010 351 352  growEvVar gbl_tvs ev tvs  simonpj@microsoft.com committed Oct 08, 2010 353  = tvs unionVarSet (ev_tvs minusVarSet gbl_tvs)  simonpj@microsoft.com committed Sep 13, 2010 354  where  simonpj@microsoft.com committed Oct 19, 2010 355 356 357  ev_tvs = growPredTyVars (evVarPred ev) tvs growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs  simonpj@microsoft.com committed Sep 13, 2010 358   simonpj@microsoft.com committed Oct 08, 2010 359 360 361 growWanted gbl_tvs (WcEvVar wev) tvs = growWantedEV gbl_tvs wev tvs growWanted gbl_tvs (WcImplic implic) tvs  simonpj@microsoft.com committed Oct 19, 2010 362 363 364 365 366 367  = foldrBag (growWanted inner_gbl_tvs) (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic)) -- Must grow over inner givens too (ic_wanted implic) where inner_gbl_tvs = gbl_tvs unionVarSet ic_skols implic  simonpj@microsoft.com committed Sep 13, 2010 368 369 370 371 372 373 374 375 376 377  -------------------- 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  simonpj@microsoft.com committed Oct 08, 2010 378 379  quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool  simonpj@microsoft.com committed Oct 19, 2010 380 -- False => we can *definitely* float the WantedConstraint out  simonpj@microsoft.com committed Oct 08, 2010 381 quantifyMeWC qtvs (WcImplic implic)  simonpj@microsoft.com committed Oct 19, 2010 382 383 384 385 386  = (tyVarsOfEvVars (ic_given implic) intersectsVarSet inner_qtvs) || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic) where inner_qtvs = qtvs minusVarSet ic_skols implic  simonpj@microsoft.com committed Oct 08, 2010 387 388 quantifyMeWC qtvs (WcEvVar wev) = quantifyMe qtvs wev  simonpj@microsoft.com committed Sep 13, 2010 389 \end{code}  simonpj committed Jan 25, 2001 390   simonpj@microsoft.com committed Oct 08, 2010 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 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.  simonpj@microsoft.com committed Nov 24, 2006 409 410 Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj committed May 03, 2001 411 412 413 Consider this: f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 414   simonpj committed May 03, 2001 415 416 417 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 418   simonpj committed May 03, 2001 419 420 421  f :: Int -> Int (so we get ?y from the context of f's definition), or  simonpj committed Jan 25, 2001 422 423 424  f :: (?y::Int) => Int -> Int  simonpj committed May 03, 2001 425 426 427 428 429 430 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 431 432 BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring.  simonpj committed Jun 25, 2001 433   simonpj committed Oct 25, 2001 434   simonpj@microsoft.com committed Sep 13, 2010 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 ********************************************************************************* * * * 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!!  464   simonpj committed Mar 09, 2005 465 \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 466 467 468 469 470 471 472 simplifySuperClass :: EvVar -- The "self" dictionary -> WantedConstraints -> TcM () simplifySuperClass self wanteds = do { wanteds <- mapBagM zonkWanted wanteds ; loc <- getCtLoc NoScSkol ; (unsolved, ev_binds)  simonpj@microsoft.com committed Oct 08, 2010 473  <- runTcS SimplCheck NoUntouchables$  simonpj@microsoft.com committed Sep 13, 2010 474  do { can_self <- canGivens loc [self]  dimitris@microsoft.com committed Oct 06, 2010 475  ; let inert = foldlBag updInertSet emptyInert can_self  simonpj@microsoft.com committed Sep 13, 2010 476 477 478 479 480 481  -- 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 482 483 484 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 485 486 487 488 489 ********************************************************************************* * * * RULES * * * ***********************************************************************************  simonpj committed May 12, 2004 490   simonpj@microsoft.com committed Sep 13, 2010 491 492 493 494 495 496 497 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 498   simonpj@microsoft.com committed Sep 13, 2010 499 500 501 Implementation: the TcSFlags carried by the TcSMonad controls the amount of simplification, so simplifyRuleLhs just sets the flag appropriately.  simonpj committed May 18, 1999 502   simonpj@microsoft.com committed May 19, 2006 503 504 505 506 507 508 509 510 511 512 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 513   simonpj@microsoft.com committed May 19, 2006 514 Here is another example:  simonpj committed Feb 28, 2001 515 516  fromIntegral :: (Integral a, Num b) => a -> b {-# RULES "foo" fromIntegral = id :: Int -> Int #-}  simonpj@microsoft.com committed May 19, 2006 517 518 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 519  forall dIntegralInt.  simonpj@microsoft.com committed May 19, 2006 520  fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int  simonpj committed Mar 09, 2005 521 because the scsel will mess up RULE matching. Instead we want  simonpj committed Feb 28, 2001 522  forall dIntegralInt, dNumInt.  simonpj@microsoft.com committed May 19, 2006 523  fromIntegral Int Int dIntegralInt dNumInt = id Int  simonpj committed Feb 28, 2001 524   simonpj@microsoft.com committed May 19, 2006 525 526 527 528 529 530 531 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 532   simonpj@microsoft.com committed Sep 13, 2010 533 534 In short, simplifyRuleLhs must *only* squash equalities, leaving all dicts unchanged, with absolutely no sharing.  lewie committed Mar 02, 2000 535   simonpj@microsoft.com committed Sep 13, 2010 536 537 538 539 540 541 542 543 544 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 545 546  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 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 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 08, 2010 582  Implic { ic_untch = NoUntouchables  simonpj@microsoft.com committed Sep 13, 2010 583 584 585 586 587 588 589 590 591 592 593 594  , 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 595 596 597 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 598 599 600 601 602 ********************************************************************************* * * * Main Simplifier * * * ***********************************************************************************  lewie committed Mar 02, 2000 603 604  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 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 ])  simonpj@microsoft.com committed Oct 08, 2010 626  ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables$  simonpj@microsoft.com committed Sep 13, 2010 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650  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  651  ; bb <- getTcEvBindsBag  simonpj@microsoft.com committed Sep 13, 2010 652 653 654  ; traceTcS "solveWanteds }"$ vcat [ text "wanteds =" <+> ppr wanteds , text "unsolved_flats =" <+> ppr unsolved_flats  655 656 657  , text "unsolved_implics =" <+> ppr unsolved_implics , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) ]  simonpj@microsoft.com committed Sep 13, 2010 658  ; return (unsolved_flats, unsolved_implics) }  simonpj@microsoft.com committed Nov 10, 2006 659  where  simonpj@microsoft.com committed Sep 13, 2010 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 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  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 715 716 717 718  imp@(Implic { ic_untch = untch , ic_binds = ev_binds , ic_skols = skols , ic_given = givens  simonpj@microsoft.com committed Sep 13, 2010 719  , ic_wanted = wanteds  simonpj@microsoft.com committed Oct 06, 2010 720  , ic_loc = loc })  simonpj@microsoft.com committed Sep 13, 2010 721  = nestImplicTcS ev_binds untch$  simonpj@microsoft.com committed Oct 19, 2010 722 723 724 725  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  simonpj@microsoft.com committed Sep 13, 2010 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752  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 753  | otherwise = partitionBag is_floatable wanteds  simonpj committed Jan 25, 2001 754  where  simonpj@microsoft.com committed Sep 13, 2010 755 756 757 758 759  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 760 \end{code}  partain committed Jan 08, 1996 761   simonpj@microsoft.com committed Sep 13, 2010 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 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:  790   simonpj@microsoft.com committed Sep 13, 2010 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816  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 817   simonm committed Jan 08, 1998 818 819  \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 820 821 822 823 824 825 826 827 828 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 829  | otherwise  simonpj@microsoft.com committed Oct 08, 2010 830  = do { untch <- getUntouchables  simonpj@microsoft.com committed Sep 13, 2010 831  ; tv_cts <- mapM (defaultTyVar untch) $ 832  varSetElems (tyVarsOfCDicts wanteds)  simonpj@microsoft.com committed Sep 13, 2010 833 834 835  ; info@(_, default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info untch wanteds  simonpj@microsoft.com committed Oct 08, 2010 836  ; deflt_cts <- mapM (disambigGroup default_tys inert) groups  simonpj@microsoft.com committed Sep 13, 2010 837 838 839 840 841 842 843  ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts , text "Type defaults =" <+> ppr deflt_cts]) ; return (unionManyBags deflt_cts andCCan unionManyBags tv_cts) } ------------------  simonpj@microsoft.com committed Oct 08, 2010 844 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts  simonpj@microsoft.com committed Sep 13, 2010 845 846 847 848 849 850 851 852 -- 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 853 --  simonpj@microsoft.com committed Sep 13, 2010 854 855 856 857 858 859 -- 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  860  | isTouchableMetaTyVar_InRange untch the_tv  simonpj@microsoft.com committed Sep 13, 2010 861  , not (k eqKind default_k)  862  = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k  simonpj@microsoft.com committed Sep 17, 2010 863 864  ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk -- 'DefaultOrigin' is strictly the declaration, but it's convenient  simonpj@microsoft.com committed Sep 13, 2010 865 866 867 868 869 870 871 872  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 873  where  simonpj@microsoft.com committed Sep 13, 2010 874 875 876 877 878 879 880 881 882  k = tyVarKind the_tv default_k = defaultKind k ---------------- findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules)  simonpj@microsoft.com committed Oct 08, 2010 883  -> Untouchables -- Untouchable  simonpj@microsoft.com committed Sep 13, 2010 884 885 886 887 888 889 890  -> 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 891  where  simonpj@microsoft.com committed Sep 13, 2010 892  unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints  simonpj@microsoft.com committed Sep 13, 2010 893  non_unaries :: [CanonicalCt] -- and *other* constraints  simonpj@microsoft.com committed Sep 13, 2010 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909  (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)  910  && isTouchableMetaTyVar_InRange untch tv  simonpj@microsoft.com committed Sep 13, 2010 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936  && 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 -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable -> TcS CanonicalCts  simonpj@microsoft.com committed Oct 08, 2010 937 disambigGroup [] _inert _grp  simonpj@microsoft.com committed Sep 13, 2010 938  = return emptyBag  simonpj@microsoft.com committed Oct 08, 2010 939 disambigGroup (default_ty:default_tys) inert group  simonpj@microsoft.com committed Sep 13, 2010 940 941 942 943 944 945 946 947 948  = 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 }  simonpj@microsoft.com committed Oct 08, 2010 949  ; success <- tryTcS$  simonpj@microsoft.com committed Sep 13, 2010 950 951 952 953 954 955 956 957 958 959 960 961 962  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)  simonpj@microsoft.com committed Oct 08, 2010 963  ; disambigGroup default_tys inert group } }  simonpj@microsoft.com committed Mar 15, 2007 964  where  simonpj@microsoft.com committed Sep 13, 2010 965 966 967  ((the_ct,the_tv):_) = group wanteds = map fst group wanted_ev_vars = map deCanonicaliseWanted wanteds  partain committed Mar 19, 1996 968 969 \end{code}  simonpj@microsoft.com committed Nov 10, 2006 970 971 972 973 974 975 976 977 978 979 980 981 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 982  ` simonpj committed Jan 25, 2001 983