1{-# LANGUAGE CPP #-} 2 3module TcSimplify( 4 simplifyInfer, InferMode(..), 5 growThetaTyVars, 6 simplifyAmbiguityCheck, 7 simplifyDefault, 8 simplifyTop, simplifyTopImplic, 9 simplifyInteractive, 10 solveEqualities, solveLocalEqualities, solveLocalEqualitiesX, 11 simplifyWantedsTcM, 12 tcCheckSatisfiability, 13 tcNormalise, 14 15 captureTopConstraints, 16 17 simpl_top, 18 19 promoteTyVar, 20 promoteTyVarSet, 21 22 -- For Rules we need these 23 solveWanteds, solveWantedsAndDrop, 24 approximateWC, runTcSDeriveds 25 ) where 26 27#include "HsVersions.h" 28 29import GhcPrelude 30 31import Bag 32import Class ( Class, classKey, classTyCon ) 33import DynFlags 34import GHC.Hs.Expr ( UnboundVar(..) ) 35import Id ( idType, mkLocalId ) 36import Inst 37import ListSetOps 38import Name 39import Outputable 40import PrelInfo 41import PrelNames 42import RdrName ( emptyGlobalRdrEnv ) 43import TcErrors 44import TcEvidence 45import TcInteract 46import TcCanonical ( makeSuperClasses, solveCallStack ) 47import TcMType as TcM 48import TcRnMonad as TcM 49import TcSMonad as TcS 50import Constraint 51import Predicate 52import TcOrigin 53import TcType 54import Type 55import TysWiredIn ( liftedRepTy ) 56import Unify ( tcMatchTyKi ) 57import Util 58import Var 59import VarSet 60import UniqSet 61import BasicTypes ( IntWithInf, intGtLimit ) 62import ErrUtils ( emptyMessages ) 63import qualified GHC.LanguageExtensions as LangExt 64 65import Control.Monad 66import Data.Foldable ( toList ) 67import Data.List ( partition ) 68import Data.List.NonEmpty ( NonEmpty(..) ) 69import Maybes ( isJust ) 70 71{- 72********************************************************************************* 73* * 74* External interface * 75* * 76********************************************************************************* 77-} 78 79captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) 80-- (captureTopConstraints m) runs m, and returns the type constraints it 81-- generates plus the constraints produced by static forms inside. 82-- If it fails with an exception, it reports any insolubles 83-- (out of scope variables) before doing so 84-- 85-- captureTopConstraints is used exclusively by TcRnDriver at the top 86-- level of a module. 87-- 88-- Importantly, if captureTopConstraints propagates an exception, it 89-- reports any insoluble constraints first, lest they be lost 90-- altogether. This is important, because solveLocalEqualities (maybe 91-- other things too) throws an exception without adding any error 92-- messages; it just puts the unsolved constraints back into the 93-- monad. See TcRnMonad Note [Constraints and errors] 94-- #16376 is an example of what goes wrong if you don't do this. 95-- 96-- NB: the caller should bring any environments into scope before 97-- calling this, so that the reportUnsolved has access to the most 98-- complete GlobalRdrEnv 99captureTopConstraints thing_inside 100 = do { static_wc_var <- TcM.newTcRef emptyWC ; 101 ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $ 102 TcM.tryCaptureConstraints thing_inside 103 ; stWC <- TcM.readTcRef static_wc_var 104 105 -- See TcRnMonad Note [Constraints and errors] 106 -- If the thing_inside threw an exception, but generated some insoluble 107 -- constraints, report the latter before propagating the exception 108 -- Otherwise they will be lost altogether 109 ; case mb_res of 110 Just res -> return (res, lie `andWC` stWC) 111 Nothing -> do { _ <- simplifyTop lie; failM } } 112 -- This call to simplifyTop is the reason 113 -- this function is here instead of TcRnMonad 114 -- We call simplifyTop so that it does defaulting 115 -- (esp of runtime-reps) before reporting errors 116 117simplifyTopImplic :: Bag Implication -> TcM () 118simplifyTopImplic implics 119 = do { empty_binds <- simplifyTop (mkImplicWC implics) 120 121 -- Since all the inputs are implications the returned bindings will be empty 122 ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds ) 123 124 ; return () } 125 126simplifyTop :: WantedConstraints -> TcM (Bag EvBind) 127-- Simplify top-level constraints 128-- Usually these will be implications, 129-- but when there is nothing to quantify we don't wrap 130-- in a degenerate implication, so we do that here instead 131simplifyTop wanteds 132 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds 133 ; ((final_wc, unsafe_ol), binds1) <- runTcS $ 134 do { final_wc <- simpl_top wanteds 135 ; unsafe_ol <- getSafeOverlapFailures 136 ; return (final_wc, unsafe_ol) } 137 ; traceTc "End simplifyTop }" empty 138 139 ; binds2 <- reportUnsolved final_wc 140 141 ; traceTc "reportUnsolved (unsafe overlapping) {" empty 142 ; unless (isEmptyCts unsafe_ol) $ do { 143 -- grab current error messages and clear, warnAllUnsolved will 144 -- update error messages which we'll grab and then restore saved 145 -- messages. 146 ; errs_var <- getErrsVar 147 ; saved_msg <- TcM.readTcRef errs_var 148 ; TcM.writeTcRef errs_var emptyMessages 149 150 ; warnAllUnsolved $ WC { wc_simple = unsafe_ol 151 , wc_impl = emptyBag } 152 153 ; whyUnsafe <- fst <$> TcM.readTcRef errs_var 154 ; TcM.writeTcRef errs_var saved_msg 155 ; recordUnsafeInfer whyUnsafe 156 } 157 ; traceTc "reportUnsolved (unsafe overlapping) }" empty 158 159 ; return (evBindMapBinds binds1 `unionBags` binds2) } 160 161 162-- | Type-check a thing that emits only equality constraints, solving any 163-- constraints we can and re-emitting constraints that we can't. The thing_inside 164-- should generally bump the TcLevel to make sure that this run of the solver 165-- doesn't affect anything lying around. 166solveLocalEqualities :: String -> TcM a -> TcM a 167solveLocalEqualities callsite thing_inside 168 = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside 169 ; emitConstraints wanted 170 171 -- See Note [Fail fast if there are insoluble kind equalities] 172 ; when (insolubleWC wanted) $ 173 failM 174 175 ; return res } 176 177{- Note [Fail fast if there are insoluble kind equalities] 178~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 179Rather like in simplifyInfer, fail fast if there is an insoluble 180constraint. Otherwise we'll just succeed in kind-checking a nonsense 181type, with a cascade of follow-up errors. 182 183For example polykinds/T12593, T15577, and many others. 184 185Take care to ensure that you emit the insoluble constraints before 186failing, because they are what will ulimately lead to the error 187messsage! 188-} 189 190solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a) 191solveLocalEqualitiesX callsite thing_inside 192 = do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ]) 193 194 ; (result, wanted) <- captureConstraints thing_inside 195 196 ; traceTc "solveLocalEqualities: running solver" (ppr wanted) 197 ; residual_wanted <- runTcSEqualities (solveWanteds wanted) 198 199 ; traceTc "solveLocalEqualitiesX end }" $ 200 text "residual_wanted =" <+> ppr residual_wanted 201 202 ; return (residual_wanted, result) } 203 204-- | Type-check a thing that emits only equality constraints, then 205-- solve those constraints. Fails outright if there is trouble. 206-- Use this if you're not going to get another crack at solving 207-- (because, e.g., you're checking a datatype declaration) 208solveEqualities :: TcM a -> TcM a 209solveEqualities thing_inside 210 = checkNoErrs $ -- See Note [Fail fast on kind errors] 211 do { lvl <- TcM.getTcLevel 212 ; traceTc "solveEqualities {" (text "level =" <+> ppr lvl) 213 214 ; (result, wanted) <- captureConstraints thing_inside 215 216 ; traceTc "solveEqualities: running solver" $ text "wanted = " <+> ppr wanted 217 ; final_wc <- runTcSEqualities $ simpl_top wanted 218 -- NB: Use simpl_top here so that we potentially default RuntimeRep 219 -- vars to LiftedRep. This is needed to avoid #14991. 220 221 ; traceTc "End solveEqualities }" empty 222 ; reportAllUnsolved final_wc 223 ; return result } 224 225-- | Simplify top-level constraints, but without reporting any unsolved 226-- constraints nor unsafe overlapping. 227simpl_top :: WantedConstraints -> TcS WantedConstraints 228 -- See Note [Top-level Defaulting Plan] 229simpl_top wanteds 230 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds) 231 -- This is where the main work happens 232 ; dflags <- getDynFlags 233 ; try_tyvar_defaulting dflags wc_first_go } 234 where 235 try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints 236 try_tyvar_defaulting dflags wc 237 | isEmptyWC wc 238 = return wc 239 | insolubleWC wc 240 , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles] 241 = try_class_defaulting wc 242 | otherwise 243 = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc) 244 ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs 245 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked 246 -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 247 -- and we definitely don't want to try to assign to those! 248 -- The isTyVar is needed to weed out coercion variables 249 250 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects 251 ; if or defaulted 252 then do { wc_residual <- nestTcS (solveWanteds wc) 253 -- See Note [Must simplify after defaulting] 254 ; try_class_defaulting wc_residual } 255 else try_class_defaulting wc } -- No defaulting took place 256 257 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints 258 try_class_defaulting wc 259 | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles] 260 = return wc 261 | otherwise -- See Note [When to do type-class defaulting] 262 = do { something_happened <- applyDefaultingRules wc 263 -- See Note [Top-level Defaulting Plan] 264 ; if something_happened 265 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc) 266 ; try_class_defaulting wc_residual } 267 -- See Note [Overview of implicit CallStacks] in TcEvidence 268 else try_callstack_defaulting wc } 269 270 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints 271 try_callstack_defaulting wc 272 | isEmptyWC wc 273 = return wc 274 | otherwise 275 = defaultCallStacks wc 276 277-- | Default any remaining @CallStack@ constraints to empty @CallStack@s. 278defaultCallStacks :: WantedConstraints -> TcS WantedConstraints 279-- See Note [Overview of implicit CallStacks] in TcEvidence 280defaultCallStacks wanteds 281 = do simples <- handle_simples (wc_simple wanteds) 282 mb_implics <- mapBagM handle_implic (wc_impl wanteds) 283 return (wanteds { wc_simple = simples 284 , wc_impl = catBagMaybes mb_implics }) 285 286 where 287 288 handle_simples simples 289 = catBagMaybes <$> mapBagM defaultCallStack simples 290 291 handle_implic :: Implication -> TcS (Maybe Implication) 292 -- The Maybe is because solving the CallStack constraint 293 -- may well allow us to discard the implication entirely 294 handle_implic implic 295 | isSolvedStatus (ic_status implic) 296 = return (Just implic) 297 | otherwise 298 = do { wanteds <- setEvBindsTcS (ic_binds implic) $ 299 -- defaultCallStack sets a binding, so 300 -- we must set the correct binding group 301 defaultCallStacks (ic_wanted implic) 302 ; setImplicationStatus (implic { ic_wanted = wanteds }) } 303 304 defaultCallStack ct 305 | ClassPred cls tys <- classifyPredType (ctPred ct) 306 , Just {} <- isCallStackPred cls tys 307 = do { solveCallStack (ctEvidence ct) EvCsEmpty 308 ; return Nothing } 309 310 defaultCallStack ct 311 = return (Just ct) 312 313 314{- Note [Fail fast on kind errors] 315~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 316solveEqualities is used to solve kind equalities when kind-checking 317user-written types. If solving fails we should fail outright, rather 318than just accumulate an error message, for two reasons: 319 320 * A kind-bogus type signature may cause a cascade of knock-on 321 errors if we let it pass 322 323 * More seriously, we don't have a convenient term-level place to add 324 deferred bindings for unsolved kind-equality constraints, so we 325 don't build evidence bindings (by usine reportAllUnsolved). That 326 means that we'll be left with with a type that has coercion holes 327 in it, something like 328 <type> |> co-hole 329 where co-hole is not filled in. Eeek! That un-filled-in 330 hole actually causes GHC to crash with "fvProv falls into a hole" 331 See #11563, #11520, #11516, #11399 332 333So it's important to use 'checkNoErrs' here! 334 335Note [When to do type-class defaulting] 336~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 337In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC 338was false, on the grounds that defaulting can't help solve insoluble 339constraints. But if we *don't* do defaulting we may report a whole 340lot of errors that would be solved by defaulting; these errors are 341quite spurious because fixing the single insoluble error means that 342defaulting happens again, which makes all the other errors go away. 343This is jolly confusing: #9033. 344 345So it seems better to always do type-class defaulting. 346 347However, always doing defaulting does mean that we'll do it in 348situations like this (#5934): 349 run :: (forall s. GenST s) -> Int 350 run = fromInteger 0 351We don't unify the return type of fromInteger with the given function 352type, because the latter involves foralls. So we're left with 353 (Num alpha, alpha ~ (forall s. GenST s) -> Int) 354Now we do defaulting, get alpha := Integer, and report that we can't 355match Integer with (forall s. GenST s) -> Int. That's not totally 356stupid, but perhaps a little strange. 357 358Another potential alternative would be to suppress *all* non-insoluble 359errors if there are *any* insoluble errors, anywhere, but that seems 360too drastic. 361 362Note [Must simplify after defaulting] 363~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 364We may have a deeply buried constraint 365 (t:*) ~ (a:Open) 366which we couldn't solve because of the kind incompatibility, and 'a' is free. 367Then when we default 'a' we can solve the constraint. And we want to do 368that before starting in on type classes. We MUST do it before reporting 369errors, because it isn't an error! #7967 was due to this. 370 371Note [Top-level Defaulting Plan] 372~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 373We have considered two design choices for where/when to apply defaulting. 374 (i) Do it in SimplCheck mode only /whenever/ you try to solve some 375 simple constraints, maybe deep inside the context of implications. 376 This used to be the case in GHC 7.4.1. 377 (ii) Do it in a tight loop at simplifyTop, once all other constraints have 378 finished. This is the current story. 379 380Option (i) had many disadvantages: 381 a) Firstly, it was deep inside the actual solver. 382 b) Secondly, it was dependent on the context (Infer a type signature, 383 or Check a type signature, or Interactive) since we did not want 384 to always start defaulting when inferring (though there is an exception to 385 this, see Note [Default while Inferring]). 386 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs: 387 f :: Int -> Bool 388 f x = const True (\y -> let w :: a -> a 389 w a = const a (y+1) 390 in w y) 391 We will get an implication constraint (for beta the type of y): 392 [untch=beta] forall a. 0 => Num beta 393 which we really cannot default /while solving/ the implication, since beta is 394 untouchable. 395 396Instead our new defaulting story is to pull defaulting out of the solver loop and 397go with option (ii), implemented at SimplifyTop. Namely: 398 - First, have a go at solving the residual constraint of the whole 399 program 400 - Try to approximate it with a simple constraint 401 - Figure out derived defaulting equations for that simple constraint 402 - Go round the loop again if you did manage to get some equations 403 404Now, that has to do with class defaulting. However there exists type variable /kind/ 405defaulting. Again this is done at the top-level and the plan is: 406 - At the top-level, once you had a go at solving the constraint, do 407 figure out /all/ the touchable unification variables of the wanted constraints. 408 - Apply defaulting to their kinds 409 410More details in Note [DefaultTyVar]. 411 412Note [Safe Haskell Overlapping Instances] 413~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 414In Safe Haskell, we apply an extra restriction to overlapping instances. The 415motive is to prevent untrusted code provided by a third-party, changing the 416behavior of trusted code through type-classes. This is due to the global and 417implicit nature of type-classes that can hide the source of the dictionary. 418 419Another way to state this is: if a module M compiles without importing another 420module N, changing M to import N shouldn't change the behavior of M. 421 422Overlapping instances with type-classes can violate this principle. However, 423overlapping instances aren't always unsafe. They are just unsafe when the most 424selected dictionary comes from untrusted code (code compiled with -XSafe) and 425overlaps instances provided by other modules. 426 427In particular, in Safe Haskell at a call site with overlapping instances, we 428apply the following rule to determine if it is a 'unsafe' overlap: 429 430 1) Most specific instance, I1, defined in an `-XSafe` compiled module. 431 2) I1 is an orphan instance or a MPTC. 432 3) At least one overlapped instance, Ix, is both: 433 A) from a different module than I1 434 B) Ix is not marked `OVERLAPPABLE` 435 436This is a slightly involved heuristic, but captures the situation of an 437imported module N changing the behavior of existing code. For example, if 438condition (2) isn't violated, then the module author M must depend either on a 439type-class or type defined in N. 440 441Secondly, when should these heuristics be enforced? We enforced them when the 442type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`. 443This allows `-XUnsafe` modules to operate without restriction, and for Safe 444Haskell inferrence to infer modules with unsafe overlaps as unsafe. 445 446One alternative design would be to also consider if an instance was imported as 447a `safe` import or not and only apply the restriction to instances imported 448safely. However, since instances are global and can be imported through more 449than one path, this alternative doesn't work. 450 451Note [Safe Haskell Overlapping Instances Implementation] 452~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 453 454How is this implemented? It's complicated! So we'll step through it all: 455 456 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where 457 we check if a particular type-class method call is safe or unsafe. We do this 458 through the return type, `ClsInstLookupResult`, where the last parameter is a 459 list of instances that are unsafe to overlap. When the method call is safe, 460 the list is null. 461 462 2) `TcInteract.matchClassInst` -- This module drives the instance resolution 463 / dictionary generation. The return type is `ClsInstResult`, which either 464 says no instance matched, or one found, and if it was a safe or unsafe 465 overlap. 466 467 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and 468 tries to resolve it by calling (in part) `matchClassInst`. The resolving 469 mechanism has a work list (of constraints) that it process one at a time. If 470 the constraint can't be resolved, it's added to an inert set. When compiling 471 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know 472 compilation should fail. These are handled as normal constraint resolution 473 failures from here-on (see step 6). 474 475 Otherwise, we may be inferring safety (or using `-Wunsafe`), and 476 compilation should succeed, but print warnings and/or mark the compiled module 477 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds 478 the unsafe (but resolved!) constraint to the `inert_safehask` field of 479 `InertCans`. 480 481 4) `TcSimplify.simplifyTop`: 482 * Call simpl_top, the top-level function for driving the simplifier for 483 constraint resolution. 484 485 * Once finished, call `getSafeOverlapFailures` to retrieve the 486 list of overlapping instances that were successfully resolved, 487 but unsafe. Remember, this is only applicable for generating warnings 488 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy` 489 cause compilation failure by not resolving the unsafe constraint at all. 490 491 * For unresolved constraints (all types), call `TcErrors.reportUnsolved`, 492 while for resolved but unsafe overlapping dictionary constraints, call 493 `TcErrors.warnAllUnsolved`. Both functions convert constraints into a 494 warning message for the user. 495 496 * In the case of `warnAllUnsolved` for resolved, but unsafe 497 dictionary constraints, we collect the generated warning 498 message (pop it) and call `TcRnMonad.recordUnsafeInfer` to 499 mark the module we are compiling as unsafe, passing the 500 warning message along as the reason. 501 502 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by 503 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we 504 know is the constraint that is unresolved or unsafe. For dictionary, all we 505 know is that we need a dictionary of type C, but not what instances are 506 available and how they overlap. So we once again call `lookupInstEnv` to 507 figure that out so we can generate a helpful error message. 508 509 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an 510 IORef called `tcg_safeInfer`. 511 512 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling 513 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence 514 failed. 515 516Note [No defaulting in the ambiguity check] 517~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 518When simplifying constraints for the ambiguity check, we use 519solveWantedsAndDrop, not simpl_top, so that we do no defaulting. 520#11947 was an example: 521 f :: Num a => Int -> Int 522This is ambiguous of course, but we don't want to default the 523(Num alpha) constraint to (Num Int)! Doing so gives a defaulting 524warning, but no error. 525 526Note [Defaulting insolubles] 527~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 528If a set of wanteds is insoluble, we have no hope of accepting the 529program. Yet we do not stop constraint solving, etc., because we may 530simplify the wanteds to produce better error messages. So, once 531we have an insoluble constraint, everything we do is just about producing 532helpful error messages. 533 534Should we default in this case or not? Let's look at an example (tcfail004): 535 536 (f,g) = (1,2,3) 537 538With defaulting, we get a conflict between (a0,b0) and (Integer,Integer,Integer). 539Without defaulting, we get a conflict between (a0,b0) and (a1,b1,c1). I (Richard) 540find the latter more helpful. Several other test cases (e.g. tcfail005) suggest 541similarly. So: we should not do class defaulting with insolubles. 542 543On the other hand, RuntimeRep-defaulting is different. Witness tcfail078: 544 545 f :: Integer i => i 546 f = 0 547 548Without RuntimeRep-defaulting, we GHC suggests that Integer should have kind 549TYPE r0 -> Constraint and then complains that r0 is actually untouchable 550(presumably, because it can't be sure if `Integer i` entails an equality). 551If we default, we are told of a clash between (* -> Constraint) and Constraint. 552The latter seems far better, suggesting we *should* do RuntimeRep-defaulting 553even on insolubles. 554 555But, evidently, not always. Witness UnliftedNewtypesInfinite: 556 557 newtype Foo = FooC (# Int#, Foo #) 558 559This should fail with an occurs-check error on the kind of Foo (with -XUnliftedNewtypes). 560If we default RuntimeRep-vars, we get 561 562 Expecting a lifted type, but ‘(# Int#, Foo #)’ is unlifted 563 564which is just plain wrong. 565 566Conclusion: we should do RuntimeRep-defaulting on insolubles only when the user does not 567want to hear about RuntimeRep stuff -- that is, when -fprint-explicit-runtime-reps 568is not set. 569-} 570 571------------------ 572simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM () 573simplifyAmbiguityCheck ty wanteds 574 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds) 575 ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds 576 -- NB: no defaulting! See Note [No defaulting in the ambiguity check] 577 578 ; traceTc "End simplifyAmbiguityCheck }" empty 579 580 -- Normally report all errors; but with -XAllowAmbiguousTypes 581 -- report only insoluble ones, since they represent genuinely 582 -- inaccessible code 583 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes 584 ; traceTc "reportUnsolved(ambig) {" empty 585 ; unless (allow_ambiguous && not (insolubleWC final_wc)) 586 (discardResult (reportUnsolved final_wc)) 587 ; traceTc "reportUnsolved(ambig) }" empty 588 589 ; return () } 590 591------------------ 592simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind) 593simplifyInteractive wanteds 594 = traceTc "simplifyInteractive" empty >> 595 simplifyTop wanteds 596 597------------------ 598simplifyDefault :: ThetaType -- Wanted; has no type variables in it 599 -> TcM () -- Succeeds if the constraint is soluble 600simplifyDefault theta 601 = do { traceTc "simplifyDefault" empty 602 ; wanteds <- newWanteds DefaultOrigin theta 603 ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds)) 604 ; reportAllUnsolved unsolved 605 ; return () } 606 607------------------ 608tcCheckSatisfiability :: Bag EvVar -> TcM Bool 609-- Return True if satisfiable, False if definitely contradictory 610tcCheckSatisfiability given_ids 611 = do { lcl_env <- TcM.getLclEnv 612 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env 613 ; (res, _ev_binds) <- runTcS $ 614 do { traceTcS "checkSatisfiability {" (ppr given_ids) 615 ; let given_cts = mkGivens given_loc (bagToList given_ids) 616 -- See Note [Superclasses and satisfiability] 617 ; solveSimpleGivens given_cts 618 ; insols <- getInertInsols 619 ; insols <- try_harder insols 620 ; traceTcS "checkSatisfiability }" (ppr insols) 621 ; return (isEmptyBag insols) } 622 ; return res } 623 where 624 try_harder :: Cts -> TcS Cts 625 -- Maybe we have to search up the superclass chain to find 626 -- an unsatisfiable constraint. Example: pmcheck/T3927b. 627 -- At the moment we try just once 628 try_harder insols 629 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable 630 = return insols -- Hurrah -- stop now. 631 | otherwise 632 = do { pending_given <- getPendingGivenScs 633 ; new_given <- makeSuperClasses pending_given 634 ; solveSimpleGivens new_given 635 ; getInertInsols } 636 637-- | Normalise a type as much as possible using the given constraints. 638-- See @Note [tcNormalise]@. 639tcNormalise :: Bag EvVar -> Type -> TcM Type 640tcNormalise given_ids ty 641 = do { lcl_env <- TcM.getLclEnv 642 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env 643 ; wanted_ct <- mk_wanted_ct 644 ; (res, _ev_binds) <- runTcS $ 645 do { traceTcS "tcNormalise {" (ppr given_ids) 646 ; let given_cts = mkGivens given_loc (bagToList given_ids) 647 ; solveSimpleGivens given_cts 648 ; wcs <- solveSimpleWanteds (unitBag wanted_ct) 649 -- It's an invariant that this wc_simple will always be 650 -- a singleton Ct, since that's what we fed in as input. 651 ; let ty' = case bagToList (wc_simple wcs) of 652 (ct:_) -> ctEvPred (ctEvidence ct) 653 cts -> pprPanic "tcNormalise" (ppr cts) 654 ; traceTcS "tcNormalise }" (ppr ty') 655 ; pure ty' } 656 ; return res } 657 where 658 mk_wanted_ct :: TcM Ct 659 mk_wanted_ct = do 660 let occ = mkVarOcc "$tcNorm" 661 name <- newSysName occ 662 let ev = mkLocalId name ty 663 hole = ExprHole $ OutOfScope occ emptyGlobalRdrEnv 664 newHoleCt hole ev ty 665 666{- Note [Superclasses and satisfiability] 667~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 668Expand superclasses before starting, because (Int ~ Bool), has 669(Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool) 670as a superclass, and it's the latter that is insoluble. See 671Note [The equality types story] in TysPrim. 672 673If we fail to prove unsatisfiability we (arbitrarily) try just once to 674find superclasses, using try_harder. Reason: we might have a type 675signature 676 f :: F op (Implements push) => .. 677where F is a type function. This happened in #3972. 678 679We could do more than once but we'd have to have /some/ limit: in the 680the recursive case, we would go on forever in the common case where 681the constraints /are/ satisfiable (#10592 comment:12!). 682 683For stratightforard situations without type functions the try_harder 684step does nothing. 685 686Note [tcNormalise] 687~~~~~~~~~~~~~~~~~~ 688tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas 689most invocations of the constraint solver are intended to simplify a set of 690constraints or to decide if a particular set of constraints is satisfiable, 691the purpose of tcNormalise is to take a type, plus some local constraints, and 692normalise the type as much as possible with respect to those constraints. 693 694It does *not* reduce type or data family applications or look through newtypes. 695 696Why is this useful? As one example, when coverage-checking an EmptyCase 697expression, it's possible that the type of the scrutinee will only reduce 698if some local equalities are solved for. See "Wrinkle: Local equalities" 699in Note [Type normalisation] in Check. 700 701To accomplish its stated goal, tcNormalise first feeds the local constraints 702into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds 703that singleton Ct into solveSimpleWanteds, which reduces the type in the 704CHoleCan as much as possible with respect to the local given constraints. When 705solveSimpleWanteds is finished, we dig out the type from the CHoleCan and 706return that. 707 708*********************************************************************************** 709* * 710* Inference 711* * 712*********************************************************************************** 713 714Note [Inferring the type of a let-bound variable] 715~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 716Consider 717 f x = rhs 718 719To infer f's type we do the following: 720 * Gather the constraints for the RHS with ambient level *one more than* 721 the current one. This is done by the call 722 pushLevelAndCaptureConstraints (tcMonoBinds...) 723 in TcBinds.tcPolyInfer 724 725 * Call simplifyInfer to simplify the constraints and decide what to 726 quantify over. We pass in the level used for the RHS constraints, 727 here called rhs_tclvl. 728 729This ensures that the implication constraint we generate, if any, 730has a strictly-increased level compared to the ambient level outside 731the let binding. 732 733-} 734 735-- | How should we choose which constraints to quantify over? 736data InferMode = ApplyMR -- ^ Apply the monomorphism restriction, 737 -- never quantifying over any constraints 738 | EagerDefaulting -- ^ See Note [TcRnExprMode] in TcRnDriver, 739 -- the :type +d case; this mode refuses 740 -- to quantify over any defaultable constraint 741 | NoRestrictions -- ^ Quantify over any constraint that 742 -- satisfies TcType.pickQuantifiablePreds 743 744instance Outputable InferMode where 745 ppr ApplyMR = text "ApplyMR" 746 ppr EagerDefaulting = text "EagerDefaulting" 747 ppr NoRestrictions = text "NoRestrictions" 748 749simplifyInfer :: TcLevel -- Used when generating the constraints 750 -> InferMode 751 -> [TcIdSigInst] -- Any signatures (possibly partial) 752 -> [(Name, TcTauType)] -- Variables to be generalised, 753 -- and their tau-types 754 -> WantedConstraints 755 -> TcM ([TcTyVar], -- Quantify over these type variables 756 [EvVar], -- ... and these constraints (fully zonked) 757 TcEvBinds, -- ... binding these evidence variables 758 WantedConstraints, -- Redidual as-yet-unsolved constraints 759 Bool) -- True <=> the residual constraints are insoluble 760 761simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds 762 | isEmptyWC wanteds 763 = do { -- When quantifying, we want to preserve any order of variables as they 764 -- appear in partial signatures. cf. decideQuantifiedTyVars 765 let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs 766 , (_,tv) <- sig_inst_skols sig ] 767 psig_theta = [ pred | sig <- partial_sigs 768 , pred <- sig_inst_theta sig ] 769 770 ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus) 771 ; qtkvs <- quantifyTyVars dep_vars 772 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs) 773 ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) } 774 775 | otherwise 776 = do { traceTc "simplifyInfer {" $ vcat 777 [ text "sigs =" <+> ppr sigs 778 , text "binds =" <+> ppr name_taus 779 , text "rhs_tclvl =" <+> ppr rhs_tclvl 780 , text "infer_mode =" <+> ppr infer_mode 781 , text "(unzonked) wanted =" <+> ppr wanteds 782 ] 783 784 ; let psig_theta = concatMap sig_inst_theta partial_sigs 785 786 -- First do full-blown solving 787 -- NB: we must gather up all the bindings from doing 788 -- this solving; hence (runTcSWithEvBinds ev_binds_var). 789 -- And note that since there are nested implications, 790 -- calling solveWanteds will side-effect their evidence 791 -- bindings, so we can't just revert to the input 792 -- constraint. 793 794 ; tc_env <- TcM.getEnv 795 ; ev_binds_var <- TcM.newTcEvBinds 796 ; psig_theta_vars <- mapM TcM.newEvVar psig_theta 797 ; wanted_transformed_incl_derivs 798 <- setTcLevel rhs_tclvl $ 799 runTcSWithEvBinds ev_binds_var $ 800 do { let loc = mkGivenLoc rhs_tclvl UnkSkol $ 801 env_lcl tc_env 802 psig_givens = mkGivens loc psig_theta_vars 803 ; _ <- solveSimpleGivens psig_givens 804 -- See Note [Add signature contexts as givens] 805 ; solveWanteds wanteds } 806 807 -- Find quant_pred_candidates, the predicates that 808 -- we'll consider quantifying over 809 -- NB1: wanted_transformed does not include anything provable from 810 -- the psig_theta; it's just the extra bit 811 -- NB2: We do not do any defaulting when inferring a type, this can lead 812 -- to less polymorphic types, see Note [Default while Inferring] 813 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs 814 ; let definite_error = insolubleWC wanted_transformed_incl_derivs 815 -- See Note [Quantification with errors] 816 -- NB: must include derived errors in this test, 817 -- hence "incl_derivs" 818 wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs 819 quant_pred_candidates 820 | definite_error = [] 821 | otherwise = ctsPreds (approximateWC False wanted_transformed) 822 823 -- Decide what type variables and constraints to quantify 824 -- NB: quant_pred_candidates is already fully zonked 825 -- NB: bound_theta are constraints we want to quantify over, 826 -- including the psig_theta, which we always quantify over 827 -- NB: bound_theta are fully zonked 828 ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl 829 name_taus partial_sigs 830 quant_pred_candidates 831 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta 832 833 -- We must produce bindings for the psig_theta_vars, because we may have 834 -- used them in evidence bindings constructed by solveWanteds earlier 835 -- Easiest way to do this is to emit them as new Wanteds (#14643) 836 ; ct_loc <- getCtLocM AnnOrigin Nothing 837 ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var 838 , ctev_dest = EvVarDest psig_theta_var 839 , ctev_nosh = WDeriv 840 , ctev_loc = ct_loc } 841 | psig_theta_var <- psig_theta_vars ] 842 843 -- Now construct the residual constraint 844 ; residual_wanted <- mkResidualConstraints rhs_tclvl ev_binds_var 845 name_taus co_vars qtvs bound_theta_vars 846 (wanted_transformed `andWC` mkSimpleWC psig_wanted) 847 848 -- All done! 849 ; traceTc "} simplifyInfer/produced residual implication for quantification" $ 850 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates 851 , text "psig_theta =" <+> ppr psig_theta 852 , text "bound_theta =" <+> ppr bound_theta 853 , text "qtvs =" <+> ppr qtvs 854 , text "definite_error =" <+> ppr definite_error ] 855 856 ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var 857 , residual_wanted, definite_error ) } 858 -- NB: bound_theta_vars must be fully zonked 859 where 860 partial_sigs = filter isPartialSig sigs 861 862-------------------- 863mkResidualConstraints :: TcLevel -> EvBindsVar 864 -> [(Name, TcTauType)] 865 -> VarSet -> [TcTyVar] -> [EvVar] 866 -> WantedConstraints -> TcM WantedConstraints 867-- Emit the remaining constraints from the RHS. 868-- See Note [Emitting the residual implication in simplifyInfer] 869mkResidualConstraints rhs_tclvl ev_binds_var 870 name_taus co_vars qtvs full_theta_vars wanteds 871 | isEmptyWC wanteds 872 = return wanteds 873 874 | otherwise 875 = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds) 876 ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple 877 is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars 878 879 ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple) 880 881 ; let inner_wanted = wanteds { wc_simple = inner_simple } 882 ; implics <- if isEmptyWC inner_wanted 883 then return emptyBag 884 else do implic1 <- newImplication 885 return $ unitBag $ 886 implic1 { ic_tclvl = rhs_tclvl 887 , ic_skols = qtvs 888 , ic_telescope = Nothing 889 , ic_given = full_theta_vars 890 , ic_wanted = inner_wanted 891 , ic_binds = ev_binds_var 892 , ic_no_eqs = False 893 , ic_info = skol_info } 894 895 ; return (WC { wc_simple = outer_simple 896 , wc_impl = implics })} 897 where 898 full_theta = map idType full_theta_vars 899 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty) 900 | (name, ty) <- name_taus ] 901 -- Don't add the quantified variables here, because 902 -- they are also bound in ic_skols and we want them 903 -- to be tidied uniformly 904 905-------------------- 906ctsPreds :: Cts -> [PredType] 907ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts 908 , let ev = ctEvidence ct ] 909 910{- Note [Emitting the residual implication in simplifyInfer] 911~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 912Consider 913 f = e 914where f's type is inferred to be something like (a, Proxy k (Int |> co)) 915and we have an as-yet-unsolved, or perhaps insoluble, constraint 916 [W] co :: Type ~ k 917We can't form types like (forall co. blah), so we can't generalise over 918the coercion variable, and hence we can't generalise over things free in 919its kind, in the case 'k'. But we can still generalise over 'a'. So 920we'll generalise to 921 f :: forall a. (a, Proxy k (Int |> co)) 922Now we do NOT want to form the residual implication constraint 923 forall a. [W] co :: Type ~ k 924because then co's eventual binding (which will be a value binding if we 925use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose 926type mentions 'co'). Instead, just as we don't generalise over 'co', we 927should not bury its constraint inside the implication. Instead, we must 928put it outside. 929 930That is the reason for the partitionBag in emitResidualConstraints, 931which takes the CoVars free in the inferred type, and pulls their 932constraints out. (NB: this set of CoVars should be closed-over-kinds.) 933 934All rather subtle; see #14584. 935 936Note [Add signature contexts as givens] 937~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 938Consider this (#11016): 939 f2 :: (?x :: Int) => _ 940 f2 = ?x 941or this 942 f3 :: a ~ Bool => (a, _) 943 f3 = (True, False) 944or theis 945 f4 :: (Ord a, _) => a -> Bool 946 f4 x = x==x 947 948We'll use plan InferGen because there are holes in the type. But: 949 * For f2 we want to have the (?x :: Int) constraint floating around 950 so that the functional dependencies kick in. Otherwise the 951 occurrence of ?x on the RHS produces constraint (?x :: alpha), and 952 we won't unify alpha:=Int. 953 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool) 954 in the RHS 955 * For f4 we want to use the (Ord a) in the signature to solve the Eq a 956 constraint. 957 958Solution: in simplifyInfer, just before simplifying the constraints 959gathered from the RHS, add Given constraints for the context of any 960type signatures. 961 962************************************************************************ 963* * 964 Quantification 965* * 966************************************************************************ 967 968Note [Deciding quantification] 969~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 970If the monomorphism restriction does not apply, then we quantify as follows: 971 972* Step 1. Take the global tyvars, and "grow" them using the equality 973 constraints 974 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can 975 happen because alpha is untouchable here) then do not quantify over 976 beta, because alpha fixes beta, and beta is effectively free in 977 the environment too 978 979 We also account for the monomorphism restriction; if it applies, 980 add the free vars of all the constraints. 981 982 Result is mono_tvs; we will not quantify over these. 983 984* Step 2. Default any non-mono tyvars (i.e ones that are definitely 985 not going to become further constrained), and re-simplify the 986 candidate constraints. 987 988 Motivation for re-simplification (#7857): imagine we have a 989 constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are 990 not free in the envt, and instance forall (a::*) (b::*). (C a) => C 991 (a -> b) The instance doesn't match while l1,l2 are polymorphic, but 992 it will match when we default them to LiftedRep. 993 994 This is all very tiresome. 995 996* Step 3: decide which variables to quantify over, as follows: 997 998 - Take the free vars of the tau-type (zonked_tau_tvs) and "grow" 999 them using all the constraints. These are tau_tvs_plus 1000 1001 - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being 1002 careful to close over kinds, and to skolemise the quantified tyvars. 1003 (This actually unifies each quantifies meta-tyvar with a fresh skolem.) 1004 1005 Result is qtvs. 1006 1007* Step 4: Filter the constraints using pickQuantifiablePreds and the 1008 qtvs. We have to zonk the constraints first, so they "see" the 1009 freshly created skolems. 1010 1011-} 1012 1013decideQuantification 1014 :: InferMode 1015 -> TcLevel 1016 -> [(Name, TcTauType)] -- Variables to be generalised 1017 -> [TcIdSigInst] -- Partial type signatures (if any) 1018 -> [PredType] -- Candidate theta; already zonked 1019 -> TcM ( [TcTyVar] -- Quantify over these (skolems) 1020 , [PredType] -- and this context (fully zonked) 1021 , VarSet) 1022-- See Note [Deciding quantification] 1023decideQuantification infer_mode rhs_tclvl name_taus psigs candidates 1024 = do { -- Step 1: find the mono_tvs 1025 ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode 1026 name_taus psigs candidates 1027 1028 -- Step 2: default any non-mono tyvars, and re-simplify 1029 -- This step may do some unification, but result candidates is zonked 1030 ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates 1031 1032 -- Step 3: decide which kind/type variables to quantify over 1033 ; qtvs <- decideQuantifiedTyVars name_taus psigs candidates 1034 1035 -- Step 4: choose which of the remaining candidate 1036 -- predicates to actually quantify over 1037 -- NB: decideQuantifiedTyVars turned some meta tyvars 1038 -- into quantified skolems, so we have to zonk again 1039 ; candidates <- TcM.zonkTcTypes candidates 1040 ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs) 1041 ; let quantifiable_candidates 1042 = pickQuantifiablePreds (mkVarSet qtvs) candidates 1043 -- NB: do /not/ run pickQuantifiablePreds over psig_theta, 1044 -- because we always want to quantify over psig_theta, and not 1045 -- drop any of them; e.g. CallStack constraints. c.f #14658 1046 1047 theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses] 1048 (psig_theta ++ quantifiable_candidates) 1049 1050 ; traceTc "decideQuantification" 1051 (vcat [ text "infer_mode:" <+> ppr infer_mode 1052 , text "candidates:" <+> ppr candidates 1053 , text "psig_theta:" <+> ppr psig_theta 1054 , text "mono_tvs:" <+> ppr mono_tvs 1055 , text "co_vars:" <+> ppr co_vars 1056 , text "qtvs:" <+> ppr qtvs 1057 , text "theta:" <+> ppr theta ]) 1058 ; return (qtvs, theta, co_vars) } 1059 1060------------------ 1061decideMonoTyVars :: InferMode 1062 -> [(Name,TcType)] 1063 -> [TcIdSigInst] 1064 -> [PredType] 1065 -> TcM (TcTyCoVarSet, [PredType], CoVarSet) 1066-- Decide which tyvars and covars cannot be generalised: 1067-- (a) Free in the environment 1068-- (b) Mentioned in a constraint we can't generalise 1069-- (c) Connected by an equality to (a) or (b) 1070-- Also return CoVars that appear free in the final quatified types 1071-- we can't quantify over these, and we must make sure they are in scope 1072decideMonoTyVars infer_mode name_taus psigs candidates 1073 = do { (no_quant, maybe_quant) <- pick infer_mode candidates 1074 1075 -- If possible, we quantify over partial-sig qtvs, so they are 1076 -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs 1077 ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ 1078 concatMap (map snd . sig_inst_skols) psigs 1079 1080 ; psig_theta <- mapM TcM.zonkTcType $ 1081 concatMap sig_inst_theta psigs 1082 1083 ; taus <- mapM (TcM.zonkTcType . snd) name_taus 1084 1085 ; tc_lvl <- TcM.getTcLevel 1086 ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta 1087 1088 co_vars = coVarsOfTypes (psig_tys ++ taus) 1089 co_var_tvs = closeOverKinds co_vars 1090 -- The co_var_tvs are tvs mentioned in the types of covars or 1091 -- coercion holes. We can't quantify over these covars, so we 1092 -- must include the variable in their types in the mono_tvs. 1093 -- E.g. If we can't quantify over co :: k~Type, then we can't 1094 -- quantify over k either! Hence closeOverKinds 1095 1096 mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $ 1097 tyCoVarsOfTypes candidates 1098 -- We need to grab all the non-quantifiable tyvars in the 1099 -- candidates so that we can grow this set to find other 1100 -- non-quantifiable tyvars. This can happen with something 1101 -- like 1102 -- f x y = ... 1103 -- where z = x 3 1104 -- The body of z tries to unify the type of x (call it alpha[1]) 1105 -- with (beta[2] -> gamma[2]). This unification fails because 1106 -- alpha is untouchable. But we need to know not to quantify over 1107 -- beta or gamma, because they are in the equality constraint with 1108 -- alpha. Actual test case: typecheck/should_compile/tc213 1109 1110 mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs 1111 1112 eq_constraints = filter isEqPrimPred candidates 1113 mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1 1114 1115 constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $ 1116 (growThetaTyVars eq_constraints 1117 (tyCoVarsOfTypes no_quant) 1118 `minusVarSet` mono_tvs2) 1119 `delVarSetList` psig_qtvs 1120 -- constrained_tvs: the tyvars that we are not going to 1121 -- quantify solely because of the monomorphism restriction 1122 -- 1123 -- (`minusVarSet` mono_tvs2`): a type variable is only 1124 -- "constrained" (so that the MR bites) if it is not 1125 -- free in the environment (#13785) 1126 -- 1127 -- (`delVarSetList` psig_qtvs): if the user has explicitly 1128 -- asked for quantification, then that request "wins" 1129 -- over the MR. Note: do /not/ delete psig_qtvs from 1130 -- mono_tvs1, because mono_tvs1 cannot under any circumstances 1131 -- be quantified (#14479); see 1132 -- Note [Quantification and partial signatures], Wrinkle 3, 4 1133 1134 mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs 1135 1136 -- Warn about the monomorphism restriction 1137 ; warn_mono <- woptM Opt_WarnMonomorphism 1138 ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $ 1139 warnTc (Reason Opt_WarnMonomorphism) 1140 (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) 1141 mr_msg 1142 1143 ; traceTc "decideMonoTyVars" $ vcat 1144 [ text "mono_tvs0 =" <+> ppr mono_tvs0 1145 , text "no_quant =" <+> ppr no_quant 1146 , text "maybe_quant =" <+> ppr maybe_quant 1147 , text "eq_constraints =" <+> ppr eq_constraints 1148 , text "mono_tvs =" <+> ppr mono_tvs 1149 , text "co_vars =" <+> ppr co_vars ] 1150 1151 ; return (mono_tvs, maybe_quant, co_vars) } 1152 where 1153 pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType]) 1154 -- Split the candidates into ones we definitely 1155 -- won't quantify, and ones that we might 1156 pick NoRestrictions cand = return ([], cand) 1157 pick ApplyMR cand = return (cand, []) 1158 pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings 1159 ; return (partition (is_int_ct os) cand) } 1160 1161 -- For EagerDefaulting, do not quantify over 1162 -- over any interactive class constraint 1163 is_int_ct ovl_strings pred 1164 | Just (cls, _) <- getClassPredTys_maybe pred 1165 = isInteractiveClass ovl_strings cls 1166 | otherwise 1167 = False 1168 1169 pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus 1170 mr_msg = 1171 hang (sep [ text "The Monomorphism Restriction applies to the binding" 1172 <> plural name_taus 1173 , text "for" <+> pp_bndrs ]) 1174 2 (hsep [ text "Consider giving" 1175 , text (if isSingleton name_taus then "it" else "them") 1176 , text "a type signature"]) 1177 1178------------------- 1179defaultTyVarsAndSimplify :: TcLevel 1180 -> TyCoVarSet 1181 -> [PredType] -- Assumed zonked 1182 -> TcM [PredType] -- Guaranteed zonked 1183-- Default any tyvar free in the constraints, 1184-- and re-simplify in case the defaulting allows further simplification 1185defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates 1186 = do { -- Promote any tyvars that we cannot generalise 1187 -- See Note [Promote momomorphic tyvars] 1188 ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) 1189 ; (prom, _) <- promoteTyVarSet mono_tvs 1190 1191 -- Default any kind/levity vars 1192 ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} 1193 <- candidateQTyVarsOfTypes candidates 1194 -- any covars should already be handled by 1195 -- the logic in decideMonoTyVars, which looks at 1196 -- the constraints generated 1197 1198 ; poly_kinds <- xoptM LangExt.PolyKinds 1199 ; default_kvs <- mapM (default_one poly_kinds True) 1200 (dVarSetElems cand_kvs) 1201 ; default_tvs <- mapM (default_one poly_kinds False) 1202 (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs)) 1203 ; let some_default = or default_kvs || or default_tvs 1204 1205 ; case () of 1206 _ | some_default -> simplify_cand candidates 1207 | prom -> mapM TcM.zonkTcType candidates 1208 | otherwise -> return candidates 1209 } 1210 where 1211 default_one poly_kinds is_kind_var tv 1212 | not (isMetaTyVar tv) 1213 = return False 1214 | tv `elemVarSet` mono_tvs 1215 = return False 1216 | otherwise 1217 = defaultTyVar (not poly_kinds && is_kind_var) tv 1218 1219 simplify_cand candidates 1220 = do { clone_wanteds <- newWanteds DefaultOrigin candidates 1221 ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $ 1222 simplifyWantedsTcM clone_wanteds 1223 -- Discard evidence; simples is fully zonked 1224 1225 ; let new_candidates = ctsPreds simples 1226 ; traceTc "Simplified after defaulting" $ 1227 vcat [ text "Before:" <+> ppr candidates 1228 , text "After:" <+> ppr new_candidates ] 1229 ; return new_candidates } 1230 1231------------------ 1232decideQuantifiedTyVars 1233 :: [(Name,TcType)] -- Annotated theta and (name,tau) pairs 1234 -> [TcIdSigInst] -- Partial signatures 1235 -> [PredType] -- Candidates, zonked 1236 -> TcM [TyVar] 1237-- Fix what tyvars we are going to quantify over, and quantify them 1238decideQuantifiedTyVars name_taus psigs candidates 1239 = do { -- Why psig_tys? We try to quantify over everything free in here 1240 -- See Note [Quantification and partial signatures] 1241 -- Wrinkles 2 and 3 1242 ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs 1243 , (_,tv) <- sig_inst_skols sig ] 1244 ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs 1245 , pred <- sig_inst_theta sig ] 1246 ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus 1247 1248 ; let -- Try to quantify over variables free in these types 1249 psig_tys = psig_tv_tys ++ psig_theta 1250 seed_tys = psig_tys ++ tau_tys 1251 1252 -- Now "grow" those seeds to find ones reachable via 'candidates' 1253 grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys) 1254 1255 -- Now we have to classify them into kind variables and type variables 1256 -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars 1257 -- 1258 -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces 1259 -- them in that order, so that the final qtvs quantifies in the same 1260 -- order as the partial signatures do (#13524) 1261 ; dv@DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes $ 1262 psig_tys ++ candidates ++ tau_tys 1263 ; let pick = (`dVarSetIntersectVarSet` grown_tcvs) 1264 dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } 1265 1266 ; traceTc "decideQuantifiedTyVars" (vcat 1267 [ text "candidates =" <+> ppr candidates 1268 , text "tau_tys =" <+> ppr tau_tys 1269 , text "seed_tys =" <+> ppr seed_tys 1270 , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys) 1271 , text "grown_tcvs =" <+> ppr grown_tcvs 1272 , text "dvs =" <+> ppr dvs_plus]) 1273 1274 ; quantifyTyVars dvs_plus } 1275 1276------------------ 1277growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet 1278-- See Note [Growing the tau-tvs using constraints] 1279growThetaTyVars theta tcvs 1280 | null theta = tcvs 1281 | otherwise = transCloVarSet mk_next seed_tcvs 1282 where 1283 seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips 1284 (ips, non_ips) = partition isIPPred theta 1285 -- See Note [Inheriting implicit parameters] in TcType 1286 1287 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones 1288 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips 1289 grow_one so_far pred tcvs 1290 | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs 1291 | otherwise = tcvs 1292 where 1293 pred_tcvs = tyCoVarsOfType pred 1294 1295 1296{- Note [Promote momomorphic tyvars] 1297~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1298Promote any type variables that are free in the environment. Eg 1299 f :: forall qtvs. bound_theta => zonked_tau 1300The free vars of f's type become free in the envt, and hence will show 1301up whenever 'f' is called. They may currently at rhs_tclvl, but they 1302had better be unifiable at the outer_tclvl! Example: envt mentions 1303alpha[1] 1304 tau_ty = beta[2] -> beta[2] 1305 constraints = alpha ~ [beta] 1306we don't quantify over beta (since it is fixed by envt) 1307so we must promote it! The inferred type is just 1308 f :: beta -> beta 1309 1310NB: promoteTyVar ignores coercion variables 1311 1312Note [Quantification and partial signatures] 1313~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1314When choosing type variables to quantify, the basic plan is to 1315quantify over all type variables that are 1316 * free in the tau_tvs, and 1317 * not forced to be monomorphic (mono_tvs), 1318 for example by being free in the environment. 1319 1320However, in the case of a partial type signature, be doing inference 1321*in the presence of a type signature*. For example: 1322 f :: _ -> a 1323 f x = ... 1324or 1325 g :: (Eq _a) => _b -> _b 1326In both cases we use plan InferGen, and hence call simplifyInfer. But 1327those 'a' variables are skolems (actually TyVarTvs), and we should be 1328sure to quantify over them. This leads to several wrinkles: 1329 1330* Wrinkle 1. In the case of a type error 1331 f :: _ -> Maybe a 1332 f x = True && x 1333 The inferred type of 'f' is f :: Bool -> Bool, but there's a 1334 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting 1335 machine expects to find a binding site for the skolem 'a', so we 1336 add it to the quantified tyvars. 1337 1338* Wrinkle 2. Consider the partial type signature 1339 f :: (Eq _) => Int -> Int 1340 f x = x 1341 In normal cases that makes sense; e.g. 1342 g :: Eq _a => _a -> _a 1343 g x = x 1344 where the signature makes the type less general than it could 1345 be. But for 'f' we must therefore quantify over the user-annotated 1346 constraints, to get 1347 f :: forall a. Eq a => Int -> Int 1348 (thereby correctly triggering an ambiguity error later). If we don't 1349 we'll end up with a strange open type 1350 f :: Eq alpha => Int -> Int 1351 which isn't ambiguous but is still very wrong. 1352 1353 Bottom line: Try to quantify over any variable free in psig_theta, 1354 just like the tau-part of the type. 1355 1356* Wrinkle 3 (#13482). Also consider 1357 f :: forall a. _ => Int -> Int 1358 f x = if (undefined :: a) == undefined then x else 0 1359 Here we get an (Eq a) constraint, but it's not mentioned in the 1360 psig_theta nor the type of 'f'. But we still want to quantify 1361 over 'a' even if the monomorphism restriction is on. 1362 1363* Wrinkle 4 (#14479) 1364 foo :: Num a => a -> a 1365 foo xxx = g xxx 1366 where 1367 g :: forall b. Num b => _ -> b 1368 g y = xxx + y 1369 1370 In the signature for 'g', we cannot quantify over 'b' because it turns out to 1371 get unified with 'a', which is free in g's environment. So we carefully 1372 refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We 1373 report the error later, in TcBinds.chooseInferredQuantifiers. 1374 1375Note [Growing the tau-tvs using constraints] 1376~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1377(growThetaTyVars insts tvs) is the result of extending the set 1378 of tyvars, tvs, using all conceivable links from pred 1379 1380E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} 1381Then growThetaTyVars preds tvs = {a,b,c} 1382 1383Notice that 1384 growThetaTyVars is conservative if v might be fixed by vs 1385 => v `elem` grow(vs,C) 1386 1387Note [Quantification with errors] 1388~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1389If we find that the RHS of the definition has some absolutely-insoluble 1390constraints (including especially "variable not in scope"), we 1391 1392* Abandon all attempts to find a context to quantify over, 1393 and instead make the function fully-polymorphic in whatever 1394 type we have found 1395 1396* Return a flag from simplifyInfer, indicating that we found an 1397 insoluble constraint. This flag is used to suppress the ambiguity 1398 check for the inferred type, which may well be bogus, and which 1399 tends to obscure the real error. This fix feels a bit clunky, 1400 but I failed to come up with anything better. 1401 1402Reasons: 1403 - Avoid downstream errors 1404 - Do not perform an ambiguity test on a bogus type, which might well 1405 fail spuriously, thereby obfuscating the original insoluble error. 1406 #14000 is an example 1407 1408I tried an alternative approach: simply failM, after emitting the 1409residual implication constraint; the exception will be caught in 1410TcBinds.tcPolyBinds, which gives all the binders in the group the type 1411(forall a. a). But that didn't work with -fdefer-type-errors, because 1412the recovery from failM emits no code at all, so there is no function 1413to run! But -fdefer-type-errors aspires to produce a runnable program. 1414 1415NB that we must include *derived* errors in the check for insolubles. 1416Example: 1417 (a::*) ~ Int# 1418We get an insoluble derived error *~#, and we don't want to discard 1419it before doing the isInsolubleWC test! (#8262) 1420 1421Note [Default while Inferring] 1422~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1423Our current plan is that defaulting only happens at simplifyTop and 1424not simplifyInfer. This may lead to some insoluble deferred constraints. 1425Example: 1426 1427instance D g => C g Int b 1428 1429constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha 1430type inferred = gamma -> gamma 1431 1432Now, if we try to default (alpha := Int) we will be able to refine the implication to 1433 (forall b. 0 => C gamma Int b) 1434which can then be simplified further to 1435 (forall b. 0 => D gamma) 1436Finally, we /can/ approximate this implication with (D gamma) and infer the quantified 1437type: forall g. D g => g -> g 1438 1439Instead what will currently happen is that we will get a quantified type 1440(forall g. g -> g) and an implication: 1441 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha 1442 1443Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an 1444unsolvable implication: 1445 forall g. 0 => (forall b. 0 => D g) 1446 1447The concrete example would be: 1448 h :: C g a s => g -> a -> ST s a 1449 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1) 1450 1451But it is quite tedious to do defaulting and resolve the implication constraints, and 1452we have not observed code breaking because of the lack of defaulting in inference, so 1453we don't do it for now. 1454 1455 1456 1457Note [Minimize by Superclasses] 1458~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1459When we quantify over a constraint, in simplifyInfer we need to 1460quantify over a constraint that is minimal in some sense: For 1461instance, if the final wanted constraint is (Eq alpha, Ord alpha), 1462we'd like to quantify over Ord alpha, because we can just get Eq alpha 1463from superclass selection from Ord alpha. This minimization is what 1464mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint 1465to check the original wanted. 1466 1467 1468Note [Avoid unnecessary constraint simplification] 1469~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1470 -------- NB NB NB (Jun 12) ------------- 1471 This note not longer applies; see the notes with #4361. 1472 But I'm leaving it in here so we remember the issue.) 1473 ---------------------------------------- 1474When inferring the type of a let-binding, with simplifyInfer, 1475try to avoid unnecessarily simplifying class constraints. 1476Doing so aids sharing, but it also helps with delicate 1477situations like 1478 1479 instance C t => C [t] where .. 1480 1481 f :: C [t] => .... 1482 f x = let g y = ...(constraint C [t])... 1483 in ... 1484When inferring a type for 'g', we don't want to apply the 1485instance decl, because then we can't satisfy (C t). So we 1486just notice that g isn't quantified over 't' and partition 1487the constraints before simplifying. 1488 1489This only half-works, but then let-generalisation only half-works. 1490 1491********************************************************************************* 1492* * 1493* Main Simplifier * 1494* * 1495*********************************************************************************** 1496 1497-} 1498 1499simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints 1500-- Solve the specified Wanted constraints 1501-- Discard the evidence binds 1502-- Discards all Derived stuff in result 1503-- Postcondition: fully zonked and unflattened constraints 1504simplifyWantedsTcM wanted 1505 = do { traceTc "simplifyWantedsTcM {" (ppr wanted) 1506 ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted)) 1507 ; result <- TcM.zonkWC result 1508 ; traceTc "simplifyWantedsTcM }" (ppr result) 1509 ; return result } 1510 1511solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints 1512-- Since solveWanteds returns the residual WantedConstraints, 1513-- it should always be called within a runTcS or something similar, 1514-- Result is not zonked 1515solveWantedsAndDrop wanted 1516 = do { wc <- solveWanteds wanted 1517 ; return (dropDerivedWC wc) } 1518 1519solveWanteds :: WantedConstraints -> TcS WantedConstraints 1520-- so that the inert set doesn't mindlessly propagate. 1521-- NB: wc_simples may be wanted /or/ derived now 1522solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics }) 1523 = do { cur_lvl <- TcS.getTcLevel 1524 ; traceTcS "solveWanteds {" $ 1525 vcat [ text "Level =" <+> ppr cur_lvl 1526 , ppr wc ] 1527 1528 ; wc1 <- solveSimpleWanteds simples 1529 -- Any insoluble constraints are in 'simples' and so get rewritten 1530 -- See Note [Rewrite insolubles] in TcSMonad 1531 1532 ; (floated_eqs, implics2) <- solveNestedImplications $ 1533 implics `unionBags` wc_impl wc1 1534 1535 ; dflags <- getDynFlags 1536 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs 1537 (wc1 { wc_impl = implics2 }) 1538 1539 ; ev_binds_var <- getTcEvBindsVar 1540 ; bb <- TcS.getTcEvBindsMap ev_binds_var 1541 ; traceTcS "solveWanteds }" $ 1542 vcat [ text "final wc =" <+> ppr final_wc 1543 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ] 1544 1545 ; return final_wc } 1546 1547simpl_loop :: Int -> IntWithInf -> Cts 1548 -> WantedConstraints -> TcS WantedConstraints 1549simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples }) 1550 | n `intGtLimit` limit 1551 = do { -- Add an error (not a warning) if we blow the limit, 1552 -- Typically if we blow the limit we are going to report some other error 1553 -- (an unsolved constraint), and we don't want that error to suppress 1554 -- the iteration limit warning! 1555 addErrTcS (hang (text "solveWanteds: too many iterations" 1556 <+> parens (text "limit =" <+> ppr limit)) 1557 2 (vcat [ text "Unsolved:" <+> ppr wc 1558 , ppUnless (isEmptyBag floated_eqs) $ 1559 text "Floated equalities:" <+> ppr floated_eqs 1560 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit" 1561 ])) 1562 ; return wc } 1563 1564 | not (isEmptyBag floated_eqs) 1565 = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples }) 1566 -- Put floated_eqs first so they get solved first 1567 -- NB: the floated_eqs may include /derived/ equalities 1568 -- arising from fundeps inside an implication 1569 1570 | superClassesMightHelp wc 1571 = -- We still have unsolved goals, and apparently no way to solve them, 1572 -- so try expanding superclasses at this level, both Given and Wanted 1573 do { pending_given <- getPendingGivenScs 1574 ; let (pending_wanted, simples1) = getPendingWantedScs simples 1575 ; if null pending_given && null pending_wanted 1576 then return wc -- After all, superclasses did not help 1577 else 1578 do { new_given <- makeSuperClasses pending_given 1579 ; new_wanted <- makeSuperClasses pending_wanted 1580 ; solveSimpleGivens new_given -- Add the new Givens to the inert set 1581 ; simplify_again n limit (null pending_given) 1582 wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } } 1583 1584 | otherwise 1585 = return wc 1586 1587simplify_again :: Int -> IntWithInf -> Bool 1588 -> WantedConstraints -> TcS WantedConstraints 1589-- We have definitely decided to have another go at solving 1590-- the wanted constraints (we have tried at least once already 1591simplify_again n limit no_new_given_scs 1592 wc@(WC { wc_simple = simples, wc_impl = implics }) 1593 = do { csTraceTcS $ 1594 text "simpl_loop iteration=" <> int n 1595 <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma 1596 , int (lengthBag simples) <+> text "simples to solve" ]) 1597 ; traceTcS "simpl_loop: wc =" (ppr wc) 1598 1599 ; (unifs1, wc1) <- reportUnifications $ 1600 solveSimpleWanteds $ 1601 simples 1602 1603 -- See Note [Cutting off simpl_loop] 1604 -- We have already tried to solve the nested implications once 1605 -- Try again only if we have unified some meta-variables 1606 -- (which is a bit like adding more givens), or we have some 1607 -- new Given superclasses 1608 ; let new_implics = wc_impl wc1 1609 ; if unifs1 == 0 && 1610 no_new_given_scs && 1611 isEmptyBag new_implics 1612 1613 then -- Do not even try to solve the implications 1614 simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics }) 1615 1616 else -- Try to solve the implications 1617 do { (floated_eqs2, implics2) <- solveNestedImplications $ 1618 implics `unionBags` new_implics 1619 ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 }) 1620 } } 1621 1622solveNestedImplications :: Bag Implication 1623 -> TcS (Cts, Bag Implication) 1624-- Precondition: the TcS inerts may contain unsolved simples which have 1625-- to be converted to givens before we go inside a nested implication. 1626solveNestedImplications implics 1627 | isEmptyBag implics 1628 = return (emptyBag, emptyBag) 1629 | otherwise 1630 = do { traceTcS "solveNestedImplications starting {" empty 1631 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics 1632 ; let floated_eqs = concatBag floated_eqs_s 1633 1634 -- ... and we are back in the original TcS inerts 1635 -- Notice that the original includes the _insoluble_simples so it was safe to ignore 1636 -- them in the beginning of this function. 1637 ; traceTcS "solveNestedImplications end }" $ 1638 vcat [ text "all floated_eqs =" <+> ppr floated_eqs 1639 , text "unsolved_implics =" <+> ppr unsolved_implics ] 1640 1641 ; return (floated_eqs, catBagMaybes unsolved_implics) } 1642 1643solveImplication :: Implication -- Wanted 1644 -> TcS (Cts, -- All wanted or derived floated equalities: var = type 1645 Maybe Implication) -- Simplified implication (empty or singleton) 1646-- Precondition: The TcS monad contains an empty worklist and given-only inerts 1647-- which after trying to solve this implication we must restore to their original value 1648solveImplication imp@(Implic { ic_tclvl = tclvl 1649 , ic_binds = ev_binds_var 1650 , ic_skols = skols 1651 , ic_given = given_ids 1652 , ic_wanted = wanteds 1653 , ic_info = info 1654 , ic_status = status }) 1655 | isSolvedStatus status 1656 = return (emptyCts, Just imp) -- Do nothing 1657 1658 | otherwise -- Even for IC_Insoluble it is worth doing more work 1659 -- The insoluble stuff might be in one sub-implication 1660 -- and other unsolved goals in another; and we want to 1661 -- solve the latter as much as possible 1662 = do { inerts <- getTcSInerts 1663 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts) 1664 1665 -- commented out; see `where` clause below 1666 -- ; when debugIsOn check_tc_level 1667 1668 -- Solve the nested constraints 1669 ; (no_given_eqs, given_insols, residual_wanted) 1670 <- nestImplicTcS ev_binds_var tclvl $ 1671 do { let loc = mkGivenLoc tclvl info (ic_env imp) 1672 givens = mkGivens loc given_ids 1673 ; solveSimpleGivens givens 1674 1675 ; residual_wanted <- solveWanteds wanteds 1676 -- solveWanteds, *not* solveWantedsAndDrop, because 1677 -- we want to retain derived equalities so we can float 1678 -- them out in floatEqualities 1679 1680 ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols 1681 -- Call getNoGivenEqs /after/ solveWanteds, because 1682 -- solveWanteds can augment the givens, via expandSuperClasses, 1683 -- to reveal given superclass equalities 1684 1685 ; return (no_eqs, given_insols, residual_wanted) } 1686 1687 ; (floated_eqs, residual_wanted) 1688 <- floatEqualities skols given_ids ev_binds_var 1689 no_given_eqs residual_wanted 1690 1691 ; traceTcS "solveImplication 2" 1692 (ppr given_insols $$ ppr residual_wanted) 1693 ; let final_wanted = residual_wanted `addInsols` given_insols 1694 -- Don't lose track of the insoluble givens, 1695 -- which signal unreachable code; put them in ic_wanted 1696 1697 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs 1698 , ic_wanted = final_wanted }) 1699 1700 ; evbinds <- TcS.getTcEvBindsMap ev_binds_var 1701 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var 1702 ; traceTcS "solveImplication end }" $ vcat 1703 [ text "no_given_eqs =" <+> ppr no_given_eqs 1704 , text "floated_eqs =" <+> ppr floated_eqs 1705 , text "res_implic =" <+> ppr res_implic 1706 , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) 1707 , text "implication tvcs =" <+> ppr tcvs ] 1708 1709 ; return (floated_eqs, res_implic) } 1710 1711 where 1712 -- TcLevels must be strictly increasing (see (ImplicInv) in 1713 -- Note [TcLevel and untouchable type variables] in TcType), 1714 -- and in fact I thinkthey should always increase one level at a time. 1715 1716 -- Though sensible, this check causes lots of testsuite failures. It is 1717 -- remaining commented out for now. 1718 {- 1719 check_tc_level = do { cur_lvl <- TcS.getTcLevel 1720 ; MASSERT2( tclvl == pushTcLevel cur_lvl , text "Cur lvl =" <+> ppr cur_lvl $$ text "Imp lvl =" <+> ppr tclvl ) } 1721 -} 1722 1723---------------------- 1724setImplicationStatus :: Implication -> TcS (Maybe Implication) 1725-- Finalise the implication returned from solveImplication: 1726-- * Set the ic_status field 1727-- * Trim the ic_wanted field to remove Derived constraints 1728-- Precondition: the ic_status field is not already IC_Solved 1729-- Return Nothing if we can discard the implication altogether 1730setImplicationStatus implic@(Implic { ic_status = status 1731 , ic_info = info 1732 , ic_wanted = wc 1733 , ic_given = givens }) 1734 | ASSERT2( not (isSolvedStatus status ), ppr info ) 1735 -- Precondition: we only set the status if it is not already solved 1736 not (isSolvedWC pruned_wc) 1737 = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic) 1738 1739 ; implic <- neededEvVars implic 1740 1741 ; let new_status | insolubleWC pruned_wc = IC_Insoluble 1742 | otherwise = IC_Unsolved 1743 new_implic = implic { ic_status = new_status 1744 , ic_wanted = pruned_wc } 1745 1746 ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic) 1747 1748 ; return $ Just new_implic } 1749 1750 | otherwise -- Everything is solved 1751 -- Set status to IC_Solved, 1752 -- and compute the dead givens and outer needs 1753 -- See Note [Tracking redundant constraints] 1754 = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic) 1755 1756 ; implic@(Implic { ic_need_inner = need_inner 1757 , ic_need_outer = need_outer }) <- neededEvVars implic 1758 1759 ; bad_telescope <- checkBadTelescope implic 1760 1761 ; let dead_givens | warnRedundantGivens info 1762 = filterOut (`elemVarSet` need_inner) givens 1763 | otherwise = [] -- None to report 1764 1765 discard_entire_implication -- Can we discard the entire implication? 1766 = null dead_givens -- No warning from this implication 1767 && not bad_telescope 1768 && isEmptyWC pruned_wc -- No live children 1769 && isEmptyVarSet need_outer -- No needed vars to pass up to parent 1770 1771 final_status 1772 | bad_telescope = IC_BadTelescope 1773 | otherwise = IC_Solved { ics_dead = dead_givens } 1774 final_implic = implic { ic_status = final_status 1775 , ic_wanted = pruned_wc } 1776 1777 ; traceTcS "setImplicationStatus(all-solved) }" $ 1778 vcat [ text "discard:" <+> ppr discard_entire_implication 1779 , text "new_implic:" <+> ppr final_implic ] 1780 1781 ; return $ if discard_entire_implication 1782 then Nothing 1783 else Just final_implic } 1784 where 1785 WC { wc_simple = simples, wc_impl = implics } = wc 1786 1787 pruned_simples = dropDerivedSimples simples 1788 pruned_implics = filterBag keep_me implics 1789 pruned_wc = WC { wc_simple = pruned_simples 1790 , wc_impl = pruned_implics } 1791 1792 keep_me :: Implication -> Bool 1793 keep_me ic 1794 | IC_Solved { ics_dead = dead_givens } <- ic_status ic 1795 -- Fully solved 1796 , null dead_givens -- No redundant givens to report 1797 , isEmptyBag (wc_impl (ic_wanted ic)) 1798 -- And no children that might have things to report 1799 = False -- Tnen we don't need to keep it 1800 | otherwise 1801 = True -- Otherwise, keep it 1802 1803checkBadTelescope :: Implication -> TcS Bool 1804-- True <=> the skolems form a bad telescope 1805-- See Note [Keeping scoped variables in order: Explicit] in TcHsType 1806checkBadTelescope (Implic { ic_telescope = m_telescope 1807 , ic_skols = skols }) 1808 | isJust m_telescope 1809 = do{ skols <- mapM TcS.zonkTyCoVarKind skols 1810 ; return (go emptyVarSet (reverse skols))} 1811 1812 | otherwise 1813 = return False 1814 1815 where 1816 go :: TyVarSet -- skolems that appear *later* than the current ones 1817 -> [TcTyVar] -- ordered skolems, in reverse order 1818 -> Bool -- True <=> there is an out-of-order skolem 1819 go _ [] = False 1820 go later_skols (one_skol : earlier_skols) 1821 | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols 1822 = True 1823 | otherwise 1824 = go (later_skols `extendVarSet` one_skol) earlier_skols 1825 1826warnRedundantGivens :: SkolemInfo -> Bool 1827warnRedundantGivens (SigSkol ctxt _ _) 1828 = case ctxt of 1829 FunSigCtxt _ warn_redundant -> warn_redundant 1830 ExprSigCtxt -> True 1831 _ -> False 1832 1833 -- To think about: do we want to report redundant givens for 1834 -- pattern synonyms, PatSynSigSkol? c.f #9953, comment:21. 1835warnRedundantGivens (InstSkol {}) = True 1836warnRedundantGivens _ = False 1837 1838neededEvVars :: Implication -> TcS Implication 1839-- Find all the evidence variables that are "needed", 1840-- and delete dead evidence bindings 1841-- See Note [Tracking redundant constraints] 1842-- See Note [Delete dead Given evidence bindings] 1843-- 1844-- - Start from initial_seeds (from nested implications) 1845-- 1846-- - Add free vars of RHS of all Wanted evidence bindings 1847-- and coercion variables accumulated in tcvs (all Wanted) 1848-- 1849-- - Generate 'needed', the needed set of EvVars, by doing transitive 1850-- closure through Given bindings 1851-- e.g. Needed {a,b} 1852-- Given a = sc_sel a2 1853-- Then a2 is needed too 1854-- 1855-- - Prune out all Given bindings that are not needed 1856-- 1857-- - From the 'needed' set, delete ev_bndrs, the binders of the 1858-- evidence bindings, to give the final needed variables 1859-- 1860neededEvVars implic@(Implic { ic_given = givens 1861 , ic_binds = ev_binds_var 1862 , ic_wanted = WC { wc_impl = implics } 1863 , ic_need_inner = old_needs }) 1864 = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var 1865 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var 1866 1867 ; let seeds1 = foldr add_implic_seeds old_needs implics 1868 seeds2 = foldEvBindMap add_wanted seeds1 ev_binds 1869 seeds3 = seeds2 `unionVarSet` tcvs 1870 need_inner = findNeededEvVars ev_binds seeds3 1871 live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds 1872 need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds 1873 `delVarSetList` givens 1874 1875 ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds 1876 -- See Note [Delete dead Given evidence bindings] 1877 1878 ; traceTcS "neededEvVars" $ 1879 vcat [ text "old_needs:" <+> ppr old_needs 1880 , text "seeds3:" <+> ppr seeds3 1881 , text "tcvs:" <+> ppr tcvs 1882 , text "ev_binds:" <+> ppr ev_binds 1883 , text "live_ev_binds:" <+> ppr live_ev_binds ] 1884 1885 ; return (implic { ic_need_inner = need_inner 1886 , ic_need_outer = need_outer }) } 1887 where 1888 add_implic_seeds (Implic { ic_need_outer = needs }) acc 1889 = needs `unionVarSet` acc 1890 1891 needed_ev_bind needed (EvBind { eb_lhs = ev_var 1892 , eb_is_given = is_given }) 1893 | is_given = ev_var `elemVarSet` needed 1894 | otherwise = True -- Keep all wanted bindings 1895 1896 del_ev_bndr :: EvBind -> VarSet -> VarSet 1897 del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v 1898 1899 add_wanted :: EvBind -> VarSet -> VarSet 1900 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs 1901 | is_given = needs -- Add the rhs vars of the Wanted bindings only 1902 | otherwise = evVarsOfTerm rhs `unionVarSet` needs 1903 1904 1905{- Note [Delete dead Given evidence bindings] 1906~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1907As a result of superclass expansion, we speculatively 1908generate evidence bindings for Givens. E.g. 1909 f :: (a ~ b) => a -> b -> Bool 1910 f x y = ... 1911We'll have 1912 [G] d1 :: (a~b) 1913and we'll specuatively generate the evidence binding 1914 [G] d2 :: (a ~# b) = sc_sel d 1915 1916Now d2 is available for solving. But it may not be needed! Usually 1917such dead superclass selections will eventually be dropped as dead 1918code, but: 1919 1920 * It won't always be dropped (#13032). In the case of an 1921 unlifted-equality superclass like d2 above, we generate 1922 case heq_sc d1 of d2 -> ... 1923 and we can't (in general) drop that case exrpession in case 1924 d1 is bottom. So it's technically unsound to have added it 1925 in the first place. 1926 1927 * Simply generating all those extra superclasses can generate lots of 1928 code that has to be zonked, only to be discarded later. Better not 1929 to generate it in the first place. 1930 1931 Moreover, if we simplify this implication more than once 1932 (e.g. because we can't solve it completely on the first iteration 1933 of simpl_looop), we'll generate all the same bindings AGAIN! 1934 1935Easy solution: take advantage of the work we are doing to track dead 1936(unused) Givens, and use it to prune the Given bindings too. This is 1937all done by neededEvVars. 1938 1939This led to a remarkable 25% overall compiler allocation decrease in 1940test T12227. 1941 1942But we don't get to discard all redundant equality superclasses, alas; 1943see #15205. 1944 1945Note [Tracking redundant constraints] 1946~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1947With Opt_WarnRedundantConstraints, GHC can report which 1948constraints of a type signature (or instance declaration) are 1949redundant, and can be omitted. Here is an overview of how it 1950works: 1951 1952----- What is a redundant constraint? 1953 1954* The things that can be redundant are precisely the Given 1955 constraints of an implication. 1956 1957* A constraint can be redundant in two different ways: 1958 a) It is implied by other givens. E.g. 1959 f :: (Eq a, Ord a) => blah -- Eq a unnecessary 1960 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary 1961 b) It is not needed by the Wanted constraints covered by the 1962 implication E.g. 1963 f :: Eq a => a -> Bool 1964 f x = True -- Equality not used 1965 1966* To find (a), when we have two Given constraints, 1967 we must be careful to drop the one that is a naked variable (if poss). 1968 So if we have 1969 f :: (Eq a, Ord a) => blah 1970 then we may find [G] sc_sel (d1::Ord a) :: Eq a 1971 [G] d2 :: Eq a 1972 We want to discard d2 in favour of the superclass selection from 1973 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther 1974 See Note [Replacement vs keeping]. 1975 1976* To find (b) we need to know which evidence bindings are 'wanted'; 1977 hence the eb_is_given field on an EvBind. 1978 1979----- How tracking works 1980 1981* The ic_need fields of an Implic records in-scope (given) evidence 1982 variables bound by the context, that were needed to solve this 1983 implication (so far). See the declaration of Implication. 1984 1985* When the constraint solver finishes solving all the wanteds in 1986 an implication, it sets its status to IC_Solved 1987 1988 - The ics_dead field, of IC_Solved, records the subset of this 1989 implication's ic_given that are redundant (not needed). 1990 1991* We compute which evidence variables are needed by an implication 1992 in setImplicationStatus. A variable is needed if 1993 a) it is free in the RHS of a Wanted EvBind, 1994 b) it is free in the RHS of an EvBind whose LHS is needed, 1995 c) it is in the ics_need of a nested implication. 1996 1997* We need to be careful not to discard an implication 1998 prematurely, even one that is fully solved, because we might 1999 thereby forget which variables it needs, and hence wrongly 2000 report a constraint as redundant. But we can discard it once 2001 its free vars have been incorporated into its parent; or if it 2002 simply has no free vars. This careful discarding is also 2003 handled in setImplicationStatus. 2004 2005----- Reporting redundant constraints 2006 2007* TcErrors does the actual warning, in warnRedundantConstraints. 2008 2009* We don't report redundant givens for *every* implication; only 2010 for those which reply True to TcSimplify.warnRedundantGivens: 2011 2012 - For example, in a class declaration, the default method *can* 2013 use the class constraint, but it certainly doesn't *have* to, 2014 and we don't want to report an error there. 2015 2016 - More subtly, in a function definition 2017 f :: (Ord a, Ord a, Ix a) => a -> a 2018 f x = rhs 2019 we do an ambiguity check on the type (which would find that one 2020 of the Ord a constraints was redundant), and then we check that 2021 the definition has that type (which might find that both are 2022 redundant). We don't want to report the same error twice, so we 2023 disable it for the ambiguity check. Hence using two different 2024 FunSigCtxts, one with the warn-redundant field set True, and the 2025 other set False in 2026 - TcBinds.tcSpecPrag 2027 - TcBinds.tcTySig 2028 2029 This decision is taken in setImplicationStatus, rather than TcErrors 2030 so that we can discard implication constraints that we don't need. 2031 So ics_dead consists only of the *reportable* redundant givens. 2032 2033----- Shortcomings 2034 2035Consider (see #9939) 2036 f2 :: (Eq a, Ord a) => a -> a -> Bool 2037 -- Ord a redundant, but Eq a is reported 2038 f2 x y = (x == y) 2039 2040We report (Eq a) as redundant, whereas actually (Ord a) is. But it's 2041really not easy to detect that! 2042 2043 2044Note [Cutting off simpl_loop] 2045~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2046It is very important not to iterate in simpl_loop unless there is a chance 2047of progress. #8474 is a classic example: 2048 2049 * There's a deeply-nested chain of implication constraints. 2050 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int 2051 2052 * From the innermost one we get a [D] alpha ~ Int, 2053 but alpha is untouchable until we get out to the outermost one 2054 2055 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha 2056 is untouchable, the solveInteract in simpl_loop makes no progress 2057 2058 * So there is no point in attempting to re-solve 2059 ?yn:betan => [W] ?x:Int 2060 via solveNestedImplications, because we'll just get the 2061 same [D] again 2062 2063 * If we *do* re-solve, we'll get an ininite loop. It is cut off by 2064 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie 2065 exponentially many) iterations! 2066 2067Conclusion: we should call solveNestedImplications only if we did 2068some unification in solveSimpleWanteds; because that's the only way 2069we'll get more Givens (a unification is like adding a Given) to 2070allow the implication to make progress. 2071-} 2072 2073promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar) 2074-- When we float a constraint out of an implication we must restore 2075-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType 2076-- Return True <=> we did some promotion 2077-- Also returns either the original tyvar (no promotion) or the new one 2078-- See Note [Promoting unification variables] 2079promoteTyVar tv 2080 = do { tclvl <- TcM.getTcLevel 2081 ; if (isFloatedTouchableMetaTyVar tclvl tv) 2082 then do { cloned_tv <- TcM.cloneMetaTyVar tv 2083 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl 2084 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) 2085 ; return (True, rhs_tv) } 2086 else return (False, tv) } 2087 2088-- Returns whether or not *any* tyvar is defaulted 2089promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet) 2090promoteTyVarSet tvs 2091 = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs) 2092 -- non-determinism is OK because order of promotion doesn't matter 2093 2094 ; return (or bools, mkVarSet tyvars) } 2095 2096promoteTyVarTcS :: TcTyVar -> TcS () 2097-- When we float a constraint out of an implication we must restore 2098-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType 2099-- See Note [Promoting unification variables] 2100-- We don't just call promoteTyVar because we want to use unifyTyVar, 2101-- not writeMetaTyVar 2102promoteTyVarTcS tv 2103 = do { tclvl <- TcS.getTcLevel 2104 ; when (isFloatedTouchableMetaTyVar tclvl tv) $ 2105 do { cloned_tv <- TcS.cloneMetaTyVar tv 2106 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl 2107 ; unifyTyVar tv (mkTyVarTy rhs_tv) } } 2108 2109-- | Like 'defaultTyVar', but in the TcS monad. 2110defaultTyVarTcS :: TcTyVar -> TcS Bool 2111defaultTyVarTcS the_tv 2112 | isRuntimeRepVar the_tv 2113 , not (isTyVarTyVar the_tv) 2114 -- TyVarTvs should only be unified with a tyvar 2115 -- never with a type; c.f. TcMType.defaultTyVar 2116 -- and Note [Inferring kinds for type declarations] in TcTyClsDecls 2117 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv) 2118 ; unifyTyVar the_tv liftedRepTy 2119 ; return True } 2120 | otherwise 2121 = return False -- the common case 2122 2123approximateWC :: Bool -> WantedConstraints -> Cts 2124-- Postcondition: Wanted or Derived Cts 2125-- See Note [ApproximateWC] 2126approximateWC float_past_equalities wc 2127 = float_wc emptyVarSet wc 2128 where 2129 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts 2130 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) 2131 = filterBag (is_floatable trapping_tvs) simples `unionBags` 2132 do_bag (float_implic trapping_tvs) implics 2133 where 2134 2135 float_implic :: TcTyCoVarSet -> Implication -> Cts 2136 float_implic trapping_tvs imp 2137 | float_past_equalities || ic_no_eqs imp 2138 = float_wc new_trapping_tvs (ic_wanted imp) 2139 | otherwise -- Take care with equalities 2140 = emptyCts -- See (1) under Note [ApproximateWC] 2141 where 2142 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp 2143 2144 do_bag :: (a -> Bag c) -> Bag a -> Bag c 2145 do_bag f = foldr (unionBags.f) emptyBag 2146 2147 is_floatable skol_tvs ct 2148 | isGivenCt ct = False 2149 | isHoleCt ct = False 2150 | insolubleEqCt ct = False 2151 | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs 2152 2153{- Note [ApproximateWC] 2154~~~~~~~~~~~~~~~~~~~~~~~ 2155approximateWC takes a constraint, typically arising from the RHS of a 2156let-binding whose type we are *inferring*, and extracts from it some 2157*simple* constraints that we might plausibly abstract over. Of course 2158the top-level simple constraints are plausible, but we also float constraints 2159out from inside, if they are not captured by skolems. 2160 2161The same function is used when doing type-class defaulting (see the call 2162to applyDefaultingRules) to extract constraints that that might be defaulted. 2163 2164There is one caveat: 2165 21661. When infering most-general types (in simplifyInfer), we do *not* 2167 float anything out if the implication binds equality constraints, 2168 because that defeats the OutsideIn story. Consider 2169 data T a where 2170 TInt :: T Int 2171 MkT :: T a 2172 2173 f TInt = 3::Int 2174 2175 We get the implication (a ~ Int => res ~ Int), where so far we've decided 2176 f :: T a -> res 2177 We don't want to float (res~Int) out because then we'll infer 2178 f :: T a -> Int 2179 which is only on of the possible types. (GHC 7.6 accidentally *did* 2180 float out of such implications, which meant it would happily infer 2181 non-principal types.) 2182 2183 HOWEVER (#12797) in findDefaultableGroups we are not worried about 2184 the most-general type; and we /do/ want to float out of equalities. 2185 Hence the boolean flag to approximateWC. 2186 2187------ Historical note ----------- 2188There used to be a second caveat, driven by #8155 2189 2190 2. We do not float out an inner constraint that shares a type variable 2191 (transitively) with one that is trapped by a skolem. Eg 2192 forall a. F a ~ beta, Integral beta 2193 We don't want to float out (Integral beta). Doing so would be bad 2194 when defaulting, because then we'll default beta:=Integer, and that 2195 makes the error message much worse; we'd get 2196 Can't solve F a ~ Integer 2197 rather than 2198 Can't solve Integral (F a) 2199 2200 Moreover, floating out these "contaminated" constraints doesn't help 2201 when generalising either. If we generalise over (Integral b), we still 2202 can't solve the retained implication (forall a. F a ~ b). Indeed, 2203 arguably that too would be a harder error to understand. 2204 2205But this transitive closure stuff gives rise to a complex rule for 2206when defaulting actually happens, and one that was never documented. 2207Moreover (#12923), the more complex rule is sometimes NOT what 2208you want. So I simply removed the extra code to implement the 2209contamination stuff. There was zero effect on the testsuite (not even 2210#8155). 2211------ End of historical note ----------- 2212 2213 2214Note [DefaultTyVar] 2215~~~~~~~~~~~~~~~~~~~ 2216defaultTyVar is used on any un-instantiated meta type variables to 2217default any RuntimeRep variables to LiftedRep. This is important 2218to ensure that instance declarations match. For example consider 2219 2220 instance Show (a->b) 2221 foo x = show (\_ -> True) 2222 2223Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r), 2224and that won't match the tcTypeKind (*) in the instance decl. See tests 2225tc217 and tc175. 2226 2227We look only at touchable type variables. No further constraints 2228are going to affect these type variables, so it's time to do it by 2229hand. However we aren't ready to default them fully to () or 2230whatever, because the type-class defaulting rules have yet to run. 2231 2232An alternate implementation would be to emit a derived constraint setting 2233the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect. 2234 2235Note [Promote _and_ default when inferring] 2236~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2237When we are inferring a type, we simplify the constraint, and then use 2238approximateWC to produce a list of candidate constraints. Then we MUST 2239 2240 a) Promote any meta-tyvars that have been floated out by 2241 approximateWC, to restore invariant (WantedInv) described in 2242 Note [TcLevel and untouchable type variables] in TcType. 2243 2244 b) Default the kind of any meta-tyvars that are not mentioned in 2245 in the environment. 2246 2247To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we 2248have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it 2249should! If we don't solve the constraint, we'll stupidly quantify over 2250(C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over 2251(b:*) instead of (a:OpenKind), which can lead to disaster; see #7332. 2252#7641 is a simpler example. 2253 2254Note [Promoting unification variables] 2255~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2256When we float an equality out of an implication we must "promote" free 2257unification variables of the equality, in order to maintain Invariant 2258(WantedInv) from Note [TcLevel and untouchable type variables] in 2259TcType. for the leftover implication. 2260 2261This is absolutely necessary. Consider the following example. We start 2262with two implications and a class with a functional dependency. 2263 2264 class C x y | x -> y 2265 instance C [a] [a] 2266 2267 (I1) [untch=beta]forall b. 0 => F Int ~ [beta] 2268 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c] 2269 2270We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 2271They may react to yield that (beta := [alpha]) which can then be pushed inwards 2272the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that 2273(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable 2274beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs: 2275 2276 class C x y | x -> y where 2277 op :: x -> y -> () 2278 2279 instance C [a] [a] 2280 2281 type family F a :: * 2282 2283 h :: F Int -> () 2284 h = undefined 2285 2286 data TEx where 2287 TEx :: a -> TEx 2288 2289 f (x::beta) = 2290 let g1 :: forall b. b -> () 2291 g1 _ = h [x] 2292 g2 z = case z of TEx y -> (h [[undefined]], op x [y]) 2293 in (g1 '3', g2 undefined) 2294 2295 2296 2297********************************************************************************* 2298* * 2299* Floating equalities * 2300* * 2301********************************************************************************* 2302 2303Note [Float Equalities out of Implications] 2304~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2305For ordinary pattern matches (including existentials) we float 2306equalities out of implications, for instance: 2307 data T where 2308 MkT :: Eq a => a -> T 2309 f x y = case x of MkT _ -> (y::Int) 2310We get the implication constraint (x::T) (y::alpha): 2311 forall a. [untouchable=alpha] Eq a => alpha ~ Int 2312We want to float out the equality into a scope where alpha is no 2313longer untouchable, to solve the implication! 2314 2315But we cannot float equalities out of implications whose givens may 2316yield or contain equalities: 2317 2318 data T a where 2319 T1 :: T Int 2320 T2 :: T Bool 2321 T3 :: T a 2322 2323 h :: T a -> a -> Int 2324 2325 f x y = case x of 2326 T1 -> y::Int 2327 T2 -> y::Bool 2328 T3 -> h x y 2329 2330We generate constraint, for (x::T alpha) and (y :: beta): 2331 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch 2332 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch 2333 (alpha ~ beta) -- From 3rd branch 2334 2335If we float the equality (beta ~ Int) outside of the first implication and 2336the equality (beta ~ Bool) out of the second we get an insoluble constraint. 2337But if we just leave them inside the implications, we unify alpha := beta and 2338solve everything. 2339 2340Principle: 2341 We do not want to float equalities out which may 2342 need the given *evidence* to become soluble. 2343 2344Consequence: classes with functional dependencies don't matter (since there is 2345no evidence for a fundep equality), but equality superclasses do matter (since 2346they carry evidence). 2347-} 2348 2349floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool 2350 -> WantedConstraints 2351 -> TcS (Cts, WantedConstraints) 2352-- Main idea: see Note [Float Equalities out of Implications] 2353-- 2354-- Precondition: the wc_simple of the incoming WantedConstraints are 2355-- fully zonked, so that we can see their free variables 2356-- 2357-- Postcondition: The returned floated constraints (Cts) are only 2358-- Wanted or Derived 2359-- 2360-- Also performs some unifications (via promoteTyVar), adding to 2361-- monadically-carried ty_binds. These will be used when processing 2362-- floated_eqs later 2363-- 2364-- Subtleties: Note [Float equalities from under a skolem binding] 2365-- Note [Skolem escape] 2366-- Note [What prevents a constraint from floating] 2367floatEqualities skols given_ids ev_binds_var no_given_eqs 2368 wanteds@(WC { wc_simple = simples }) 2369 | not no_given_eqs -- There are some given equalities, so don't float 2370 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications] 2371 2372 | otherwise 2373 = do { -- First zonk: the inert set (from whence they came) is fully 2374 -- zonked, but unflattening may have filled in unification 2375 -- variables, and we /must/ see them. Otherwise we may float 2376 -- constraints that mention the skolems! 2377 simples <- TcS.zonkSimples simples 2378 ; binds <- TcS.getTcEvBindsMap ev_binds_var 2379 2380 -- Now we can pick the ones to float 2381 -- The constraints are un-flattened and de-canonicalised 2382 ; let (candidate_eqs, no_float_cts) = partitionBag is_float_eq_candidate simples 2383 2384 seed_skols = mkVarSet skols `unionVarSet` 2385 mkVarSet given_ids `unionVarSet` 2386 foldr add_non_flt_ct emptyVarSet no_float_cts `unionVarSet` 2387 foldEvBindMap add_one_bind emptyVarSet binds 2388 -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3) 2389 -- Include the EvIds of any non-floating constraints 2390 2391 extended_skols = transCloVarSet (add_captured_ev_ids candidate_eqs) seed_skols 2392 -- extended_skols contains the EvIds of all the trapped constraints 2393 -- See Note [What prevents a constraint from floating] (3) 2394 2395 (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) 2396 candidate_eqs 2397 2398 remaining_simples = no_float_cts `andCts` no_flt_eqs 2399 2400 -- Promote any unification variables mentioned in the floated equalities 2401 -- See Note [Promoting unification variables] 2402 ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs) 2403 2404 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols 2405 , text "Extended skols =" <+> ppr extended_skols 2406 , text "Simples =" <+> ppr simples 2407 , text "Candidate eqs =" <+> ppr candidate_eqs 2408 , text "Floated eqs =" <+> ppr flt_eqs]) 2409 ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) } 2410 2411 where 2412 add_one_bind :: EvBind -> VarSet -> VarSet 2413 add_one_bind bind acc = extendVarSet acc (evBindVar bind) 2414 2415 add_non_flt_ct :: Ct -> VarSet -> VarSet 2416 add_non_flt_ct ct acc | isDerivedCt ct = acc 2417 | otherwise = extendVarSet acc (ctEvId ct) 2418 2419 is_floatable :: VarSet -> Ct -> Bool 2420 is_floatable skols ct 2421 | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols) 2422 | otherwise = not (ctEvId ct `elemVarSet` skols) 2423 2424 add_captured_ev_ids :: Cts -> VarSet -> VarSet 2425 add_captured_ev_ids cts skols = foldr extra_skol emptyVarSet cts 2426 where 2427 extra_skol ct acc 2428 | isDerivedCt ct = acc 2429 | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct) 2430 | otherwise = acc 2431 2432 -- Identify which equalities are candidates for floating 2433 -- Float out alpha ~ ty, or ty ~ alpha which might be unified outside 2434 -- See Note [Which equalities to float] 2435 is_float_eq_candidate ct 2436 | pred <- ctPred ct 2437 , EqPred NomEq ty1 ty2 <- classifyPredType pred 2438 , tcTypeKind ty1 `tcEqType` tcTypeKind ty2 2439 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of 2440 (Just tv1, _) -> float_tv_eq_candidate tv1 ty2 2441 (_, Just tv2) -> float_tv_eq_candidate tv2 ty1 2442 _ -> False 2443 | otherwise = False 2444 2445 float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float] 2446 = isMetaTyVar tv1 2447 && (not (isTyVarTyVar tv1) || isTyVarTy ty2) 2448 2449 2450{- Note [Float equalities from under a skolem binding] 2451~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2452Which of the simple equalities can we float out? Obviously, only 2453ones that don't mention the skolem-bound variables. But that is 2454over-eager. Consider 2455 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int 2456The second constraint doesn't mention 'a'. But if we float it, 2457we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that 2458beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll 2459we left with the constraint 2460 [2] forall a. a ~ gamma'[1] 2461which is insoluble because gamma became untouchable. 2462 2463Solution: float only constraints that stand a jolly good chance of 2464being soluble simply by being floated, namely ones of form 2465 a ~ ty 2466where 'a' is a currently-untouchable unification variable, but may 2467become touchable by being floated (perhaps by more than one level). 2468 2469We had a very complicated rule previously, but this is nice and 2470simple. (To see the notes, look at this Note in a version of 2471TcSimplify prior to Oct 2014). 2472 2473Note [Which equalities to float] 2474~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2475Which equalities should we float? We want to float ones where there 2476is a decent chance that floating outwards will allow unification to 2477happen. In particular, float out equalities that are: 2478 2479* Of form (alpha ~# ty) or (ty ~# alpha), where 2480 * alpha is a meta-tyvar. 2481 * And 'alpha' is not a TyVarTv with 'ty' being a non-tyvar. In that 2482 case, floating out won't help either, and it may affect grouping 2483 of error messages. 2484 2485* Homogeneous (both sides have the same kind). Why only homogeneous? 2486 Because heterogeneous equalities have derived kind equalities. 2487 See Note [Equalities with incompatible kinds] in TcCanonical. 2488 If we float out a hetero equality, then it will spit out the same 2489 derived kind equality again, which might create duplicate error 2490 messages. 2491 2492 Instead, we do float out the kind equality (if it's worth floating 2493 out, as above). If/when we solve it, we'll be able to rewrite the 2494 original hetero equality to be homogeneous, and then perhaps make 2495 progress / float it out. The duplicate error message was spotted in 2496 typecheck/should_fail/T7368. 2497 2498* Nominal. No point in floating (alpha ~R# ty), because we do not 2499 unify representational equalities even if alpha is touchable. 2500 See Note [Do not unify representational equalities] in TcInteract. 2501 2502Note [Skolem escape] 2503~~~~~~~~~~~~~~~~~~~~ 2504You might worry about skolem escape with all this floating. 2505For example, consider 2506 [2] forall a. (a ~ F beta[2] delta, 2507 Maybe beta[2] ~ gamma[1]) 2508 2509The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and 2510solve with gamma := beta. But what if later delta:=Int, and 2511 F b Int = b. 2512Then we'd get a ~ beta[2], and solve to get beta:=a, and now the 2513skolem has escaped! 2514 2515But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2] 2516to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be. 2517 2518Note [What prevents a constraint from floating] 2519~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2520What /prevents/ a constraint from floating? If it mentions one of the 2521"bound variables of the implication". What are they? 2522 2523The "bound variables of the implication" are 2524 2525 1. The skolem type variables `ic_skols` 2526 2527 2. The "given" evidence variables `ic_given`. Example: 2528 forall a. (co :: t1 ~# t2) => [W] co2 : (a ~# b |> co) 2529 Here 'co' is bound 2530 2531 3. The binders of all evidence bindings in `ic_binds`. Example 2532 forall a. (d :: t1 ~ t2) 2533 EvBinds { (co :: t1 ~# t2) = superclass-sel d } 2534 => [W] co2 : (a ~# b |> co) 2535 Here `co` is gotten by superclass selection from `d`, and the 2536 wanted constraint co2 must not float. 2537 2538 4. And the evidence variable of any equality constraint (incl 2539 Wanted ones) whose type mentions a bound variable. Example: 2540 forall k. [W] co1 :: t1 ~# t2 |> co2 2541 [W] co2 :: k ~# * 2542 Here, since `k` is bound, so is `co2` and hence so is `co1`. 2543 2544Here (1,2,3) are handled by the "seed_skols" calculation, and 2545(4) is done by the transCloVarSet call. 2546 2547The possible dependence on givens, and evidence bindings, is more 2548subtle than we'd realised at first. See #14584. 2549 2550 2551********************************************************************************* 2552* * 2553* Defaulting and disambiguation * 2554* * 2555********************************************************************************* 2556-} 2557 2558applyDefaultingRules :: WantedConstraints -> TcS Bool 2559-- True <=> I did some defaulting, by unifying a meta-tyvar 2560-- Input WantedConstraints are not necessarily zonked 2561 2562applyDefaultingRules wanteds 2563 | isEmptyWC wanteds 2564 = return False 2565 | otherwise 2566 = do { info@(default_tys, _) <- getDefaultInfo 2567 ; wanteds <- TcS.zonkWC wanteds 2568 2569 ; let groups = findDefaultableGroups info wanteds 2570 2571 ; traceTcS "applyDefaultingRules {" $ 2572 vcat [ text "wanteds =" <+> ppr wanteds 2573 , text "groups =" <+> ppr groups 2574 , text "info =" <+> ppr info ] 2575 2576 ; something_happeneds <- mapM (disambigGroup default_tys) groups 2577 2578 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds) 2579 2580 ; return (or something_happeneds) } 2581 2582findDefaultableGroups 2583 :: ( [Type] 2584 , (Bool,Bool) ) -- (Overloaded strings, extended default rules) 2585 -> WantedConstraints -- Unsolved (wanted or derived) 2586 -> [(TyVar, [Ct])] 2587findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds 2588 | null default_tys 2589 = [] 2590 | otherwise 2591 = [ (tv, map fstOf3 group) 2592 | group'@((_,_,tv) :| _) <- unary_groups 2593 , let group = toList group' 2594 , defaultable_tyvar tv 2595 , defaultable_classes (map sndOf3 group) ] 2596 where 2597 simples = approximateWC True wanteds 2598 (unaries, non_unaries) = partitionWith find_unary (bagToList simples) 2599 unary_groups = equivClasses cmp_tv unaries 2600 2601 unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints 2602 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints 2603 non_unaries :: [Ct] -- and *other* constraints 2604 2605 -- Finds unary type-class constraints 2606 -- But take account of polykinded classes like Typeable, 2607 -- which may look like (Typeable * (a:*)) (#8931) 2608 find_unary :: Ct -> Either (Ct, Class, TyVar) Ct 2609 find_unary cc 2610 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc) 2611 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys 2612 -- Ignore invisible arguments for this purpose 2613 , Just tv <- tcGetTyVar_maybe ty 2614 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and 2615 -- we definitely don't want to try to assign to those! 2616 = Left (cc, cls, tv) 2617 find_unary cc = Right cc -- Non unary or non dictionary 2618 2619 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries 2620 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries 2621 2622 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2 2623 2624 defaultable_tyvar :: TcTyVar -> Bool 2625 defaultable_tyvar tv 2626 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors] 2627 b2 = not (tv `elemVarSet` bad_tvs) 2628 in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults] 2629 2630 defaultable_classes :: [Class] -> Bool 2631 defaultable_classes clss 2632 | extended_defaults = any (isInteractiveClass ovl_strings) clss 2633 | otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss) 2634 2635 -- is_std_class adds IsString to the standard numeric classes, 2636 -- when -foverloaded-strings is enabled 2637 is_std_class cls = isStandardClass cls || 2638 (ovl_strings && (cls `hasKey` isStringClassKey)) 2639 2640------------------------------ 2641disambigGroup :: [Type] -- The default types 2642 -> (TcTyVar, [Ct]) -- All classes of the form (C a) 2643 -- sharing same type variable 2644 -> TcS Bool -- True <=> something happened, reflected in ty_binds 2645 2646disambigGroup [] _ 2647 = return False 2648disambigGroup (default_ty:default_tys) group@(the_tv, wanteds) 2649 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ]) 2650 ; fake_ev_binds_var <- TcS.newTcEvBinds 2651 ; tclvl <- TcS.getTcLevel 2652 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group 2653 2654 ; if success then 2655 -- Success: record the type variable binding, and return 2656 do { unifyTyVar the_tv default_ty 2657 ; wrapWarnTcS $ warnDefaulting wanteds default_ty 2658 ; traceTcS "disambigGroup succeeded }" (ppr default_ty) 2659 ; return True } 2660 else 2661 -- Failure: try with the next type 2662 do { traceTcS "disambigGroup failed, will try other default types }" 2663 (ppr default_ty) 2664 ; disambigGroup default_tys group } } 2665 where 2666 try_group 2667 | Just subst <- mb_subst 2668 = do { lcl_env <- TcS.getLclEnv 2669 ; tc_lvl <- TcS.getTcLevel 2670 ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env 2671 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred) 2672 wanteds 2673 ; fmap isEmptyWC $ 2674 solveSimpleWanteds $ listToBag $ 2675 map mkNonCanonical wanted_evs } 2676 2677 | otherwise 2678 = return False 2679 2680 the_ty = mkTyVarTy the_tv 2681 mb_subst = tcMatchTyKi the_ty default_ty 2682 -- Make sure the kinds match too; hence this call to tcMatchTyKi 2683 -- E.g. suppose the only constraint was (Typeable k (a::k)) 2684 -- With the addition of polykinded defaulting we also want to reject 2685 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here. 2686 2687-- In interactive mode, or with -XExtendedDefaultRules, 2688-- we default Show a to Show () to avoid graututious errors on "show []" 2689isInteractiveClass :: Bool -- -XOverloadedStrings? 2690 -> Class -> Bool 2691isInteractiveClass ovl_strings cls 2692 = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys) 2693 2694 -- isNumClass adds IsString to the standard numeric classes, 2695 -- when -foverloaded-strings is enabled 2696isNumClass :: Bool -- -XOverloadedStrings? 2697 -> Class -> Bool 2698isNumClass ovl_strings cls 2699 = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey)) 2700 2701 2702{- 2703Note [Avoiding spurious errors] 2704~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2705When doing the unification for defaulting, we check for skolem 2706type variables, and simply don't default them. For example: 2707 f = (*) -- Monomorphic 2708 g :: Num a => a -> a 2709 g x = f x x 2710Here, we get a complaint when checking the type signature for g, 2711that g isn't polymorphic enough; but then we get another one when 2712dealing with the (Num a) context arising from f's definition; 2713we try to unify a with Int (to default it), but find that it's 2714already been unified with the rigid variable from g's type sig. 2715 2716Note [Multi-parameter defaults] 2717~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2718With -XExtendedDefaultRules, we default only based on single-variable 2719constraints, but do not exclude from defaulting any type variables which also 2720appear in multi-variable constraints. This means that the following will 2721default properly: 2722 2723 default (Integer, Double) 2724 2725 class A b (c :: Symbol) where 2726 a :: b -> Proxy c 2727 2728 instance A Integer c where a _ = Proxy 2729 2730 main = print (a 5 :: Proxy "5") 2731 2732Note that if we change the above instance ("instance A Integer") to 2733"instance A Double", we get an error: 2734 2735 No instance for (A Integer "5") 2736 2737This is because the first defaulted type (Integer) has successfully satisfied 2738its single-parameter constraints (in this case Num). 2739-} 2740