TcSimplify.lhs 48.7 KB
 simonm committed Jan 08, 1998 1 \begin{code} Ian Lynagh committed Nov 04, 2011 2 3 4 5 6 7 8 {-# OPTIONS -fno-warn-tabs #-} -- The above warning supression flag is a temporary kludge. -- While working on this module you are encouraged to remove it and -- detab the module (please do the detabbing in a separate patch). See -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces -- for details simonpj@microsoft.com committed Sep 13, 2010 9 module TcSimplify( Simon Peyton Jones committed Jan 15, 2013 10 11 simplifyInfer, quantifyPred, simplifyAmbiguityCheck, Simon Peyton Jones committed Jan 08, 2013 12 simplifyDefault, Simon Peyton Jones committed Sep 03, 2012 13 14 simplifyRule, simplifyTop, simplifyInteractive, solveWantedsTcM simonpj@microsoft.com committed Sep 13, 2010 15 ) where partain committed Jan 08, 1996 16 simonm committed Jan 08, 1998 17 #include "HsVersions.h" partain committed Mar 19, 1996 18 Simon Peyton Jones committed Aug 28, 2012 19 import TcRnTypes simonpj committed Sep 13, 2002 20 import TcRnMonad simonpj@microsoft.com committed Sep 13, 2010 21 import TcErrors Simon Peyton Jones committed Dec 24, 2012 22 import TcMType as TcM simonpj@microsoft.com committed Sep 13, 2010 23 import TcType Simon Peyton Jones committed Dec 24, 2012 24 import TcSMonad as TcS dimitris committed Nov 16, 2011 25 import TcInteract simonpj@microsoft.com committed Sep 13, 2010 26 import Inst Simon Peyton Jones committed Jan 15, 2013 27 import FunDeps ( growThetaTyVars ) Simon Peyton Jones committed Aug 28, 2012 28 29 import Type ( classifyPredType, PredTree(..), getClassPredTys_maybe ) import Class ( Class ) Simon Marlow committed Oct 11, 2006 30 import Var dimitris committed Jun 08, 2012 31 import Unique simonm committed Dec 02, 1998 32 import VarSet simonpj@microsoft.com committed Nov 12, 2010 33 import VarEnv Simon Peyton Jones committed Dec 05, 2011 34 import TcEvidence simonpj@microsoft.com committed Sep 13, 2010 35 import Name simonmar committed Dec 10, 2003 36 import Bag Simon Marlow committed Oct 11, 2006 37 38 import ListSetOps import Util simonpj@microsoft.com committed Sep 13, 2010 39 40 41 import PrelInfo import PrelNames import Class ( classKey ) Simon Peyton Jones committed Aug 16, 2011 42 import BasicTypes ( RuleName ) simonpj@microsoft.com committed Sep 13, 2010 43 import Outputable Ian Lynagh committed Mar 29, 2008 44 import FastString dimitris committed Mar 28, 2012 45 import TrieMap () -- DV: for now partain committed Jan 08, 1996 46 47 48 \end{code} simonpj@microsoft.com committed Sep 13, 2010 49 50 51 52 53 ********************************************************************************* * * * External interface * * * ********************************************************************************* simonpj committed Jan 25, 2001 54 simonpj@microsoft.com committed Sep 13, 2010 55 56 57 \begin{code} simplifyTop :: WantedConstraints -> TcM (Bag EvBind) -- Simplify top-level constraints simonpj@microsoft.com committed Dec 13, 2010 58 59 60 -- 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 dimitris committed Sep 06, 2012 61 62 63 64 65 simplifyTop wanteds = do { traceTc "simplifyTop {" $text "wanted = " <+> ppr wanteds ; ev_binds_var <- newTcEvBinds ; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top ; binds1 <- TcRnMonad.getTcEvBinds ev_binds_var Simon Peyton Jones committed Sep 01, 2012 66 67 68 ; traceTc "End simplifyTop }" empty ; traceTc "reportUnsolved {" empty Simon Peyton Jones committed Sep 17, 2012 69 ; binds2 <- reportUnsolved zonked_final_wc Simon Peyton Jones committed Sep 01, 2012 70 ; traceTc "reportUnsolved }" empty dimitris committed Sep 06, 2012 71 Simon Peyton Jones committed Sep 01, 2012 72 ; return (binds1 unionBags binds2) } Simon Peyton Jones committed Aug 28, 2012 73 Simon Peyton Jones committed Sep 01, 2012 74 75 where -- See Note [Top-level Defaulting Plan] Simon Peyton Jones committed Sep 18, 2012 76 simpl_top :: WantedConstraints -> TcS WantedConstraints Simon Peyton Jones committed Sep 01, 2012 77 simpl_top wanteds dimitris committed Sep 06, 2012 78 = do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds) Simon Peyton Jones committed Dec 24, 2012 79 80 81 ; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go) ; let meta_tvs = filterVarSet isMetaTyVar free_tvs -- zonkTyVarsAndFV: the wc_first_go is not yet zonked Simon Peyton Jones committed Oct 15, 2012 82 83 84 -- filter isMetaTyVar: we might have runtime-skolems in GHCi, -- and we definitely don't want to try to assign to those! Simon Peyton Jones committed Dec 24, 2012 85 ; mapM_ defaultTyVar (varSetElems meta_tvs) -- Has unification side effects Simon Peyton Jones committed Sep 01, 2012 86 ; simpl_top_loop wc_first_go } dimitris committed Jun 08, 2012 87 Simon Peyton Jones committed Sep 01, 2012 88 simpl_top_loop wc Simon Peyton Jones committed Oct 04, 2012 89 90 91 | isEmptyWC wc || insolubleWC wc -- Don't do type-class defaulting if there are insolubles -- Doing so is not going to solve the insolubles Simon Peyton Jones committed Sep 01, 2012 92 93 = return wc | otherwise dimitris committed Sep 06, 2012 94 = do { wc_residual <- nestTcS (solve_wanteds_and_drop wc) Simon Peyton Jones committed Sep 01, 2012 95 96 97 98 99 100 101 ; let wc_flat_approximate = approximateWC wc_residual ; something_happened <- applyDefaultingRules wc_flat_approximate -- See Note [Top-level Defaulting Plan] ; if something_happened then simpl_top_loop wc_residual else return wc_residual } dimitris committed Jun 08, 2012 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 \end{code} Note [Top-level Defaulting Plan] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We have considered two design choices for where/when to apply defaulting. (i) Do it in SimplCheck mode only /whenever/ you try to solve some flat constraints, maybe deep inside the context of implications. This used to be the case in GHC 7.4.1. (ii) Do it in a tight loop at simplifyTop, once all other constraint has finished. This is the current story. Option (i) had many disadvantages: a) First it was deep inside the actual solver, b) Second it was dependent on the context (Infer a type signature, or Check a type signature, or Interactive) since we did not want to always start defaulting when inferring (though there is an exception to this see Note [Default while Inferring]) c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs: f :: Int -> Bool f x = const True (\y -> let w :: a -> a w a = const a (y+1) in w y) We will get an implication constraint (for beta the type of y): [untch=beta] forall a. 0 => Num beta which we really cannot default /while solving/ the implication, since beta is untouchable. Instead our new defaulting story is to pull defaulting out of the solver loop and go with option (i), implemented at SimplifyTop. Namely: - First have a go at solving the residual constraint of the whole program - Try to approximate it with a flat constraint - Figure out derived defaulting equations for that flat constraint - Go round the loop again if you did manage to get some equations Now, that has to do with class defaulting. However there exists type variable /kind/ defaulting. Again this is done at the top-level and the plan is: - At the top-level, once you had a go at solving the constraint, do figure out /all/ the touchable unification variables of the wanted contraints. - Apply defaulting to their kinds More details in Note [DefaultTyVar]. \begin{code} simonpj@microsoft.com committed Sep 13, 2010 146 Simon Peyton Jones committed Aug 16, 2011 147 148 149 ------------------ simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind) simplifyAmbiguityCheck name wanteds dimitris committed Jun 08, 2012 150 = traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >> Simon Peyton Jones committed Sep 03, 2012 151 simplifyTop wanteds -- NB: must be simplifyTop so that we 152 153 -- do ambiguity resolution. -- See Note [Impedence matching] in TcBinds. dimitris committed Nov 16, 2011 154 simonpj@microsoft.com committed Sep 13, 2010 155 156 157 ------------------ simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind) simplifyInteractive wanteds dimitris committed Jun 08, 2012 158 159 = traceTc "simplifyInteractive" empty >> simplifyTop wanteds simonpj@microsoft.com committed Sep 13, 2010 160 161 162 163 164 ------------------ simplifyDefault :: ThetaType -- Wanted; has no type variables in it -> TcM () -- Succeeds iff the constraint is soluble simplifyDefault theta dimitris committed Jun 08, 2012 165 166 = do { traceTc "simplifyInteractive" empty ; wanted <- newFlatWanteds DefaultOrigin theta Simon Peyton Jones committed Sep 03, 2012 167 168 169 170 ; (unsolved, _binds) <- solveWantedsTcM (mkFlatWC wanted) ; traceTc "reportUnsolved {" empty -- See Note [Deferring coercion errors to runtime] Simon Peyton Jones committed Sep 17, 2012 171 ; reportAllUnsolved unsolved dimitris committed Sep 06, 2012 172 173 174 -- Postcondition of solveWantedsTcM is that returned -- constraints are zonked. So Precondition of reportUnsolved -- is true. Simon Peyton Jones committed Sep 03, 2012 175 176 ; traceTc "reportUnsolved }" empty simonpj@microsoft.com committed Sep 13, 2010 177 178 ; return () } \end{code} simonpj committed Jan 25, 2001 179 simonpj committed May 03, 2001 180 simonpj@microsoft.com committed Sep 13, 2010 181 182 183 184 185 ********************************************************************************* * * * Inference * * *********************************************************************************** simonpj committed Feb 10, 2004 186 dreixel committed Nov 11, 2011 187 188 189 190 191 192 193 194 195 196 197 198 Note [Which variables to quantify] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose the inferred type of a function is T kappa (alpha:kappa) -> Int where alpha is a type unification variable and kappa is a kind unification variable Then we want to quantify over *both* alpha and kappa. But notice that kappa appears "at top level" of the type, as well as inside the kind of alpha. So it should be fine to just look for the "top level" kind/type variables of the type, without looking transitively into the kinds of those type variables. simonpj@microsoft.com committed Sep 13, 2010 199 \begin{code} Simon Peyton Jones committed Aug 16, 2011 200 simplifyInfer :: Bool simonpj@microsoft.com committed Jan 12, 2011 201 202 203 -> Bool -- Apply monomorphism restriction -> [(Name, TcTauType)] -- Variables to be generalised, -- and their tau-types Simon Peyton Jones committed Aug 29, 2012 204 -> WantedConstraints simonpj@microsoft.com committed Sep 13, 2010 205 206 -> TcM ([TcTyVar], -- Quantify over these type variables [EvVar], -- ... and these constraints Simon Peyton Jones committed Aug 16, 2011 207 208 209 Bool, -- The monomorphism restriction did something -- so the results type is not as general as -- it could be simonpj@microsoft.com committed Sep 13, 2010 210 TcEvBinds) -- ... binding these evidence variables Simon Peyton Jones committed Aug 29, 2012 211 simplifyInfer _top_lvl apply_mr name_taus wanteds simonpj@microsoft.com committed Jan 12, 2011 212 213 214 | isEmptyWC wanteds = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; zonked_taus <- zonkTcTypes (map snd name_taus) Simon Peyton Jones committed Feb 16, 2012 215 ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus minusVarSet gbl_tvs) dreixel committed Nov 11, 2011 216 217 218 -- tvs_to_quantify can contain both kind and type vars -- See Note [Which variables to quantify] ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify Simon Peyton Jones committed Aug 16, 2011 219 ; return (qtvs, [], False, emptyTcEvBinds) } simonpj committed Feb 10, 2004 220 simonpj@microsoft.com committed Sep 13, 2010 221 | otherwise Simon Peyton Jones committed Oct 15, 2012 222 223 = do { traceTc "simplifyInfer {"$ vcat [ ptext (sLit "binds =") <+> ppr name_taus Simon Peyton Jones committed Aug 16, 2011 224 225 , ptext (sLit "closed =") <+> ppr _top_lvl , ptext (sLit "apply_mr =") <+> ppr apply_mr dimitris committed Sep 06, 2012 226 , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds simonpj@microsoft.com committed Sep 13, 2010 227 228 ] Simon Peyton Jones committed Jun 21, 2012 229 230 231 232 233 -- Historical note: Before step 2 we used to have a -- HORRIBLE HACK described in Note [Avoid unecessary -- constraint simplification] but, as described in Trac -- #4361, we have taken in out now. That's why we start -- with step 2! simonpj@microsoft.com committed Jan 12, 2011 234 Simon Peyton Jones committed Jun 21, 2012 235 236 237 238 239 240 241 242 -- Step 2) First try full-blown solving -- NB: we must gather up all the bindings from doing -- this solving; hence (runTcSWithEvBinds ev_binds_var). -- And note that since there are nested implications, -- calling solveWanteds will side-effect their evidence -- bindings, so we can't just revert to the input -- constraint. Simon Peyton Jones committed Oct 15, 2012 243 244 ; ev_binds_var <- newTcEvBinds dimitris committed Sep 06, 2012 245 246 247 ; wanted_transformed <- solveWantedsTcMWithEvBinds ev_binds_var wanteds $solve_wanteds_and_drop -- Post: wanted_transformed are zonked Simon Peyton Jones committed Jun 21, 2012 248 249 -- Step 4) Candidates for quantification are an approximation of wanted_transformed dimitris committed Jun 08, 2012 250 251 252 -- NB: Already the fixpoint of any unifications that may have happened -- NB: We do not do any defaulting when inferring a type, this can lead -- to less polymorphic types, see Note [Default while Inferring] dimitris committed Jul 19, 2012 253 Simon Peyton Jones committed Jun 21, 2012 254 255 -- Step 5) Minimize the quantification candidates -- Step 6) Final candidates for quantification Simon Peyton Jones committed Sep 01, 2012 256 -- We discard bindings, insolubles etc, because all we are dimitris committed Sep 06, 2012 257 258 -- care aout it Simon Peyton Jones committed Oct 15, 2012 259 260 261 262 263 264 265 266 267 268 269 270 271 ; tc_lcl_env <- TcRnMonad.getLclEnv ; let untch = tcl_untch tc_lcl_env ; quant_pred_candidates <- if insolubleWC wanted_transformed then return [] -- See Note [Quantification with errors] else do { gbl_tvs <- tcGetGlobalTyVars ; let quant_cand = approximateWC wanted_transformed meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand)) ; ((flats, _insols), _extra_binds) <- runTcS$ do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs ; _implics <- solveInteract quant_cand ; getInertUnsolved } ; return (map ctPred $filter isWantedCt (bagToList flats)) } Simon Peyton Jones committed Sep 17, 2012 272 273 274 275 276 -- NB: Dimitrios is slightly worried that we will get -- family equalities (F Int ~ alpha) in the quantification -- candidates, as we have performed no further unflattening -- at this point. Nothing bad, but inferred contexts might -- look complicated. Simon Peyton Jones committed Sep 01, 2012 277 Simon Peyton Jones committed Oct 15, 2012 278 279 280 -- NB: quant_pred_candidates is already the fixpoint of any -- unifications that may have happened ; gbl_tvs <- tcGetGlobalTyVars Simon Peyton Jones committed Dec 24, 2012 281 ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus)) 282 ; let init_tvs = zonked_tau_tvs minusVarSet gbl_tvs Simon Peyton Jones committed Sep 01, 2012 283 poly_qtvs = growThetaTyVars quant_pred_candidates init_tvs 284 minusVarSet gbl_tvs Simon Peyton Jones committed Sep 01, 2012 285 pbound = filter (quantifyPred poly_qtvs) quant_pred_candidates dimitris committed Jun 08, 2012 286 Simon Peyton Jones committed Aug 16, 2011 287 -- Monomorphism restriction Simon Peyton Jones committed Sep 01, 2012 288 289 mr_qtvs = init_tvs minusVarSet constrained_tvs constrained_tvs = tyVarsOfTypes quant_pred_candidates 290 mr_bites = apply_mr && not (null pbound) Simon Peyton Jones committed Aug 16, 2011 291 Simon Peyton Jones committed Sep 01, 2012 292 293 (qtvs, bound) | mr_bites = (mr_qtvs, []) | otherwise = (poly_qtvs, pbound) dimitris committed Jun 08, 2012 294 Simon Peyton Jones committed Sep 01, 2012 295 296 297 298 299 300 301 ; traceTc "simplifyWithApprox"$ vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs , ptext (sLit "pbound =") <+> ppr pbound , ptext (sLit "init_qtvs =") <+> ppr init_tvs , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ] simonpj@microsoft.com committed Jan 12, 2011 302 303 ; if isEmptyVarSet qtvs && null bound Simon Peyton Jones committed Jul 14, 2012 304 305 306 307 then do { traceTc "} simplifyInfer/no quantification" empty ; emitConstraints wanted_transformed -- Includes insolubles (if -fdefer-type-errors) -- as well as flats and implications dimitris committed Jun 08, 2012 308 ; return ([], [], mr_bites, TcEvBinds ev_binds_var) } simonpj@microsoft.com committed Jan 12, 2011 309 310 else do dimitris committed Jun 08, 2012 311 312 313 { traceTc "simplifyApprox" $ptext (sLit "bound are =") <+> ppr bound simonpj@microsoft.com committed Jan 12, 2011 314 -- Step 4, zonk quantified variables 315 ; let minimal_flat_preds = mkMinimalBySCs bound Simon Peyton Jones committed Aug 16, 2011 316 317 skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty) | (name, ty) <- name_taus ] simonpj@microsoft.com committed Jan 12, 2011 318 319 320 321 -- Don't add the quantified variables here, because -- they are also bound in ic_skols and we want them to be -- tidied uniformly Simon Peyton Jones committed Feb 16, 2012 322 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs) simonpj@microsoft.com committed Jan 12, 2011 323 Simon Peyton Jones committed Jun 21, 2012 324 -- Step 7) Emit an implication Simon Peyton Jones committed Dec 24, 2012 325 ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds Simon Peyton Jones committed Oct 15, 2012 326 ; let implic = Implic { ic_untch = pushUntouchables untch Simon Peyton Jones committed Jan 12, 2012 327 , ic_skols = qtvs_to_return Simon Peyton Jones committed Aug 28, 2012 328 329 , ic_fsks = [] -- wanted_tansformed arose only from solveWanteds -- hence no flatten-skolems (which come from givens) simonpj@microsoft.com committed Jan 12, 2011 330 , ic_given = minimal_bound_ev_vars dimitris committed Jun 08, 2012 331 , ic_wanted = wanted_transformed simonpj@microsoft.com committed Jan 12, 2011 332 333 , ic_insol = False , ic_binds = ev_binds_var Simon Peyton Jones committed Sep 17, 2012 334 , ic_info = skol_info Simon Peyton Jones committed Oct 15, 2012 335 , ic_env = tc_lcl_env } simonpj@microsoft.com committed Jan 12, 2011 336 ; emitImplication implic dimitris committed Jun 08, 2012 337 simonpj@microsoft.com committed Jan 12, 2011 338 339 340 ; traceTc "} simplifyInfer/produced residual implication for quantification"$ vcat [ ptext (sLit "implic =") <+> ppr implic -- ic_skols, ic_given give rest of result Simon Peyton Jones committed Aug 16, 2011 341 , ptext (sLit "qtvs =") <+> ppr qtvs_to_return Simon Peyton Jones committed Sep 01, 2012 342 , ptext (sLit "spb =") <+> ppr quant_pred_candidates simonpj@microsoft.com committed Jan 12, 2011 343 344 , ptext (sLit "bound =") <+> ppr bound ] Simon Peyton Jones committed Aug 16, 2011 345 346 ; return ( qtvs_to_return, minimal_bound_ev_vars , mr_bites, TcEvBinds ev_binds_var) } } Simon Peyton Jones committed Jan 15, 2013 347 348 349 350 351 352 quantifyPred :: TyVarSet -- Quantifying over these -> PredType -> Bool -- True <=> quantify over this wanted quantifyPred qtvs pred | isIPPred pred = True -- Note [Inheriting implicit parameters] | otherwise = tyVarsOfType pred intersectsVarSet qtvs simonpj@microsoft.com committed Jan 12, 2011 353 \end{code} simonpj@microsoft.com committed Sep 13, 2010 354 Simon Peyton Jones committed Jan 15, 2013 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y 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: f :: Int -> Int (so we get ?y from the context of f's definition), or f :: (?y::Int) => Int -> Int 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. BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring. Simon Peyton Jones committed Sep 17, 2012 380 381 382 383 384 385 386 387 388 Note [Quantification with errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If we find that the RHS of the definition has some absolutely-insoluble constraints, we abandon all attempts to find a context to quantify over, and instead make the function fully-polymorphic in whatever type we have found. For two reasons a) Minimise downstream errors b) Avoid spurious errors from this function simonpj@microsoft.com committed Sep 13, 2010 389 390 391 Note [Default while Inferring] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ dimitris committed Jun 08, 2012 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 Our current plan is that defaulting only happens at simplifyTop and not simplifyInfer. This may lead to some insoluble deferred constraints Example: instance D g => C g Int b constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha type inferred = gamma -> gamma Now, if we try to default (alpha := Int) we will be able to refine the implication to (forall b. 0 => C gamma Int b) which can then be simplified further to (forall b. 0 => D gamma) Finally we /can/ approximate this implication with (D gamma) and infer the quantified type: forall g. D g => g -> g Instead what will currently happen is that we will get a quantified type (forall g. g -> g) and an implication: forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha which, even if the simplifyTop defaults (alpha := Int) we will still be left with an unsolvable implication: forall g. 0 => (forall b. 0 => D g) The concrete example would be: h :: C g a s => g -> a -> ST s a f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1) But it is quite tedious to do defaulting and resolve the implication constraints and we have not observed code breaking because of the lack of defaulting in inference so we don't do it for now. simonpj@microsoft.com committed Jan 12, 2011 426 427 428 429 430 431 432 433 434 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. simonpj@microsoft.com committed Sep 13, 2010 435 simonpj committed Jan 25, 2001 436 simonpj@microsoft.com committed Oct 08, 2010 437 438 Note [Avoid unecessary constraint simplification] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Simon Peyton Jones committed Jun 21, 2012 439 440 441 442 -------- NB NB NB (Jun 12) ------------- This note not longer applies; see the notes with Trac #4361. But I'm leaving it in here so we remember the issue.) ---------------------------------------- simonpj@microsoft.com committed Oct 08, 2010 443 When inferring the type of a let-binding, with simplifyInfer, Simon Peyton Jones committed Jun 21, 2012 444 try to avoid unnecessarily simplifying class constraints. simonpj@microsoft.com committed Oct 08, 2010 445 446 Doing so aids sharing, but it also helps with delicate situations like dimitris committed Jun 08, 2012 447 simonpj@microsoft.com committed Oct 08, 2010 448 instance C t => C [t] where .. dimitris committed Jun 08, 2012 449 simonpj@microsoft.com committed Oct 08, 2010 450 451 452 453 454 455 456 457 458 459 460 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 Sep 13, 2010 461 462 463 464 465 ********************************************************************************* * * * RULES * * * *********************************************************************************** simonpj committed May 12, 2004 466 Simon Peyton Jones committed Apr 16, 2012 467 See note [Simplifying RULE consraints] in TcRule simonpj committed Jun 28, 1999 468 Simon Peyton Jones committed Apr 16, 2012 469 470 471 472 473 474 475 476 477 478 479 480 481 482 Note [RULE quanfification over equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Decideing which equalities to quantify over is tricky: * We do not want to quantify over insoluble equalities (Int ~ Bool) (a) because we prefer to report a LHS type error (b) because if such things end up in 'givens' we get a bogus "inaccessible code" error * But we do want to quantify over things like (a ~ F b), where F is a type function. The difficulty is that it's hard to tell what is insoluble! So we see whether the simplificaiotn step yielded any type errors, and if so refrain from quantifying over *any* equalites. simonpj committed Sep 13, 2002 483 484 \begin{code} simonpj@microsoft.com committed Sep 13, 2010 485 486 487 simplifyRule :: RuleName -> WantedConstraints -- Constraints from LHS -> WantedConstraints -- Constraints from RHS Simon Peyton Jones committed Apr 16, 2012 488 489 490 -> TcM ([EvVar], WantedConstraints) -- LHS evidence varaibles -- See Note [Simplifying RULE constraints] in TcRule simplifyRule name lhs_wanted rhs_wanted Simon Peyton Jones committed Sep 03, 2012 491 = do { -- We allow ourselves to unify environment dimitris committed Jun 08, 2012 492 -- variables: runTcS runs with NoUntouchables Simon Peyton Jones committed Sep 03, 2012 493 (resid_wanted, _) <- solveWantedsTcM (lhs_wanted andWC rhs_wanted) dimitris committed Sep 06, 2012 494 -- Post: these are zonked and unflattened Simon Peyton Jones committed Apr 16, 2012 495 Simon Peyton Jones committed Sep 17, 2012 496 497 ; zonked_lhs_flats <- zonkCts (wc_flat lhs_wanted) ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_flats Simon Peyton Jones committed Apr 16, 2012 498 499 500 501 502 503 504 505 506 507 508 509 quantify_me -- Note [RULE quantification over equalities] | insolubleWC resid_wanted = quantify_insol | otherwise = quantify_normal quantify_insol ct = not (isEqPred (ctPred ct)) quantify_normal ct | EqPred t1 t2 <- classifyPredType (ctPred ct) = not (t1 eqType t2) | otherwise = True simonpj@microsoft.com committed Jan 12, 2011 510 ; traceTc "simplifyRule" $Simon Peyton Jones committed Sep 03, 2012 511 vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name) Simon Peyton Jones committed Sep 17, 2012 512 , text "zonked_lhs_flats" <+> ppr zonked_lhs_flats Simon Peyton Jones committed Apr 16, 2012 513 514 , text "q_cts" <+> ppr q_cts ] Simon Peyton Jones committed May 07, 2012 515 ; return ( map (ctEvId . ctEvidence) (bagToList q_cts) Simon Peyton Jones committed Sep 17, 2012 516 , lhs_wanted { wc_flat = non_q_cts }) } simonpj committed Sep 13, 2002 517 518 519 \end{code} simonpj@microsoft.com committed Sep 13, 2010 520 521 522 523 524 ********************************************************************************* * * * Main Simplifier * * * *********************************************************************************** lewie committed Mar 02, 2000 525 Simon Peyton Jones committed Jan 12, 2012 526 527 528 529 530 531 Note [Deferring coercion errors to runtime] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ While developing, sometimes it is desirable to allow compilation to succeed even if there are type errors in the code. Consider the following case: module Main where simonpj@microsoft.com committed Sep 13, 2010 532 Simon Peyton Jones committed Jan 12, 2012 533 534 a :: Int a = 'a' simonpj@microsoft.com committed Sep 13, 2010 535 Simon Peyton Jones committed Jan 12, 2012 536 main = print "b" simonpj@microsoft.com committed Sep 13, 2010 537 Simon Peyton Jones committed Jan 12, 2012 538 539 Even though a is ill-typed, it is not used in the end, so if all that we're interested in is main it is handy to be able to ignore the problems in a. simonpj@microsoft.com committed Sep 13, 2010 540 Simon Peyton Jones committed Jan 12, 2012 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 Since we treat type equalities as evidence, this is relatively simple. Whenever we run into a type mismatch in TcUnify, we normally just emit an error. But it is always safe to defer the mismatch to the main constraint solver. If we do that, a will get transformed into co :: Int ~ Char co = ... a :: Int a = 'a' cast co The constraint solver would realize that co is an insoluble constraint, and emit an error with reportUnsolved. But we can also replace the right-hand side of co with error "Deferred type error: Int ~ Char". This allows the program to compile, and it will run fine unless we evaluate a. This is what deferErrorsToRuntime does. It does this by keeping track of which errors correspond to which coercion in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors and does not fail if -fwarn-type-errors is on, so that we can continue compilation. The errors are turned into warnings in reportUnsolved. Simon Peyton Jones committed Sep 17, 2012 563 564 565 566 567 568 569 570 571 572 Note [Zonk after solving] ~~~~~~~~~~~~~~~~~~~~~~~~~ We zonk the result immediately after constraint solving, for two reasons: a) because zonkWC generates evidence, and this is the moment when we have a suitable evidence variable to hand. Note that *after* solving the constraints are typically small, so the overhead is not great. Simon Peyton Jones committed Jan 12, 2012 573 \begin{code} dimitris committed Sep 06, 2012 574 575 576 577 solveWantedsTcMWithEvBinds :: EvBindsVar -> WantedConstraints -> (WantedConstraints -> TcS WantedConstraints) -> TcM WantedConstraints Simon Peyton Jones committed Sep 17, 2012 578 579 580 581 582 583 -- Returns a *zonked* result -- We zonk when we finish primarily to un-flatten out any -- flatten-skolems etc introduced by canonicalisation of -- types involving type funuctions. Happily the result -- is typically much smaller than the input, indeed it is -- often empty. dimitris committed Sep 06, 2012 584 solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action Simon Peyton Jones committed Sep 17, 2012 585 586 = do { traceTc "solveWantedsTcMWithEvBinds"$ text "wanted=" <+> ppr wc ; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc) dimitris committed Sep 06, 2012 587 ; zonkWC ev_binds_var wc2 } Simon Peyton Jones committed Sep 17, 2012 588 -- See Note [Zonk after solving] dimitris committed Sep 06, 2012 589 Simon Peyton Jones committed Sep 01, 2012 590 solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind) Simon Peyton Jones committed Sep 03, 2012 591 -- Zonk the input constraints, and simplify them dimitris committed Jul 19, 2012 592 -- Return the evidence binds in the BagEvBinds result Simon Peyton Jones committed Aug 28, 2012 593 -- Discards all Derived stuff in result dimitris committed Sep 06, 2012 594 -- Postcondition: fully zonked and unflattened constraints Simon Peyton Jones committed Sep 03, 2012 595 solveWantedsTcM wanted dimitris committed Sep 06, 2012 596 597 598 = do { ev_binds_var <- newTcEvBinds ; wanteds' <- solveWantedsTcMWithEvBinds ev_binds_var wanted solve_wanteds_and_drop ; binds <- TcRnMonad.getTcEvBinds ev_binds_var Simon Peyton Jones committed Sep 03, 2012 599 ; return (wanteds', binds) } dimitris committed Jul 19, 2012 600 Simon Peyton Jones committed Sep 01, 2012 601 602 603 604 605 solve_wanteds_and_drop :: WantedConstraints -> TcS (WantedConstraints) -- Since solve_wanteds returns the residual WantedConstraints, -- it should alway be called within a runTcS or something similar, solve_wanteds_and_drop wanted = do { wc <- solve_wanteds wanted ; return (dropDerivedWC wc) } dimitris committed Jul 19, 2012 606 607 solve_wanteds :: WantedConstraints -> TcS WantedConstraints Simon Peyton Jones committed Sep 01, 2012 608 -- so that the inert set doesn't mindlessly propagate. dimitris committed Jul 19, 2012 609 -- NB: wc_flats may be wanted /or/ derived now dimitris committed Nov 16, 2011 610 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) simonpj@microsoft.com committed Jan 12, 2011 611 612 = do { traceTcS "solveWanteds {" (ppr wanted) dimitris committed Jul 19, 2012 613 -- Try the flat bit, including insolubles. Solving insolubles a Simon Peyton Jones committed Sep 28, 2012 614 -- second time round is a bit of a waste; but the code is simple Simon Peyton Jones committed Jul 23, 2012 615 616 617 -- and the program is wrong anyway, and we don't run the danger -- of adding Derived insolubles twice; see -- TcSMonad Note [Do not add duplicate derived insolubles] Simon Peyton Jones committed Aug 28, 2012 618 ; traceTcS "solveFlats {" empty Simon Peyton Jones committed Jul 23, 2012 619 ; let all_flats = flats unionBags insols Simon Peyton Jones committed Aug 28, 2012 620 621 ; impls_from_flats <- solveInteract all_flats ; traceTcS "solveFlats end }" (ppr impls_from_flats) simonpj@microsoft.com committed Jan 12, 2011 622 dimitris committed Nov 16, 2011 623 624 -- solve_wanteds iterates when it is able to float equalities -- out of one or more of the implications. dimitris committed Apr 10, 2012 625 ; unsolved_implics <- simpl_loop 1 (implics unionBags impls_from_flats) simonpj@microsoft.com committed Jan 12, 2011 626 Simon Peyton Jones committed Aug 28, 2012 627 628 ; (unsolved_flats, insoluble_flats) <- getInertUnsolved dimitris committed Sep 06, 2012 629 630 631 632 633 634 -- We used to unflatten here but now we only do it once at top-level -- during zonking -- see Note [Unflattening while zonking] in TcMType ; let wc = WC { wc_flat = unsolved_flats , wc_impl = unsolved_implics , wc_insol = insoluble_flats } dimitris committed Nov 16, 2011 635 ; bb <- getTcEvBindsMap simonpj@microsoft.com committed Nov 12, 2010 636 ; tb <- getTcSTyBindsMap simonpj@microsoft.com committed Sep 13, 2010 637 ; traceTcS "solveWanteds }" $simonpj@microsoft.com committed Nov 12, 2010 638 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats simonpj@microsoft.com committed Jan 12, 2011 639 , text "unsolved_implics =" <+> ppr unsolved_implics dimitris committed Nov 16, 2011 640 , text "current evbinds =" <+> ppr (evBindMapBinds bb) simonpj@microsoft.com committed Nov 12, 2010 641 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb)) Simon Peyton Jones committed Aug 28, 2012 642 , text "final wc =" <+> ppr wc ] Simon Peyton Jones committed Mar 02, 2012 643 Simon Peyton Jones committed Aug 28, 2012 644 ; return wc } dimitris committed Nov 16, 2011 645 646 647 648 649 650 651 652 simpl_loop :: Int -> Bag Implication -> TcS (Bag Implication) simpl_loop n implics | n > 10 = traceTcS "solveWanteds: loop!" empty >> return implics | otherwise Simon Peyton Jones committed Aug 28, 2012 653 654 655 656 657 658 659 = do { (floated_eqs, unsolved_implics) <- solveNestedImplications implics ; if isEmptyBag floated_eqs then return unsolved_implics else do { -- Put floated_eqs into the current inert set before looping impls_from_eqs <- solveInteract floated_eqs ; simpl_loop (n+1) (unsolved_implics unionBags impls_from_eqs)} } 660 dimitris committed Jul 19, 2012 661 dimitris committed Nov 16, 2011 662 663 664 665 666 667 668 669 670 solveNestedImplications :: Bag Implication -> TcS (Cts, Bag Implication) -- Precondition: the TcS inerts may contain unsolved flats which have -- to be converted to givens before we go inside a nested implication. solveNestedImplications implics | isEmptyBag implics = return (emptyBag, emptyBag) | otherwise = do { inerts <- getTcSInerts Simon Peyton Jones committed Aug 28, 2012 671 672 ; let thinner_inerts = prepareInertsForImplications inerts -- See Note [Preparing inert set for implications] dimitris committed Jul 19, 2012 673 Simon Peyton Jones committed Aug 28, 2012 674 ; traceTcS "solveNestedImplications starting {"$ dimitris committed Jul 19, 2012 675 vcat [ text "original inerts = " <+> ppr inerts dimitris committed Jun 08, 2012 676 677 , text "thinner_inerts = " <+> ppr thinner_inerts ] Simon Peyton Jones committed Aug 28, 2012 678 ; (floated_eqs, unsolved_implics) Simon Peyton Jones committed Aug 28, 2012 679 <- flatMapBagPairM (solveImplication thinner_inerts) implics dimitris committed Nov 16, 2011 680 681 682 683 -- ... and we are back in the original TcS inerts -- Notice that the original includes the _insoluble_flats so it was safe to ignore -- them in the beginning of this function. Simon Peyton Jones committed Aug 28, 2012 684 ; traceTcS "solveNestedImplications end }" $Simon Peyton Jones committed Aug 28, 2012 685 vcat [ text "all floated_eqs =" <+> ppr floated_eqs 686 687 , text "unsolved_implics =" <+> ppr unsolved_implics ] Simon Peyton Jones committed Aug 28, 2012 688 ; return (floated_eqs, unsolved_implics) } 689 Simon Peyton Jones committed Aug 28, 2012 690 solveImplication :: InertSet dimitris committed Nov 16, 2011 691 692 693 694 695 -> Implication -- Wanted -> TcS (Cts, -- All wanted or derived floated equalities: var = type Bag Implication) -- Unsolved rest (always empty or singleton) -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value Simon Peyton Jones committed Aug 28, 2012 696 solveImplication inerts dimitris committed Nov 16, 2011 697 imp@(Implic { ic_untch = untch simonpj@microsoft.com committed Oct 06, 2010 698 699 , ic_binds = ev_binds , ic_skols = skols Simon Peyton Jones committed Aug 28, 2012 700 , ic_fsks = old_fsks simonpj@microsoft.com committed Oct 06, 2010 701 , ic_given = givens simonpj@microsoft.com committed Sep 13, 2010 702 , ic_wanted = wanteds Simon Peyton Jones committed Sep 17, 2012 703 704 , ic_info = info , ic_env = env }) Simon Peyton Jones committed Jan 01, 2013 705 = do { traceTcS "solveImplication {" (ppr imp) simonpj@microsoft.com committed Sep 13, 2010 706 Simon Peyton Jones committed Aug 28, 2012 707 -- Solve the nested constraints Simon Peyton Jones committed Sep 01, 2012 708 709 710 -- NB: 'inerts' has empty inert_fsks ; (new_fsks, residual_wanted) <- nestImplicTcS ev_binds untch inerts$ Simon Peyton Jones committed Sep 17, 2012 711 do { solveInteractGiven (mkGivenLoc info env) old_fsks givens Simon Peyton Jones committed Sep 01, 2012 712 ; residual_wanted <- solve_wanteds wanteds Simon Peyton Jones committed Sep 17, 2012 713 714 715 -- solve_wanteds, *not* solve_wanteds_and_drop, because -- we want to retain derived equalities so we can float -- them out in floatEqualities Simon Peyton Jones committed Sep 01, 2012 716 717 718 719 720 721 722 ; more_fsks <- getFlattenSkols ; return (more_fsks ++ old_fsks, residual_wanted) } ; (floated_eqs, final_wanted) <- floatEqualities (skols ++ new_fsks) givens residual_wanted ; let res_implic | isEmptyWC final_wanted Simon Peyton Jones committed Aug 28, 2012 723 724 = emptyBag | otherwise Simon Peyton Jones committed Sep 01, 2012 725 726 727 = unitBag (imp { ic_fsks = new_fsks , ic_wanted = dropDerivedWC final_wanted , ic_insol = insolubleWC final_wanted }) simonpj@microsoft.com committed Sep 13, 2010 728 dimitris committed Nov 16, 2011 729 ; evbinds <- getTcEvBindsMap simonpj@microsoft.com committed Sep 13, 2010 730 ; traceTcS "solveImplication end }" $vcat Simon Peyton Jones committed Aug 28, 2012 731 [ text "floated_eqs =" <+> ppr floated_eqs Simon Peyton Jones committed Sep 01, 2012 732 , text "new_fsks =" <+> ppr new_fsks Simon Peyton Jones committed Aug 28, 2012 733 734 , text "res_implic =" <+> ppr res_implic , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ] simonpj@microsoft.com committed Sep 13, 2010 735 Simon Peyton Jones committed Aug 28, 2012 736 ; return (floated_eqs, res_implic) } dimitris committed Jul 19, 2012 737 738 739 740 \end{code} \begin{code} Simon Peyton Jones committed Sep 01, 2012 741 742 floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints -> TcS (Cts, WantedConstraints) simonpj@microsoft.com committed Jan 12, 2011 743 744 -- Post: The returned FlavoredEvVar's are only Wanted or Derived -- and come from the input wanted ev vars or deriveds Simon Peyton Jones committed Sep 01, 2012 745 746 -- Also performs some unifications, adding to monadically-carried ty_binds -- These will be used when processing floated_eqs later Simon Peyton Jones committed Aug 28, 2012 747 748 floatEqualities skols can_given wanteds@(WC { wc_flat = flats }) | hasEqualities can_given Simon Peyton Jones committed Sep 01, 2012 749 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications] Simon Peyton Jones committed Aug 28, 2012 750 | otherwise Simon Peyton Jones committed Sep 01, 2012 751 = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats Simon Peyton Jones committed Dec 24, 2012 752 ; untch <- TcS.getUntouchables Simon Peyton Jones committed Oct 15, 2012 753 ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs)) Simon Peyton Jones committed Sep 01, 2012 754 ; ty_binds <- getTcSTyBindsMap Simon Peyton Jones committed Sep 01, 2012 755 ; traceTcS "floatEqualities" (vcat [ text "Floated eqs =" <+> ppr float_eqs Simon Peyton Jones committed Sep 01, 2012 756 757 , text "Ty binds =" <+> ppr ty_binds]) ; return (float_eqs, wanteds { wc_flat = remaining_flats }) } Simon Peyton Jones committed Aug 28, 2012 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 where skol_set = growSkols wanteds (mkVarSet skols) is_floatable :: Ct -> Bool is_floatable ct = isEqPred pred && skol_set disjointVarSet tyVarsOfType pred where pred = ctPred ct growSkols :: WantedConstraints -> VarSet -> VarSet -- Find all the type variables that might possibly be unified -- with a type that mentions a skolem. This test is very conservative. -- I don't *think* we need look inside the implications, because any -- relevant unification variables in there are untouchable. growSkols (WC { wc_flat = flats }) skols = growThetaTyVars theta skols where theta = foldrBag ((:) . ctPred) [] flats Simon Peyton Jones committed Sep 01, 2012 776 Simon Peyton Jones committed Oct 15, 2012 777 778 779 780 781 promoteTyVar :: Untouchables -> TcTyVar -> TcS () -- When we float a constraint out of an implication we must restore -- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType promoteTyVar untch tv | isFloatedTouchableMetaTyVar untch tv Simon Peyton Jones committed Dec 24, 2012 782 = do { cloned_tv <- TcS.cloneMetaTyVar tv Simon Peyton Jones committed Oct 15, 2012 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch ; setWantedTyBind tv (mkTyVarTy rhs_tv) } | otherwise = return () promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS () -- See Note [Promote _and_ default when inferring] promoteAndDefaultTyVar untch gbl_tvs tv = do { tv1 <- if tv elemVarSet gbl_tvs then return tv else defaultTyVar tv ; promoteTyVar untch tv1 } defaultTyVar :: TcTyVar -> TcS TcTyVar -- Precondition: MetaTyVars only -- See Note [DefaultTyVar] defaultTyVar the_tv | not (k eqKind default_k) Simon Peyton Jones committed Dec 24, 2012 801 = do { tv' <- TcS.cloneMetaTyVar the_tv Simon Peyton Jones committed Oct 15, 2012 802 803 804 805 806 807 808 809 810 811 812 813 814 ; let new_tv = setTyVarKind tv' default_k ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv) ; setWantedTyBind the_tv (mkTyVarTy new_tv) ; return new_tv } -- Why not directly derived_pred = mkTcEqPred k default_k? -- See Note [DefaultTyVar] -- We keep the same Untouchables on tv' | otherwise = return the_tv -- The common case where k = tyVarKind the_tv default_k = defaultKind k Simon Peyton Jones committed Sep 01, 2012 815 816 approximateWC :: WantedConstraints -> Cts -- Postcondition: Wanted or Derived Cts Simon Peyton Jones committed Oct 15, 2012 817 818 approximateWC wc = float_wc emptyVarSet wc Simon Peyton Jones committed Sep 01, 2012 819 820 where float_wc :: TcTyVarSet -> WantedConstraints -> Cts Simon Peyton Jones committed Oct 15, 2012 821 822 823 float_wc skols (WC { wc_flat = flats, wc_impl = implics }) = do_bag (float_flat skols) flats unionBags do_bag (float_implic skols) implics Simon Peyton Jones committed Sep 01, 2012 824 825 826 float_implic :: TcTyVarSet -> Implication -> Cts float_implic skols imp 827 828 829 | hasEqualities (ic_given imp) -- Don't float out of equalities = emptyCts -- cf floatEqualities | otherwise -- See Note [approximateWC] Simon Peyton Jones committed Sep 01, 2012 830 831 832 833 834 835 836 837 838 839 840 841 842 = float_wc skols' (ic_wanted imp) where skols' = skols extendVarSetList ic_skols imp extendVarSetList ic_fsks imp float_flat :: TcTyVarSet -> Ct -> Cts float_flat skols ct | tyVarsOfCt ct disjointVarSet skols = singleCt ct | otherwise = emptyCts do_bag :: (a -> Bag c) -> Bag a -> Bag c do_bag f = foldrBag (unionBags.f) emptyBag \end{code} partain committed Jan 08, 1996 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 Note [ApproximateWC] ~~~~~~~~~~~~~~~~~~~~ approximateWC takes a constraint, typically arising from the RHS of a let-binding whose type we are *inferring*, and extracts from it some *flat* constraints that we might plausibly abstract over. Of course the top-level flat constraints are plausible, but we also float constraints out from inside, if the are not captured by skolems. However we do *not* float anything out if the implication binds equality constriants, because that defeats the OutsideIn story. Consider data T a where TInt :: T Int MkT :: T a f TInt = 3::Int We get the implication (a ~ Int => res ~ Int), where so far we've decided f :: T a -> res We don't want to float (res~Int) out because then we'll infer f :: T a -> Int which is only on of the possible types. (GHC 7.6 accidentally *did* float out of such implications, which meant it would happily infer non-principal types.) Simon Peyton Jones committed Oct 15, 2012 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 Note [DefaultTyVar] ~~~~~~~~~~~~~~~~~~~ defaultTyVar is used on any un-instantiated meta type variables to default the kind of OpenKind and ArgKind 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 kind ArgKind, and that won't match the typeKind (*) in the instance decl. See tests tc217 and tc175. 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. An important point is that if the type variable tv has kind k and the default is default_k we do not simply generate [D] (k ~ default_k) because: (1) k may be ArgKind and default_k may be * so we will fail (2) We need to rewrite all occurrences of the tv to be a type variable with the right kind and we choose to do this by rewriting the type variable /itself/ by a new variable which does have the right kind. Note [Promote _and_ default when inferring] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we are inferring a type, we simplify the constraint, and then use approximateWC to produce a list of candidate constraints. Then we MUST a) Promote any meta-tyvars that have been floated out by approximateWC, to restore invariant (MetaTvInv) described in Note [Untouchable type variables] in TcType. b) Default the kind of any meta-tyyvars that are not mentioned in in the environment. To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it should! If we don't solve the constraint, we'll stupidly quantify over (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332. simonpj@microsoft.com committed Feb 14, 2011 914 915 Note [Float Equalities out of Implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ dimitris committed Jun 08, 2012 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 For ordinary pattern matches (including existentials) we float equalities out of implications, for instance: data T where MkT :: Eq a => a -> T f x y = case x of MkT _ -> (y::Int) We get the implication constraint (x::T) (y::alpha): forall a. [untouchable=alpha] Eq a => alpha ~ Int We want to float out the equality into a scope where alpha is no longer untouchable, to solve the implication! But we cannot float equalities out of implications whose givens may yield or contain equalities: data T a where T1 :: T Int T2 :: T Bool T3 :: T a h :: T a -> a -> Int f x y = case x of T1 -> y::Int T2 -> y::Bool T3 -> h x y We generate constraint, for (x::T alpha) and (y :: beta): [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch (alpha ~ beta) -- From 3rd branch If we float the equality (beta ~ Int) outside of the first implication and the equality (beta ~ Bool) out of the second we get an insoluble constraint. But if we just leave them inside the implications we unify alpha := beta and solve everything. Principle: We do not want to float equalities out which may need the given *evidence* to become soluble. Consequence: classes with functional dependencies don't matter (since there is no evidence for a fundep equality), but equality superclasses do matter (since they carry evidence). Simon Peyton Jones committed Sep 17, 2012 959 960 961 962 963 964 965 966 967 Note [Promoting unification variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we float an equality out of an implication we must "promote" free unification variables of the equality, in order to maintain Invariant (MetaTvInv) from Note [Untouchable type variables] in TcType. for the leftover implication. This is absolutely necessary. Consider the following example. We start with two implications and a class with a functional dependency. dimitris committed Jun 08, 2012 968 Simon Peyton Jones committed Aug 28, 2012 969 970 971 972 973 class C x y | x -> y instance C [a] [a] (I1) [untch=beta]forall b. 0 => F Int ~ [beta] (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c] dimitris committed Jun 08, 2012 974 975 976 977 978 979 980 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. They may react to yield that (beta := [alpha]) which can then be pushed inwards the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs: Simon Peyton Jones committed Aug 28, 2012 981 982 983 984 985 986 987 988 989 990 991 992 993 class C x y | x -> y where op :: x -> y -> () instance C [a] [a] type family F a :: * h :: F Int -> () h = undefined data TEx where TEx :: a -> TEx dimitris committed Jun 08, 2012 994 Simon Peyton Jones committed Aug 28, 2012 995 996 997 998 999 1000 f (x::beta) = let g1 :: forall b. b -> () g1 _ = h [x] g2 z = case z of TEx y -> (h [[undefined]], op x [y]) in (g1 '3', g2 undefined) simonpj@microsoft.com committed Sep 13, 2010 1001 simonpj@microsoft.com committed Nov 12, 2010 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 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 dimitris committed Sep 06, 2012 1021 1022 of type family equations. See Inert Set invariants in TcInteract. Simon Peyton Jones committed Sep 17, 2012 1023 This solving is now happening during zonking, see Note [Unflattening while zonking] dimitris committed Sep 06, 2012 1024 in TcMType. simonpj@microsoft.com committed Nov 12, 2010 1025 1026 simonpj@microsoft.com committed Sep 13, 2010 1027 1028 1029 1030 1031 ********************************************************************************* * * * Defaulting and disamgiguation * * * ********************************************************************************* Simon Peyton Jones committed Oct 15, 2012 1032 simonm committed Jan 08, 1998 1033 \begin{code} Simon Peyton Jones committed Sep 01, 2012 1034 1035 1036 applyDefaultingRules :: Cts -> TcS Bool -- True <=> I did some defaulting, reflected in ty_binds dimitris committed Jul 19, 2012 1037 1038 -- Return some extra derived equalities, which express the -- type-class default choice. dimitris committed Nov 16, 2011 1039 applyDefaultingRules wanteds simonpj@microsoft.com committed Sep 13, 2010 1040 | isEmptyBag wanteds Simon Peyton Jones committed Sep 01, 2012 1041 = return False simonpj committed Dec 18, 1998 1042 | otherwise dimitris committed Nov 16, 2011 1043 1044 = do { traceTcS "applyDefaultingRules { "$ text "wanteds =" <+> ppr wanteds dimitris committed Jun 08, 2012 1045 1046 1047 ; info@(default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info wanteds dimitris committed Nov 16, 2011 1048 1049 ; traceTcS "findDefaultableGroups" \$ vcat [ text "groups=" <+> ppr groups , text "info=" <+> ppr info ] Simon Peyton Jones committed Sep 01, 2012 1050 ; something_happeneds <- mapM (disambigGroup default_tys) groups simonpj@microsoft.com committed Sep 13, 2010 1051 Simon Peyton Jones committed Sep 01, 2012 1052 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds) simonpj@microsoft.com committed Sep 13, 2010 1053 Simon Peyton Jones committed Sep 01, 2012 1054 ; return (or something_happeneds) } dimitris committed Nov 16, 2011 1055 1056 1057 1058 \end{code} dimitris committed Jun 08, 2012 1059 \begin{code} simonpj@microsoft.com committed Sep 13, 2010 1060 findDefaultableGroups dimitris committed Jun 08, 2012 1061 :: ( [Type] simonpj@microsoft.com committed Sep 13, 2010 1062 , (Bool,Bool) ) -- (Overloaded strings, extended default rules) dimitris committed Jul 19, 2012 1063 -> Cts -- Unsolved (wanted or derived) Simon Peyton Jones committed Aug 28, 2012 1064 -> [[(Ct,Class,TcTyVar)]] dimitris committed Jun 08, 2012 1065 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds simonpj@microsoft.com committed Sep 13, 2010 1066 1067 | null default_tys = [] | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries) simonpj committed Mar 09, 2005 1068 where Simon Peyton Jones committed Aug 28, 2012 1069 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints dimitris committed Nov 16, 2011 1070