c889b4b840fdc190142d2d95a87d87a59bfc7a8e
[ghc.git] / compiler / typecheck / TcSimplify.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcSimplify(
4 simplifyInfer,
5 growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, simplifyInteractive, solveEqualities,
9 simplifyWantedsTcM,
10 tcCheckSatisfiability,
11
12 -- For Rules we need these
13 solveWanteds, runTcSDeriveds
14 ) where
15
16 #include "HsVersions.h"
17
18 import Bag
19 import Class ( Class, classKey, classTyCon )
20 import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
21 , WarnReason ( Reason )
22 , DynFlags( solverIterations ) )
23 import Inst
24 import ListSetOps
25 import Maybes
26 import Name
27 import Outputable
28 import PrelInfo
29 import PrelNames
30 import TcErrors
31 import TcEvidence
32 import TcInteract
33 import TcCanonical ( makeSuperClasses, mkGivensWithSuperClasses )
34 import TcMType as TcM
35 import TcRnMonad as TcM
36 import TcSMonad as TcS
37 import TcType
38 import TrieMap () -- DV: for now
39 import Type
40 import TysWiredIn ( ptrRepLiftedTy )
41 import Unify ( tcMatchTy )
42 import Util
43 import Var
44 import VarSet
45 import UniqFM
46 import BasicTypes ( IntWithInf, intGtLimit )
47 import ErrUtils ( emptyMessages )
48 import qualified GHC.LanguageExtensions as LangExt
49
50 import Control.Monad ( when, unless )
51 import Data.List ( partition )
52
53 {-
54 *********************************************************************************
55 * *
56 * External interface *
57 * *
58 *********************************************************************************
59 -}
60
61 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
62 -- Simplify top-level constraints
63 -- Usually these will be implications,
64 -- but when there is nothing to quantify we don't wrap
65 -- in a degenerate implication, so we do that here instead
66 simplifyTop wanteds
67 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
68 ; ((final_wc, unsafe_ol), binds1) <- runTcS $
69 do { final_wc <- simpl_top wanteds
70 ; unsafe_ol <- getSafeOverlapFailures
71 ; return (final_wc, unsafe_ol) }
72 ; traceTc "End simplifyTop }" empty
73
74 ; traceTc "reportUnsolved {" empty
75 ; binds2 <- reportUnsolved final_wc
76 ; traceTc "reportUnsolved }" empty
77
78 ; traceTc "reportUnsolved (unsafe overlapping) {" empty
79 ; unless (isEmptyCts unsafe_ol) $ do {
80 -- grab current error messages and clear, warnAllUnsolved will
81 -- update error messages which we'll grab and then restore saved
82 -- messages.
83 ; errs_var <- getErrsVar
84 ; saved_msg <- TcM.readTcRef errs_var
85 ; TcM.writeTcRef errs_var emptyMessages
86
87 ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
88 , wc_insol = emptyCts
89 , wc_impl = emptyBag }
90
91 ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
92 ; TcM.writeTcRef errs_var saved_msg
93 ; recordUnsafeInfer whyUnsafe
94 }
95 ; traceTc "reportUnsolved (unsafe overlapping) }" empty
96
97 ; return (evBindMapBinds binds1 `unionBags` binds2) }
98
99 -- | Type-check a thing that emits only equality constraints, then
100 -- solve those constraints. Fails outright if there is trouble.
101 solveEqualities :: TcM a -> TcM a
102 solveEqualities thing_inside
103 = checkNoErrs $ -- See Note [Fail fast on kind errors]
104 do { (result, wanted) <- captureConstraints thing_inside
105 ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
106 ; final_wc <- runTcSEqualities $ simpl_top wanted
107 ; traceTc "End solveEqualities }" empty
108
109 ; traceTc "reportAllUnsolved {" empty
110 ; reportAllUnsolved final_wc
111 ; traceTc "reportAllUnsolved }" empty
112 ; return result }
113
114 simpl_top :: WantedConstraints -> TcS WantedConstraints
115 -- See Note [Top-level Defaulting Plan]
116 simpl_top wanteds
117 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
118 -- This is where the main work happens
119 ; try_tyvar_defaulting wc_first_go }
120 where
121 try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
122 try_tyvar_defaulting wc
123 | isEmptyWC wc
124 = return wc
125 | otherwise
126 = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
127 ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
128 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
129 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
130 -- and we definitely don't want to try to assign to those!
131 -- the isTyVar needs to weed out coercion variables
132
133 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
134 ; if or defaulted
135 then do { wc_residual <- nestTcS (solveWanteds wc)
136 -- See Note [Must simplify after defaulting]
137 ; try_class_defaulting wc_residual }
138 else try_class_defaulting wc } -- No defaulting took place
139
140 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
141 try_class_defaulting wc
142 | isEmptyWC wc
143 = return wc
144 | otherwise -- See Note [When to do type-class defaulting]
145 = do { something_happened <- applyDefaultingRules wc
146 -- See Note [Top-level Defaulting Plan]
147 ; if something_happened
148 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
149 ; try_class_defaulting wc_residual }
150 -- See Note [Overview of implicit CallStacks] in TcEvidence
151 else try_callstack_defaulting wc }
152
153 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
154 try_callstack_defaulting wc
155 | isEmptyWC wc
156 = return wc
157 | otherwise
158 = defaultCallStacks wc
159
160 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
161 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
162 -- See Note [Overview of implicit CallStacks] in TcEvidence
163 defaultCallStacks wanteds
164 = do simples <- handle_simples (wc_simple wanteds)
165 implics <- mapBagM handle_implic (wc_impl wanteds)
166 return (wanteds { wc_simple = simples, wc_impl = implics })
167
168 where
169
170 handle_simples simples
171 = catBagMaybes <$> mapBagM defaultCallStack simples
172
173 handle_implic implic = do
174 wanteds <- defaultCallStacks (ic_wanted implic)
175 return (implic { ic_wanted = wanteds })
176
177 defaultCallStack ct
178 | Just _ <- isCallStackPred (ctPred ct)
179 = do { solveCallStack (cc_ev ct) EvCsEmpty
180 ; return Nothing }
181
182 defaultCallStack ct
183 = return (Just ct)
184
185
186 {- Note [Fail fast on kind errors]
187 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
188 solveEqualities is used to solve kind equalities when kind-checking
189 user-written types. If solving fails we should fail outright, rather
190 than just accumulate an error message, for two reasons:
191
192 * A kind-bogus type signature may cause a cascade of knock-on
193 errors if we let it pass
194
195 * More seriously, we don't have a convenient term-level place to add
196 deferred bindings for unsolved kind-equality constraints, so we
197 don't build evidence bindings (by usine reportAllUnsolved). That
198 means that we'll be left with with a type that has coercion holes
199 in it, something like
200 <type> |> co-hole
201 where co-hole is not filled in. Eeek! That un-filled-in
202 hole actually causes GHC to crash with "fvProv falls into a hole"
203 See Trac #11563, #11520, #11516, #11399
204
205 So it's important to use 'checkNoErrs' here!
206
207 Note [When to do type-class defaulting]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
210 was false, on the grounds that defaulting can't help solve insoluble
211 constraints. But if we *don't* do defaulting we may report a whole
212 lot of errors that would be solved by defaulting; these errors are
213 quite spurious because fixing the single insoluble error means that
214 defaulting happens again, which makes all the other errors go away.
215 This is jolly confusing: Trac #9033.
216
217 So it seems better to always do type-class defaulting.
218
219 However, always doing defaulting does mean that we'll do it in
220 situations like this (Trac #5934):
221 run :: (forall s. GenST s) -> Int
222 run = fromInteger 0
223 We don't unify the return type of fromInteger with the given function
224 type, because the latter involves foralls. So we're left with
225 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
226 Now we do defaulting, get alpha := Integer, and report that we can't
227 match Integer with (forall s. GenST s) -> Int. That's not totally
228 stupid, but perhaps a little strange.
229
230 Another potential alternative would be to suppress *all* non-insoluble
231 errors if there are *any* insoluble errors, anywhere, but that seems
232 too drastic.
233
234 Note [Must simplify after defaulting]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 We may have a deeply buried constraint
237 (t:*) ~ (a:Open)
238 which we couldn't solve because of the kind incompatibility, and 'a' is free.
239 Then when we default 'a' we can solve the constraint. And we want to do
240 that before starting in on type classes. We MUST do it before reporting
241 errors, because it isn't an error! Trac #7967 was due to this.
242
243 Note [Top-level Defaulting Plan]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 We have considered two design choices for where/when to apply defaulting.
246 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
247 simple constraints, maybe deep inside the context of implications.
248 This used to be the case in GHC 7.4.1.
249 (ii) Do it in a tight loop at simplifyTop, once all other constraints have
250 finished. This is the current story.
251
252 Option (i) had many disadvantages:
253 a) Firstly, it was deep inside the actual solver.
254 b) Secondly, it was dependent on the context (Infer a type signature,
255 or Check a type signature, or Interactive) since we did not want
256 to always start defaulting when inferring (though there is an exception to
257 this, see Note [Default while Inferring]).
258 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
259 f :: Int -> Bool
260 f x = const True (\y -> let w :: a -> a
261 w a = const a (y+1)
262 in w y)
263 We will get an implication constraint (for beta the type of y):
264 [untch=beta] forall a. 0 => Num beta
265 which we really cannot default /while solving/ the implication, since beta is
266 untouchable.
267
268 Instead our new defaulting story is to pull defaulting out of the solver loop and
269 go with option (ii), implemented at SimplifyTop. Namely:
270 - First, have a go at solving the residual constraint of the whole
271 program
272 - Try to approximate it with a simple constraint
273 - Figure out derived defaulting equations for that simple constraint
274 - Go round the loop again if you did manage to get some equations
275
276 Now, that has to do with class defaulting. However there exists type variable /kind/
277 defaulting. Again this is done at the top-level and the plan is:
278 - At the top-level, once you had a go at solving the constraint, do
279 figure out /all/ the touchable unification variables of the wanted constraints.
280 - Apply defaulting to their kinds
281
282 More details in Note [DefaultTyVar].
283
284 Note [Safe Haskell Overlapping Instances]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 In Safe Haskell, we apply an extra restriction to overlapping instances. The
287 motive is to prevent untrusted code provided by a third-party, changing the
288 behavior of trusted code through type-classes. This is due to the global and
289 implicit nature of type-classes that can hide the source of the dictionary.
290
291 Another way to state this is: if a module M compiles without importing another
292 module N, changing M to import N shouldn't change the behavior of M.
293
294 Overlapping instances with type-classes can violate this principle. However,
295 overlapping instances aren't always unsafe. They are just unsafe when the most
296 selected dictionary comes from untrusted code (code compiled with -XSafe) and
297 overlaps instances provided by other modules.
298
299 In particular, in Safe Haskell at a call site with overlapping instances, we
300 apply the following rule to determine if it is a 'unsafe' overlap:
301
302 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
303 2) I1 is an orphan instance or a MPTC.
304 3) At least one overlapped instance, Ix, is both:
305 A) from a different module than I1
306 B) Ix is not marked `OVERLAPPABLE`
307
308 This is a slightly involved heuristic, but captures the situation of an
309 imported module N changing the behavior of existing code. For example, if
310 condition (2) isn't violated, then the module author M must depend either on a
311 type-class or type defined in N.
312
313 Secondly, when should these heuristics be enforced? We enforced them when the
314 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
315 This allows `-XUnsafe` modules to operate without restriction, and for Safe
316 Haskell inferrence to infer modules with unsafe overlaps as unsafe.
317
318 One alternative design would be to also consider if an instance was imported as
319 a `safe` import or not and only apply the restriction to instances imported
320 safely. However, since instances are global and can be imported through more
321 than one path, this alternative doesn't work.
322
323 Note [Safe Haskell Overlapping Instances Implementation]
324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
325
326 How is this implemented? It's complicated! So we'll step through it all:
327
328 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
329 we check if a particular type-class method call is safe or unsafe. We do this
330 through the return type, `ClsInstLookupResult`, where the last parameter is a
331 list of instances that are unsafe to overlap. When the method call is safe,
332 the list is null.
333
334 2) `TcInteract.matchClassInst` -- This module drives the instance resolution
335 / dictionary generation. The return type is `LookupInstResult`, which either
336 says no instance matched, or one found, and if it was a safe or unsafe
337 overlap.
338
339 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
340 tries to resolve it by calling (in part) `matchClassInst`. The resolving
341 mechanism has a work list (of constraints) that it process one at a time. If
342 the constraint can't be resolved, it's added to an inert set. When compiling
343 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
344 compilation should fail. These are handled as normal constraint resolution
345 failures from here-on (see step 6).
346
347 Otherwise, we may be inferring safety (or using `-Wunsafe`), and
348 compilation should succeed, but print warnings and/or mark the compiled module
349 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
350 the unsafe (but resolved!) constraint to the `inert_safehask` field of
351 `InertCans`.
352
353 4) `TcSimplify.simplifyTop`:
354 * Call simpl_top, the top-level function for driving the simplifier for
355 constraint resolution.
356
357 * Once finished, call `getSafeOverlapFailures` to retrieve the
358 list of overlapping instances that were successfully resolved,
359 but unsafe. Remember, this is only applicable for generating warnings
360 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
361 cause compilation failure by not resolving the unsafe constraint at all.
362
363 * For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
364 while for resolved but unsafe overlapping dictionary constraints, call
365 `TcErrors.warnAllUnsolved`. Both functions convert constraints into a
366 warning message for the user.
367
368 * In the case of `warnAllUnsolved` for resolved, but unsafe
369 dictionary constraints, we collect the generated warning
370 message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
371 mark the module we are compiling as unsafe, passing the
372 warning message along as the reason.
373
374 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by
375 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
376 know is the constraint that is unresolved or unsafe. For dictionary, all we
377 know is that we need a dictionary of type C, but not what instances are
378 available and how they overlap. So we once again call `lookupInstEnv` to
379 figure that out so we can generate a helpful error message.
380
381 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an
382 IORef called `tcg_safeInfer`.
383
384 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
385 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
386 failed.
387
388 Note [No defaulting in the ambiguity check]
389 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 When simplifying constraints for the ambiguity check, we use
391 solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
392 Trac #11947 was an example:
393 f :: Num a => Int -> Int
394 This is ambiguous of course, but we don't want to default the
395 (Num alpha) constraint to (Num Int)! Doing so gives a defaulting
396 warning, but no error.
397 -}
398
399 ------------------
400 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
401 simplifyAmbiguityCheck ty wanteds
402 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
403 ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds
404 -- NB: no defaulting! See Note [No defaulting in the ambiguity check]
405
406 ; traceTc "End simplifyAmbiguityCheck }" empty
407
408 -- Normally report all errors; but with -XAllowAmbiguousTypes
409 -- report only insoluble ones, since they represent genuinely
410 -- inaccessible code
411 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
412 ; traceTc "reportUnsolved(ambig) {" empty
413 ; tc_lvl <- TcM.getTcLevel
414 ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc))
415 (discardResult (reportUnsolved final_wc))
416 ; traceTc "reportUnsolved(ambig) }" empty
417
418 ; return () }
419
420 ------------------
421 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
422 simplifyInteractive wanteds
423 = traceTc "simplifyInteractive" empty >>
424 simplifyTop wanteds
425
426 ------------------
427 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
428 -> TcM () -- Succeeds if the constraint is soluble
429 simplifyDefault theta
430 = do { traceTc "simplifyInteractive" empty
431 ; loc <- getCtLocM DefaultOrigin Nothing
432 ; let wanted = [ CtDerived { ctev_pred = pred
433 , ctev_loc = loc }
434 | pred <- theta ]
435 ; unsolved <- runTcSDeriveds (solveWanteds (mkSimpleWC wanted))
436 ; traceTc "reportUnsolved {" empty
437 ; reportAllUnsolved unsolved
438 ; traceTc "reportUnsolved }" empty
439 ; return () }
440
441 ------------------
442 tcCheckSatisfiability :: Bag EvVar -> TcM Bool
443 -- Return True if satisfiable, False if definitely contradictory
444 tcCheckSatisfiability given_ids
445 = do { lcl_env <- TcM.getLclEnv
446 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
447 ; (res, _ev_binds) <- runTcS $
448 do { traceTcS "checkSatisfiability {" (ppr given_ids)
449 ; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
450 -- See Note [Superclasses and satisfiability]
451 ; insols <- solveSimpleGivens given_cts
452 ; insols <- try_harder insols
453 ; traceTcS "checkSatisfiability }" (ppr insols)
454 ; return (isEmptyBag insols) }
455 ; return res }
456 where
457 try_harder :: Cts -> TcS Cts
458 -- Maybe we have to search up the superclass chain to find
459 -- an unsatisfiable constraint. Example: pmcheck/T3927b.
460 -- At the moment we try just once
461 try_harder insols
462 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
463 = return insols -- Hurrah -- stop now.
464 | otherwise
465 = do { pending_given <- getPendingScDicts
466 ; new_given <- makeSuperClasses pending_given
467 ; solveSimpleGivens new_given }
468
469 {- Note [Superclasses and satisfiability]
470 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
471 Expand superclasses before starting, because (Int ~ Bool), has
472 (Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
473 as a superclass, and it's the latter that is insoluble. See
474 Note [The equality types story] in TysPrim.
475
476 If we fail to prove unsatisfiability we (arbitrarily) try just once to
477 find superclasses, using try_harder. Reason: we might have a type
478 signature
479 f :: F op (Implements push) => ..
480 where F is a type function. This happened in Trac #3972.
481
482 We could do more than once but we'd have to have /some/ limit: in the
483 the recurisve case, we would go on forever in the common case where
484 the constraints /are/ satisfiable (Trac #10592 comment:12!).
485
486 For stratightforard situations without type functions the try_harder
487 step does nothing.
488
489
490 ***********************************************************************************
491 * *
492 * Inference
493 * *
494 ***********************************************************************************
495
496 Note [Inferring the type of a let-bound variable]
497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 Consider
499 f x = rhs
500
501 To infer f's type we do the following:
502 * Gather the constraints for the RHS with ambient level *one more than*
503 the current one. This is done by the call
504 pushLevelAndCaptureConstraints (tcMonoBinds...)
505 in TcBinds.tcPolyInfer
506
507 * Call simplifyInfer to simplify the constraints and decide what to
508 quantify over. We pass in the level used for the RHS constraints,
509 here called rhs_tclvl.
510
511 This ensures that the implication constraint we generate, if any,
512 has a strictly-increased level compared to the ambient level outside
513 the let binding.
514
515 -}
516
517 simplifyInfer :: TcLevel -- Used when generating the constraints
518 -> Bool -- Apply monomorphism restriction
519 -> [TcIdSigInfo] -- Any signatures (possibly partial)
520 -> [(Name, TcTauType)] -- Variables to be generalised,
521 -- and their tau-types
522 -> WantedConstraints
523 -> TcM ([TcTyVar], -- Quantify over these type variables
524 [EvVar], -- ... and these constraints (fully zonked)
525 TcEvBinds) -- ... binding these evidence variables
526 simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
527 | isEmptyWC wanteds
528 = do { gbl_tvs <- tcGetGlobalTyCoVars
529 ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
530 ; qtkvs <- quantifyZonkedTyVars gbl_tvs dep_vars
531 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
532 ; return (qtkvs, [], emptyTcEvBinds) }
533
534 | otherwise
535 = do { traceTc "simplifyInfer {" $ vcat
536 [ text "sigs =" <+> ppr sigs
537 , text "binds =" <+> ppr name_taus
538 , text "rhs_tclvl =" <+> ppr rhs_tclvl
539 , text "apply_mr =" <+> ppr apply_mr
540 , text "(unzonked) wanted =" <+> ppr wanteds
541 ]
542
543 ; let partial_sigs = filter isPartialSig sigs
544 psig_theta = concatMap sig_theta partial_sigs
545
546 -- First do full-blown solving
547 -- NB: we must gather up all the bindings from doing
548 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
549 -- And note that since there are nested implications,
550 -- calling solveWanteds will side-effect their evidence
551 -- bindings, so we can't just revert to the input
552 -- constraint.
553
554 ; tc_lcl_env <- TcM.getLclEnv
555 ; ev_binds_var <- TcM.newTcEvBinds
556 ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
557 ; wanted_transformed_incl_derivs
558 <- setTcLevel rhs_tclvl $
559 runTcSWithEvBinds False (Just ev_binds_var) $
560 do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
561 ; psig_givens <- mkGivensWithSuperClasses loc psig_theta_vars
562 ; _ <- solveSimpleGivens psig_givens
563 -- See Note [Add signature contexts as givens]
564 ; solveWanteds wanteds }
565 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
566
567 -- Find quant_pred_candidates, the predicates that
568 -- we'll consider quantifying over
569 -- NB1: wanted_transformed does not include anything provable from
570 -- the psig_theta; it's just the extra bit
571 -- NB2: We do not do any defaulting when inferring a type, this can lead
572 -- to less polymorphic types, see Note [Default while Inferring]
573
574 ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
575 ; quant_pred_candidates -- Fully zonked
576 <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs
577 then return [] -- See Note [Quantification with errors]
578 -- NB: must include derived errors in this test,
579 -- hence "incl_derivs"
580
581 else do { let quant_cand = approximateWC wanted_transformed
582 meta_tvs = filter isMetaTyVar $
583 tyCoVarsOfCtsList quant_cand
584
585 ; gbl_tvs <- tcGetGlobalTyCoVars
586 -- Miminise quant_cand. We are not interested in any evidence
587 -- produced, because we are going to simplify wanted_transformed
588 -- again later. All we want here are the predicates over which to
589 -- quantify.
590 --
591 -- If any meta-tyvar unifications take place (unlikely),
592 -- we'll pick that up later.
593
594 -- See Note [Promote _and_ default when inferring]
595 ; let def_tyvar tv
596 = when (not $ tv `elemVarSet` gbl_tvs) $
597 defaultTyVar tv
598 ; mapM_ def_tyvar meta_tvs
599 ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
600
601 ; WC { wc_simple = simples }
602 <- setTcLevel rhs_tclvl $
603 runTcSDeriveds $
604 solveSimpleWanteds $
605 mapBag toDerivedCt quant_cand
606 -- NB: we don't want evidence,
607 -- so use Derived constraints
608
609 ; simples <- TcM.zonkSimples simples
610
611 ; return [ ctEvPred ev | ct <- bagToList simples
612 , let ev = ctEvidence ct ] }
613
614 -- NB: quant_pred_candidates is already fully zonked
615
616 -- Decide what type variables and constraints to quantify
617 -- NB: bound_theta are constraints we want to quantify over,
618 -- /apart from/ the psig_theta, which we always quantify over
619 ; (qtvs, bound_theta) <- decideQuantification apply_mr name_taus psig_theta
620 quant_pred_candidates
621
622 -- Promote any type variables that are free in the inferred type
623 -- of the function:
624 -- f :: forall qtvs. bound_theta => zonked_tau
625 -- These variables now become free in the envt, and hence will show
626 -- up whenever 'f' is called. They may currently at rhs_tclvl, but
627 -- they had better be unifiable at the outer_tclvl!
628 -- Example: envt mentions alpha[1]
629 -- tau_ty = beta[2] -> beta[2]
630 -- consraints = alpha ~ [beta]
631 -- we don't quantify over beta (since it is fixed by envt)
632 -- so we must promote it! The inferred type is just
633 -- f :: beta -> beta
634 ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
635 -- decideQuantification turned some meta tyvars into
636 -- quantified skolems, so we have to zonk again
637
638 ; let phi_tkvs = tyCoVarsOfTypes bound_theta -- Already zonked
639 `unionVarSet` tyCoVarsOfTypes zonked_taus
640 promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
641
642 ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
643 , ppr phi_tkvs $$
644 ppr (closeOverKinds phi_tkvs) $$
645 ppr promote_tkvs $$
646 ppr (closeOverKinds promote_tkvs) )
647 -- we really don't want a type to be promoted when its kind isn't!
648
649 -- promoteTyVar ignores coercion variables
650 ; outer_tclvl <- TcM.getTcLevel
651 ; mapM_ (promoteTyVar outer_tclvl) (nonDetEltsUFM promote_tkvs)
652 -- It's OK to use nonDetEltsUFM here because promoteTyVar is
653 -- commutative
654
655 -- Emit an implication constraint for the
656 -- remaining constraints from the RHS
657 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
658 ; psig_theta_vars <- mapM zonkId psig_theta_vars
659 ; let full_theta = psig_theta ++ bound_theta
660 full_theta_vars = psig_theta_vars ++ bound_theta_vars
661 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
662 | (name, ty) <- name_taus ]
663 -- Don't add the quantified variables here, because
664 -- they are also bound in ic_skols and we want them
665 -- to be tidied uniformly
666
667 -- extra_qtvs: see Note [Quantification and partial signatures]
668 extra_qtvs = [ tv | sig <- partial_sigs
669 , (_, tv) <- sig_skols sig
670 , not (tv `elem` qtvs) ]
671
672 implic = Implic { ic_tclvl = rhs_tclvl
673 , ic_skols = extra_qtvs ++ qtvs
674 , ic_no_eqs = False
675 , ic_given = full_theta_vars
676 , ic_wanted = wanted_transformed
677 , ic_status = IC_Unsolved
678 , ic_binds = Just ev_binds_var
679 , ic_info = skol_info
680 , ic_env = tc_lcl_env }
681 ; emitImplication implic
682
683 -- All done!
684 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
685 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
686 , text "promote_tvs=" <+> ppr promote_tkvs
687 , text "psig_theta =" <+> ppr psig_theta
688 , text "bound_theta =" <+> ppr bound_theta
689 , text "full_theta =" <+> ppr full_theta
690 , text "qtvs =" <+> ppr qtvs
691 , text "implic =" <+> ppr implic ]
692
693 ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
694
695 {- Note [Add signature contexts as givens]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 Consider this (Trac #11016):
698 f2 :: (?x :: Int) => _
699 f2 = ?x
700 or this
701 f3 :: a ~ Bool => (a, _)
702 f3 = (True, False)
703 or theis
704 f4 :: (Ord a, _) => a -> Bool
705 f4 x = x==x
706
707 We'll use plan InferGen because there are holes in the type. But:
708 * For f2 we want to have the (?x :: Int) constraint floating around
709 so that the functional dependencies kick in. Otherwise the
710 occurrence of ?x on the RHS produces constraint (?x :: alpha), and
711 we won't unify alpha:=Int.
712 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
713 in the RHS
714 * For f4 we want to use the (Ord a) in the signature to solve the Eq a
715 constraint.
716
717 Solution: in simplifyInfer, just before simplifying the constraints
718 gathered from the RHS, add Given constraints for the context of any
719 type signatures.
720
721 ************************************************************************
722 * *
723 Quantification
724 * *
725 ************************************************************************
726
727 Note [Deciding quantification]
728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
729 If the monomorphism restriction does not apply, then we quantify as follows:
730 * Take the global tyvars, and "grow" them using the equality constraints
731 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
732 happen because alpha is untouchable here) then do not quantify over
733 beta, because alpha fixes beta, and beta is effectively free in
734 the environment too
735 These are the mono_tvs
736
737 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
738 using all the constraints. These are tau_tvs_plus
739
740 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
741 careful to close over kinds, and to skolemise the quantified tyvars.
742 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
743 Result is qtvs.
744
745 * Filter the constraints using pickQuantifiablePreds and the qtvs.
746 We have to zonk the constraints first, so they "see" the freshly
747 created skolems.
748
749 If the MR does apply, mono_tvs includes all the constrained tyvars --
750 including all covars -- and the quantified constraints are empty/insoluble.
751
752 -}
753
754 decideQuantification
755 :: Bool -- try the MR restriction?
756 -> [(Name, TcTauType)] -- Variables to be generalised
757 -> [PredType] -- All annotated constraints from signatures
758 -> [PredType] -- Candidate theta
759 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
760 , [PredType] ) -- and this context (fully zonked)
761 -- See Note [Deciding quantification]
762 decideQuantification apply_mr name_taus psig_theta constraints
763 | apply_mr -- Apply the Monomorphism restriction
764 = do { gbl_tvs <- tcGetGlobalTyCoVars
765 ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
766 -- psig_theta: see Note [Quantification and partial signatures]
767 ; let zonked_dvs = splitDepVarsOfTypes zonked_taus
768 zonked_tkvs = tcDepVarSet zonked_dvs
769 constrained_tvs = tyCoVarsOfTypes constraints `unionVarSet`
770 filterVarSet isCoVar zonked_tkvs
771 mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
772
773 ; qtvs <- quantifyZonkedTyVars mono_tvs zonked_dvs
774
775 -- Warn about the monomorphism restriction
776 ; warn_mono <- woptM Opt_WarnMonomorphism
777 ; let mr_bites = constrained_tvs `intersectsVarSet` zonked_tkvs
778 ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
779 hang (text "The Monomorphism Restriction applies to the binding"
780 <> plural bndrs <+> text "for" <+> pp_bndrs)
781 2 (text "Consider giving a type signature for"
782 <+> if isSingleton bndrs then pp_bndrs
783 else text "these binders")
784
785 -- All done
786 ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
787 , ppr qtvs, ppr mr_bites])
788 ; return (qtvs, []) }
789
790 | otherwise
791 = do { gbl_tvs <- tcGetGlobalTyCoVars
792 ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
793 -- psig_theta: see Note [Quantification and partial signatures]
794 ; let DV { dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
795 mono_tvs = growThetaTyVars equality_constraints gbl_tvs
796 tau_tvs_plus = growThetaTyVarsDSet constraints ztvs
797 dvs_plus = DV { dv_kvs = zkvs, dv_tvs = tau_tvs_plus }
798 ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
799 -- We don't grow the kvs, as there's no real need to. Recall
800 -- that quantifyTyVars uses the separation between kvs and tvs
801 -- only for defaulting, and we don't want (ever) to default a tv
802 -- to *. So, don't grow the kvs.
803
804 ; constraints <- TcM.zonkTcTypes constraints
805 -- quantifyTyVars turned some meta tyvars into
806 -- quantified skolems, so we have to zonk again
807
808 ; let qtv_set = mkVarSet qtvs
809 theta = pickQuantifiablePreds qtv_set constraints
810 min_theta = mkMinimalBySCs theta
811 -- See Note [Minimize by Superclasses]
812
813 ; traceTc "decideQuantification 2"
814 (vcat [ text "constraints:" <+> ppr constraints
815 , text "gbl_tvs:" <+> ppr gbl_tvs
816 , text "mono_tvs:" <+> ppr mono_tvs
817 , text "tau_tvs_plus:" <+> ppr tau_tvs_plus
818 , text "qtvs:" <+> ppr qtvs
819 , text "min_theta:" <+> ppr min_theta ])
820 ; return (qtvs, min_theta) }
821 where
822 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
823 equality_constraints = filter isEqPred constraints
824 (bndrs, taus) = unzip name_taus
825
826 ------------------
827 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
828 -- See Note [Growing the tau-tvs using constraints]
829 -- NB: only returns tyvars, never covars
830 growThetaTyVars theta tvs
831 | null theta = tvs_only
832 | otherwise = filterVarSet isTyVar $
833 transCloVarSet mk_next seed_tvs
834 where
835 tvs_only = filterVarSet isTyVar tvs
836 seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
837 (ips, non_ips) = partition isIPPred theta
838 -- See Note [Inheriting implicit parameters] in TcType
839
840 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
841 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
842 grow_one so_far pred tvs
843 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
844 | otherwise = tvs
845 where
846 pred_tvs = tyCoVarsOfType pred
847
848 ------------------
849 growThetaTyVarsDSet :: ThetaType -> DTyCoVarSet -> DTyVarSet
850 -- See Note [Growing the tau-tvs using constraints]
851 -- NB: only returns tyvars, never covars
852 -- It takes a deterministic set of TyCoVars and returns a deterministic set
853 -- of TyVars.
854 -- The implementation mirrors growThetaTyVars, the only difference is that
855 -- it avoids unionDVarSet and uses more efficient extendDVarSetList.
856 growThetaTyVarsDSet theta tvs
857 | null theta = tvs_only
858 | otherwise = filterDVarSet isTyVar $
859 transCloDVarSet mk_next seed_tvs
860 where
861 tvs_only = filterDVarSet isTyVar tvs
862 seed_tvs = tvs `extendDVarSetList` tyCoVarsOfTypesList ips
863 (ips, non_ips) = partition isIPPred theta
864 -- See Note [Inheriting implicit parameters] in TcType
865
866 mk_next :: DVarSet -> DVarSet -- Maps current set to newly-grown ones
867 mk_next so_far = foldr (grow_one so_far) emptyDVarSet non_ips
868 grow_one so_far pred tvs
869 | any (`elemDVarSet` so_far) pred_tvs = tvs `extendDVarSetList` pred_tvs
870 | otherwise = tvs
871 where
872 pred_tvs = tyCoVarsOfTypeList pred
873
874 {- Note [Quantification and partial signatures]
875 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
876 When choosing type variables to quantify, the basic plan is to
877 quantify over all type variables that are
878 * free in the tau_tvs, and
879 * not forced to be monomorphic (mono_tvs),
880 for example by being free in the environment.
881
882 However, in the case of a partial type signature, be doing inference
883 *in the presence of a type signature*. For example:
884 f :: _ -> a
885 f x = ...
886 or
887 g :: (Eq _a) => _b -> _b
888 In both cases we use plan InferGen, and hence call simplifyInfer.
889 But those 'a' variables are skolems, and we should be sure to quantify
890 over them, for two reasons
891
892 * In the case of a type error
893 f :: _ -> Maybe a
894 f x = True && x
895 The inferred type of 'f' is f :: Bool -> Bool, but there's a
896 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
897 machine expects to find a binding site for the skolem 'a', so we
898 add it to the ic_skols of the residual implication.
899
900 Note that we /only/ do this to the residual implication. We don't
901 complicate the quantified type varialbes of 'f' for downstream code;
902 it's just a device to make the error message generator know what to
903 report.
904
905 * Consider the partial type signature
906 f :: (Eq _) => Int -> Int
907 f x = x
908 In normal cases that makes sense; e.g.
909 g :: Eq _a => _a -> _a
910 g x = x
911 where the signature makes the type less general than it could
912 be. But for 'f' we must therefore quantify over the user-annotated
913 constraints, to get
914 f :: forall a. Eq a => Int -> Int
915 (thereby correctly triggering an ambiguity error later). If we don't
916 we'll end up with a strange open type
917 f :: Eq alpha => Int -> Int
918 which isn't ambiguous but is still very wrong. That's why include
919 psig_theta in the variables to quantify over, passed to
920 decideQuantification.
921
922 Note [Quantifying over equality constraints]
923 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
924 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
925 Doing so may simply postpone a type error from the function definition site to
926 its call site. (At worst, imagine (Int ~ Bool)).
927
928 However, consider this
929 forall a. (F [a] ~ Int) => blah
930 Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
931 site we will know 'a', and perhaps we have instance F [Bool] = Int.
932 So we *do* quantify over a type-family equality where the arguments mention
933 the quantified variables.
934
935 Note [Growing the tau-tvs using constraints]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 (growThetaTyVars insts tvs) is the result of extending the set
938 of tyvars, tvs, using all conceivable links from pred
939
940 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
941 Then growThetaTyVars preds tvs = {a,b,c}
942
943 Notice that
944 growThetaTyVars is conservative if v might be fixed by vs
945 => v `elem` grow(vs,C)
946
947 Note [Quantification with errors]
948 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
949 If we find that the RHS of the definition has some absolutely-insoluble
950 constraints, we abandon all attempts to find a context to quantify
951 over, and instead make the function fully-polymorphic in whatever
952 type we have found. For two reasons
953 a) Minimise downstream errors
954 b) Avoid spurious errors from this function
955
956 But NB that we must include *derived* errors in the check. Example:
957 (a::*) ~ Int#
958 We get an insoluble derived error *~#, and we don't want to discard
959 it before doing the isInsolubleWC test! (Trac #8262)
960
961 Note [Default while Inferring]
962 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
963 Our current plan is that defaulting only happens at simplifyTop and
964 not simplifyInfer. This may lead to some insoluble deferred constraints.
965 Example:
966
967 instance D g => C g Int b
968
969 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
970 type inferred = gamma -> gamma
971
972 Now, if we try to default (alpha := Int) we will be able to refine the implication to
973 (forall b. 0 => C gamma Int b)
974 which can then be simplified further to
975 (forall b. 0 => D gamma)
976 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
977 type: forall g. D g => g -> g
978
979 Instead what will currently happen is that we will get a quantified type
980 (forall g. g -> g) and an implication:
981 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
982
983 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
984 unsolvable implication:
985 forall g. 0 => (forall b. 0 => D g)
986
987 The concrete example would be:
988 h :: C g a s => g -> a -> ST s a
989 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
990
991 But it is quite tedious to do defaulting and resolve the implication constraints, and
992 we have not observed code breaking because of the lack of defaulting in inference, so
993 we don't do it for now.
994
995
996
997 Note [Minimize by Superclasses]
998 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
999 When we quantify over a constraint, in simplifyInfer we need to
1000 quantify over a constraint that is minimal in some sense: For
1001 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
1002 we'd like to quantify over Ord alpha, because we can just get Eq alpha
1003 from superclass selection from Ord alpha. This minimization is what
1004 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
1005 to check the original wanted.
1006
1007
1008 Note [Avoid unnecessary constraint simplification]
1009 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1010 -------- NB NB NB (Jun 12) -------------
1011 This note not longer applies; see the notes with Trac #4361.
1012 But I'm leaving it in here so we remember the issue.)
1013 ----------------------------------------
1014 When inferring the type of a let-binding, with simplifyInfer,
1015 try to avoid unnecessarily simplifying class constraints.
1016 Doing so aids sharing, but it also helps with delicate
1017 situations like
1018
1019 instance C t => C [t] where ..
1020
1021 f :: C [t] => ....
1022 f x = let g y = ...(constraint C [t])...
1023 in ...
1024 When inferring a type for 'g', we don't want to apply the
1025 instance decl, because then we can't satisfy (C t). So we
1026 just notice that g isn't quantified over 't' and partition
1027 the constraints before simplifying.
1028
1029 This only half-works, but then let-generalisation only half-works.
1030
1031 *********************************************************************************
1032 * *
1033 * Main Simplifier *
1034 * *
1035 ***********************************************************************************
1036
1037 -}
1038
1039 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
1040 -- Solve the specified Wanted constraints
1041 -- Discard the evidence binds
1042 -- Discards all Derived stuff in result
1043 -- Postcondition: fully zonked and unflattened constraints
1044 simplifyWantedsTcM wanted
1045 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
1046 ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted)
1047 ; result <- TcM.zonkWC result
1048 ; traceTc "simplifyWantedsTcM }" (ppr result)
1049 ; return result }
1050
1051 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1052 -- Since solveWanteds returns the residual WantedConstraints,
1053 -- it should always be called within a runTcS or something similar,
1054 -- Result is not zonked
1055 solveWantedsAndDrop wanted
1056 = do { wc <- solveWanteds wanted
1057 ; return (dropDerivedWC wc) }
1058
1059 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1060 -- so that the inert set doesn't mindlessly propagate.
1061 -- NB: wc_simples may be wanted /or/ derived now
1062 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1063 = do { traceTcS "solveWanteds {" (ppr wc)
1064
1065 -- Try the simple bit, including insolubles. Solving insolubles a
1066 -- second time round is a bit of a waste; but the code is simple
1067 -- and the program is wrong anyway, and we don't run the danger
1068 -- of adding Derived insolubles twice; see
1069 -- TcSMonad Note [Do not add duplicate derived insolubles]
1070 ; wc1 <- solveSimpleWanteds simples
1071 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1072 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1073
1074 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
1075
1076 ; dflags <- getDynFlags
1077 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
1078 (WC { wc_simple = simples1, wc_impl = implics2
1079 , wc_insol = insols `unionBags` insols1 })
1080
1081 ; bb <- TcS.getTcEvBindsMap
1082 ; traceTcS "solveWanteds }" $
1083 vcat [ text "final wc =" <+> ppr final_wc
1084 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1085
1086 ; return final_wc }
1087
1088 simpl_loop :: Int -> IntWithInf -> Cts -> Bool
1089 -> WantedConstraints
1090 -> TcS WantedConstraints
1091 simpl_loop n limit floated_eqs no_new_scs
1092 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1093 | isEmptyBag floated_eqs && no_new_scs
1094 = return wc -- Done!
1095
1096 | n `intGtLimit` limit
1097 = do { -- Add an error (not a warning) if we blow the limit,
1098 -- Typically if we blow the limit we are going to report some other error
1099 -- (an unsolved constraint), and we don't want that error to suppress
1100 -- the iteration limit warning!
1101 addErrTcS (hang (text "solveWanteds: too many iterations"
1102 <+> parens (text "limit =" <+> ppr limit))
1103 2 (vcat [ text "Unsolved:" <+> ppr wc
1104 , ppUnless (isEmptyBag floated_eqs) $
1105 text "Floated equalities:" <+> ppr floated_eqs
1106 , ppUnless no_new_scs $
1107 text "New superclasses found"
1108 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
1109 ]))
1110 ; return wc }
1111
1112 | otherwise
1113 = do { let n_floated = lengthBag floated_eqs
1114 ; csTraceTcS $
1115 text "simpl_loop iteration=" <> int n
1116 <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma
1117 , int n_floated <+> text "floated eqs" <> comma
1118 , int (lengthBag simples) <+> text "simples to solve" ])
1119
1120 -- solveSimples may make progress if either float_eqs hold
1121 ; (unifs1, wc1) <- reportUnifications $
1122 solveSimpleWanteds (floated_eqs `unionBags` simples)
1123 -- Put floated_eqs first so they get solved first
1124 -- NB: the floated_eqs may include /derived/ equalities
1125 -- arising from fundeps inside an implication
1126
1127 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1128 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1129
1130 -- We have already tried to solve the nested implications once
1131 -- Try again only if we have unified some meta-variables
1132 -- (which is a bit like adding more givens
1133 -- See Note [Cutting off simpl_loop]
1134 ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
1135 then return (emptyBag, implics)
1136 else solveNestedImplications (implics `unionBags` implics1)
1137
1138 ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
1139 (WC { wc_simple = simples1, wc_impl = implics2
1140 , wc_insol = insols `unionBags` insols1 }) }
1141
1142 expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
1143 -- If there are any unsolved wanteds, expand one step of superclasses for
1144 -- unsolved wanteds or givens
1145 -- See Note [The superclass story] in TcCanonical
1146 expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
1147 | not (anyBag superClassesMightHelp unsolved)
1148 = return (True, wc)
1149 | otherwise
1150 = do { traceTcS "expandSuperClasses {" empty
1151 ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
1152 get acc ct = case isPendingScDict ct of
1153 Just ct' -> (ct':acc, ct')
1154 Nothing -> (acc, ct)
1155 ; pending_given <- getPendingScDicts
1156 ; if null pending_given && null pending_wanted
1157 then do { traceTcS "End expandSuperClasses no-op }" empty
1158 ; return (True, wc) }
1159 else
1160 do { new_given <- makeSuperClasses pending_given
1161 ; new_insols <- solveSimpleGivens new_given
1162 ; new_wanted <- makeSuperClasses pending_wanted
1163 ; traceTcS "End expandSuperClasses }"
1164 (vcat [ text "Given:" <+> ppr pending_given
1165 , text "Insols from given:" <+> ppr new_insols
1166 , text "Wanted:" <+> ppr new_wanted ])
1167 ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
1168 , wc_insol = insols `unionBags` new_insols }) } }
1169
1170 solveNestedImplications :: Bag Implication
1171 -> TcS (Cts, Bag Implication)
1172 -- Precondition: the TcS inerts may contain unsolved simples which have
1173 -- to be converted to givens before we go inside a nested implication.
1174 solveNestedImplications implics
1175 | isEmptyBag implics
1176 = return (emptyBag, emptyBag)
1177 | otherwise
1178 = do { traceTcS "solveNestedImplications starting {" empty
1179 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
1180 ; let floated_eqs = concatBag floated_eqs_s
1181
1182 -- ... and we are back in the original TcS inerts
1183 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1184 -- them in the beginning of this function.
1185 ; traceTcS "solveNestedImplications end }" $
1186 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
1187 , text "unsolved_implics =" <+> ppr unsolved_implics ]
1188
1189 ; return (floated_eqs, catBagMaybes unsolved_implics) }
1190
1191 solveImplication :: Implication -- Wanted
1192 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
1193 Maybe Implication) -- Simplified implication (empty or singleton)
1194 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1195 -- which after trying to solve this implication we must restore to their original value
1196 solveImplication imp@(Implic { ic_tclvl = tclvl
1197 , ic_binds = m_ev_binds
1198 , ic_skols = skols
1199 , ic_given = given_ids
1200 , ic_wanted = wanteds
1201 , ic_info = info
1202 , ic_status = status
1203 , ic_env = env })
1204 | IC_Solved {} <- status
1205 = return (emptyCts, Just imp) -- Do nothing
1206
1207 | otherwise -- Even for IC_Insoluble it is worth doing more work
1208 -- The insoluble stuff might be in one sub-implication
1209 -- and other unsolved goals in another; and we want to
1210 -- solve the latter as much as possible
1211 = do { inerts <- getTcSInerts
1212 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1213
1214 -- Solve the nested constraints
1215 ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
1216 <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
1217 do { let loc = mkGivenLoc tclvl info env
1218 ; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
1219 ; given_insols <- solveSimpleGivens givens_w_scs
1220
1221 ; residual_wanted <- solveWanteds wanteds
1222 -- solveWanteds, *not* solveWantedsAndDrop, because
1223 -- we want to retain derived equalities so we can float
1224 -- them out in floatEqualities
1225
1226 ; no_eqs <- getNoGivenEqs tclvl skols
1227 -- Call getNoGivenEqs /after/ solveWanteds, because
1228 -- solveWanteds can augment the givens, via expandSuperClasses,
1229 -- to reveal given superclass equalities
1230
1231 ; return (no_eqs, given_insols, residual_wanted) }
1232
1233 ; (floated_eqs, residual_wanted)
1234 <- floatEqualities skols no_given_eqs residual_wanted
1235
1236 ; traceTcS "solveImplication 2"
1237 (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs)
1238 ; let final_wanted = residual_wanted `addInsols` given_insols
1239
1240 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
1241 , ic_wanted = final_wanted })
1242 used_tcvs
1243
1244 ; evbinds <- TcS.getTcEvBindsMap
1245 ; traceTcS "solveImplication end }" $ vcat
1246 [ text "no_given_eqs =" <+> ppr no_given_eqs
1247 , text "floated_eqs =" <+> ppr floated_eqs
1248 , text "res_implic =" <+> ppr res_implic
1249 , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
1250
1251 ; return (floated_eqs, res_implic) }
1252
1253 ----------------------
1254 setImplicationStatus :: Implication -> TyCoVarSet -- needed variables
1255 -> TcS (Maybe Implication)
1256 -- Finalise the implication returned from solveImplication:
1257 -- * Set the ic_status field
1258 -- * Trim the ic_wanted field to remove Derived constraints
1259 -- Return Nothing if we can discard the implication altogether
1260 setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
1261 , ic_info = info
1262 , ic_tclvl = tc_lvl
1263 , ic_wanted = wc
1264 , ic_given = givens })
1265 used_tcvs
1266 | some_insoluble
1267 = return $ Just $
1268 implic { ic_status = IC_Insoluble
1269 , ic_wanted = wc { wc_simple = pruned_simples
1270 , wc_insol = pruned_insols } }
1271
1272 | some_unsolved
1273 = return $ Just $
1274 implic { ic_status = IC_Unsolved
1275 , ic_wanted = wc { wc_simple = pruned_simples
1276 , wc_insol = pruned_insols } }
1277
1278 | otherwise -- Everything is solved; look at the implications
1279 -- See Note [Tracking redundant constraints]
1280 = do { ev_binds <- case m_ev_binds_var of
1281 Just (EvBindsVar ref _) -> TcS.readTcRef ref
1282 Nothing -> return emptyEvBindMap
1283 ; let all_needs = neededEvVars ev_binds
1284 (used_tcvs `unionVarSet` implic_needs)
1285
1286 dead_givens | warnRedundantGivens info
1287 = filterOut (`elemVarSet` all_needs) givens
1288 | otherwise = [] -- None to report
1289
1290 final_needs = all_needs `delVarSetList` givens
1291
1292 discard_entire_implication -- Can we discard the entire implication?
1293 = null dead_givens -- No warning from this implication
1294 && isEmptyBag pruned_implics -- No live children
1295 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
1296
1297 final_status = IC_Solved { ics_need = final_needs
1298 , ics_dead = dead_givens }
1299 final_implic = implic { ic_status = final_status
1300 , ic_wanted = wc { wc_simple = pruned_simples
1301 , wc_insol = pruned_insols
1302 , wc_impl = pruned_implics } }
1303 -- We can only prune the child implications (pruned_implics)
1304 -- in the IC_Solved status case, because only then we can
1305 -- accumulate their needed evidence variales into the
1306 -- IC_Solved final_status field of the parent implication.
1307
1308 ; return $ if discard_entire_implication
1309 then Nothing
1310 else Just final_implic }
1311 where
1312 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
1313
1314 some_insoluble = insolubleWC tc_lvl wc
1315 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
1316 || isNothing mb_implic_needs
1317
1318 pruned_simples = dropDerivedSimples simples
1319 pruned_insols = dropDerivedInsols insols
1320 pruned_implics = filterBag need_to_keep_implic implics
1321
1322 mb_implic_needs :: Maybe VarSet
1323 -- Just vs => all implics are IC_Solved, with 'vs' needed
1324 -- Nothing => at least one implic is not IC_Solved
1325 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
1326 Just implic_needs = mb_implic_needs
1327
1328 add_implic implic acc
1329 | Just vs_acc <- acc
1330 , IC_Solved { ics_need = vs } <- ic_status implic
1331 = Just (vs `unionVarSet` vs_acc)
1332 | otherwise = Nothing
1333
1334 need_to_keep_implic ic
1335 | IC_Solved { ics_dead = [] } <- ic_status ic
1336 -- Fully solved, and no redundant givens to report
1337 , isEmptyBag (wc_impl (ic_wanted ic))
1338 -- And no children that might have things to report
1339 = False
1340 | otherwise
1341 = True
1342
1343 warnRedundantGivens :: SkolemInfo -> Bool
1344 warnRedundantGivens (SigSkol ctxt _)
1345 = case ctxt of
1346 FunSigCtxt _ warn_redundant -> warn_redundant
1347 ExprSigCtxt -> True
1348 _ -> False
1349
1350 -- To think about: do we want to report redundant givens for
1351 -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
1352 warnRedundantGivens (InstSkol {}) = True
1353 warnRedundantGivens _ = False
1354
1355 neededEvVars :: EvBindMap -> VarSet -> VarSet
1356 -- Find all the evidence variables that are "needed",
1357 -- and then delete all those bound by the evidence bindings
1358 -- See note [Tracking redundant constraints]
1359 neededEvVars ev_binds initial_seeds
1360 = needed `minusVarSet` bndrs
1361 where
1362 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
1363 needed = transCloVarSet also_needs seeds
1364 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
1365
1366 add_wanted :: EvBind -> VarSet -> VarSet
1367 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1368 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1369 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1370
1371 also_needs :: VarSet -> VarSet
1372 also_needs needs
1373 = nonDetFoldUFM add emptyVarSet needs
1374 -- It's OK to use nonDetFoldUFM here because we immediately forget
1375 -- about the ordering by creating a set
1376 where
1377 add v needs
1378 | Just ev_bind <- lookupEvBind ev_binds v
1379 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
1380 , is_given
1381 = evVarsOfTerm rhs `unionVarSet` needs
1382 | otherwise
1383 = needs
1384
1385 add_bndr :: EvBind -> VarSet -> VarSet
1386 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
1387
1388
1389 {-
1390 Note [Tracking redundant constraints]
1391 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1392 With Opt_WarnRedundantConstraints, GHC can report which
1393 constraints of a type signature (or instance declaration) are
1394 redundant, and can be omitted. Here is an overview of how it
1395 works:
1396
1397 ----- What is a redundant constraint?
1398
1399 * The things that can be redundant are precisely the Given
1400 constraints of an implication.
1401
1402 * A constraint can be redundant in two different ways:
1403 a) It is implied by other givens. E.g.
1404 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1405 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1406 b) It is not needed by the Wanted constraints covered by the
1407 implication E.g.
1408 f :: Eq a => a -> Bool
1409 f x = True -- Equality not used
1410
1411 * To find (a), when we have two Given constraints,
1412 we must be careful to drop the one that is a naked variable (if poss).
1413 So if we have
1414 f :: (Eq a, Ord a) => blah
1415 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1416 [G] d2 :: Eq a
1417 We want to discard d2 in favour of the superclass selection from
1418 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1419 See Note [Replacement vs keeping].
1420
1421 * To find (b) we need to know which evidence bindings are 'wanted';
1422 hence the eb_is_given field on an EvBind.
1423
1424 ----- How tracking works
1425
1426 * When the constraint solver finishes solving all the wanteds in
1427 an implication, it sets its status to IC_Solved
1428
1429 - The ics_dead field, of IC_Solved, records the subset of this implication's
1430 ic_given that are redundant (not needed).
1431
1432 - The ics_need field of IC_Solved then records all the
1433 in-scope (given) evidence variables bound by the context, that
1434 were needed to solve this implication, including all its nested
1435 implications. (We remove the ic_given of this implication from
1436 the set, of course.)
1437
1438 * We compute which evidence variables are needed by an implication
1439 in setImplicationStatus. A variable is needed if
1440 a) it is free in the RHS of a Wanted EvBind,
1441 b) it is free in the RHS of an EvBind whose LHS is needed,
1442 c) it is in the ics_need of a nested implication.
1443 d) it is listed in the tcs_used_tcvs field of the nested TcSEnv
1444
1445 * We need to be careful not to discard an implication
1446 prematurely, even one that is fully solved, because we might
1447 thereby forget which variables it needs, and hence wrongly
1448 report a constraint as redundant. But we can discard it once
1449 its free vars have been incorporated into its parent; or if it
1450 simply has no free vars. This careful discarding is also
1451 handled in setImplicationStatus.
1452
1453 ----- Reporting redundant constraints
1454
1455 * TcErrors does the actual warning, in warnRedundantConstraints.
1456
1457 * We don't report redundant givens for *every* implication; only
1458 for those which reply True to TcSimplify.warnRedundantGivens:
1459
1460 - For example, in a class declaration, the default method *can*
1461 use the class constraint, but it certainly doesn't *have* to,
1462 and we don't want to report an error there.
1463
1464 - More subtly, in a function definition
1465 f :: (Ord a, Ord a, Ix a) => a -> a
1466 f x = rhs
1467 we do an ambiguity check on the type (which would find that one
1468 of the Ord a constraints was redundant), and then we check that
1469 the definition has that type (which might find that both are
1470 redundant). We don't want to report the same error twice, so we
1471 disable it for the ambiguity check. Hence using two different
1472 FunSigCtxts, one with the warn-redundant field set True, and the
1473 other set False in
1474 - TcBinds.tcSpecPrag
1475 - TcBinds.tcTySig
1476
1477 This decision is taken in setImplicationStatus, rather than TcErrors
1478 so that we can discard implication constraints that we don't need.
1479 So ics_dead consists only of the *reportable* redundant givens.
1480
1481 ----- Shortcomings
1482
1483 Consider (see Trac #9939)
1484 f2 :: (Eq a, Ord a) => a -> a -> Bool
1485 -- Ord a redundant, but Eq a is reported
1486 f2 x y = (x == y)
1487
1488 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1489 really not easy to detect that!
1490
1491
1492 Note [Cutting off simpl_loop]
1493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1494 It is very important not to iterate in simpl_loop unless there is a chance
1495 of progress. Trac #8474 is a classic example:
1496
1497 * There's a deeply-nested chain of implication constraints.
1498 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1499
1500 * From the innermost one we get a [D] alpha ~ Int,
1501 but alpha is untouchable until we get out to the outermost one
1502
1503 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1504 is untouchable, the solveInteract in simpl_loop makes no progress
1505
1506 * So there is no point in attempting to re-solve
1507 ?yn:betan => [W] ?x:Int
1508 via solveNestedImplications, because we'll just get the
1509 same [D] again
1510
1511 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1512 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1513 exponentially many) iterations!
1514
1515 Conclusion: we should call solveNestedImplications only if we did
1516 some unifiction in solveSimpleWanteds; because that's the only way
1517 we'll get more Givens (a unificaiton is like adding a Given) to
1518 allow the implication to make progress.
1519 -}
1520
1521 promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
1522 -- When we float a constraint out of an implication we must restore
1523 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1524 -- See Note [Promoting unification variables]
1525 promoteTyVar tclvl tv
1526 | isFloatedTouchableMetaTyVar tclvl tv
1527 = do { cloned_tv <- TcM.cloneMetaTyVar tv
1528 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1529 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
1530 | otherwise
1531 = return ()
1532
1533 promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
1534 -- When we float a constraint out of an implication we must restore
1535 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1536 -- See Note [Promoting unification variables]
1537 -- We don't just call promoteTyVar because we want to use unifyTyVar,
1538 -- not writeMetaTyVar
1539 promoteTyVarTcS tclvl tv
1540 | isFloatedTouchableMetaTyVar tclvl tv
1541 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1542 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1543 ; unifyTyVar tv (mkTyVarTy rhs_tv) }
1544 | otherwise
1545 = return ()
1546
1547 -- | If the tyvar is a RuntimeRep var, set it to PtrRepLifted. Returns whether or
1548 -- not this happened.
1549 defaultTyVar :: TcTyVar -> TcM ()
1550 -- Precondition: MetaTyVars only
1551 -- See Note [DefaultTyVar]
1552 defaultTyVar the_tv
1553 | isRuntimeRepVar the_tv
1554 = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
1555 ; writeMetaTyVar the_tv ptrRepLiftedTy }
1556
1557 | otherwise = return () -- The common case
1558
1559 -- | Like 'defaultTyVar', but in the TcS monad.
1560 defaultTyVarTcS :: TcTyVar -> TcS Bool
1561 defaultTyVarTcS the_tv
1562 | isRuntimeRepVar the_tv
1563 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
1564 ; unifyTyVar the_tv ptrRepLiftedTy
1565 ; return True }
1566 | otherwise
1567 = return False -- the common case
1568
1569 approximateWC :: WantedConstraints -> Cts
1570 -- Postcondition: Wanted or Derived Cts
1571 -- See Note [ApproximateWC]
1572 approximateWC wc
1573 = float_wc emptyVarSet wc
1574 where
1575 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
1576 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1577 = filterBag is_floatable simples `unionBags`
1578 do_bag (float_implic new_trapping_tvs) implics
1579 where
1580 is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` new_trapping_tvs
1581 new_trapping_tvs = transCloVarSet grow trapping_tvs
1582
1583 grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
1584 grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
1585 grow_one so_far ct tvs
1586 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
1587 | otherwise = tvs
1588 where
1589 ct_tvs = tyCoVarsOfCt ct
1590
1591 float_implic :: TcTyCoVarSet -> Implication -> Cts
1592 float_implic trapping_tvs imp
1593 | ic_no_eqs imp -- No equalities, so float
1594 = float_wc new_trapping_tvs (ic_wanted imp)
1595 | otherwise -- Don't float out of equalities
1596 = emptyCts -- See Note [ApproximateWC]
1597 where
1598 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1599 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1600 do_bag f = foldrBag (unionBags.f) emptyBag
1601
1602 {-
1603 Note [ApproximateWC]
1604 ~~~~~~~~~~~~~~~~~~~~
1605 approximateWC takes a constraint, typically arising from the RHS of a
1606 let-binding whose type we are *inferring*, and extracts from it some
1607 *simple* constraints that we might plausibly abstract over. Of course
1608 the top-level simple constraints are plausible, but we also float constraints
1609 out from inside, if they are not captured by skolems.
1610
1611 The same function is used when doing type-class defaulting (see the call
1612 to applyDefaultingRules) to extract constraints that that might be defaulted.
1613
1614 There are two caveats:
1615
1616 1. We do *not* float anything out if the implication binds equality
1617 constraints, because that defeats the OutsideIn story. Consider
1618 data T a where
1619 TInt :: T Int
1620 MkT :: T a
1621
1622 f TInt = 3::Int
1623
1624 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1625 f :: T a -> res
1626 We don't want to float (res~Int) out because then we'll infer
1627 f :: T a -> Int
1628 which is only on of the possible types. (GHC 7.6 accidentally *did*
1629 float out of such implications, which meant it would happily infer
1630 non-principal types.)
1631
1632 2. We do not float out an inner constraint that shares a type variable
1633 (transitively) with one that is trapped by a skolem. Eg
1634 forall a. F a ~ beta, Integral beta
1635 We don't want to float out (Integral beta). Doing so would be bad
1636 when defaulting, because then we'll default beta:=Integer, and that
1637 makes the error message much worse; we'd get
1638 Can't solve F a ~ Integer
1639 rather than
1640 Can't solve Integral (F a)
1641
1642 Moreover, floating out these "contaminated" constraints doesn't help
1643 when generalising either. If we generalise over (Integral b), we still
1644 can't solve the retained implication (forall a. F a ~ b). Indeed,
1645 arguably that too would be a harder error to understand.
1646
1647 Note [DefaultTyVar]
1648 ~~~~~~~~~~~~~~~~~~~
1649 defaultTyVar is used on any un-instantiated meta type variables to
1650 default any RuntimeRep variables to PtrRepLifted. This is important
1651 to ensure that instance declarations match. For example consider
1652
1653 instance Show (a->b)
1654 foo x = show (\_ -> True)
1655
1656 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
1657 and that won't match the typeKind (*) in the instance decl. See tests
1658 tc217 and tc175.
1659
1660 We look only at touchable type variables. No further constraints
1661 are going to affect these type variables, so it's time to do it by
1662 hand. However we aren't ready to default them fully to () or
1663 whatever, because the type-class defaulting rules have yet to run.
1664
1665 An alternate implementation would be to emit a derived constraint setting
1666 the RuntimeRep variable to PtrRepLifted, but this seems unnecessarily indirect.
1667
1668 Note [Promote _and_ default when inferring]
1669 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1670 When we are inferring a type, we simplify the constraint, and then use
1671 approximateWC to produce a list of candidate constraints. Then we MUST
1672
1673 a) Promote any meta-tyvars that have been floated out by
1674 approximateWC, to restore invariant (MetaTvInv) described in
1675 Note [TcLevel and untouchable type variables] in TcType.
1676
1677 b) Default the kind of any meta-tyyvars that are not mentioned in
1678 in the environment.
1679
1680 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1681 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1682 should! If we don't solve the constraint, we'll stupidly quantify over
1683 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1684 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1685 Trac #7641 is a simpler example.
1686
1687 Note [Promoting unification variables]
1688 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1689 When we float an equality out of an implication we must "promote" free
1690 unification variables of the equality, in order to maintain Invariant
1691 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1692 leftover implication.
1693
1694 This is absolutely necessary. Consider the following example. We start
1695 with two implications and a class with a functional dependency.
1696
1697 class C x y | x -> y
1698 instance C [a] [a]
1699
1700 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1701 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1702
1703 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1704 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1705 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1706 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1707 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1708
1709 class C x y | x -> y where
1710 op :: x -> y -> ()
1711
1712 instance C [a] [a]
1713
1714 type family F a :: *
1715
1716 h :: F Int -> ()
1717 h = undefined
1718
1719 data TEx where
1720 TEx :: a -> TEx
1721
1722 f (x::beta) =
1723 let g1 :: forall b. b -> ()
1724 g1 _ = h [x]
1725 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1726 in (g1 '3', g2 undefined)
1727
1728
1729 Note [Solving Family Equations]
1730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1731 After we are done with simplification we may be left with constraints of the form:
1732 [Wanted] F xis ~ beta
1733 If 'beta' is a touchable unification variable not already bound in the TyBinds
1734 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1735
1736 When is it ok to do so?
1737 1) 'beta' must not already be defaulted to something. Example:
1738
1739 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1740 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1741 have to report this as unsolved.
1742
1743 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1744 set [beta := F xis] only if beta is not among the free variables of xis.
1745
1746 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1747 of type family equations. See Inert Set invariants in TcInteract.
1748
1749 This solving is now happening during zonking, see Note [Unflattening while zonking]
1750 in TcMType.
1751
1752
1753 *********************************************************************************
1754 * *
1755 * Floating equalities *
1756 * *
1757 *********************************************************************************
1758
1759 Note [Float Equalities out of Implications]
1760 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1761 For ordinary pattern matches (including existentials) we float
1762 equalities out of implications, for instance:
1763 data T where
1764 MkT :: Eq a => a -> T
1765 f x y = case x of MkT _ -> (y::Int)
1766 We get the implication constraint (x::T) (y::alpha):
1767 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1768 We want to float out the equality into a scope where alpha is no
1769 longer untouchable, to solve the implication!
1770
1771 But we cannot float equalities out of implications whose givens may
1772 yield or contain equalities:
1773
1774 data T a where
1775 T1 :: T Int
1776 T2 :: T Bool
1777 T3 :: T a
1778
1779 h :: T a -> a -> Int
1780
1781 f x y = case x of
1782 T1 -> y::Int
1783 T2 -> y::Bool
1784 T3 -> h x y
1785
1786 We generate constraint, for (x::T alpha) and (y :: beta):
1787 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1788 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1789 (alpha ~ beta) -- From 3rd branch
1790
1791 If we float the equality (beta ~ Int) outside of the first implication and
1792 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1793 But if we just leave them inside the implications, we unify alpha := beta and
1794 solve everything.
1795
1796 Principle:
1797 We do not want to float equalities out which may
1798 need the given *evidence* to become soluble.
1799
1800 Consequence: classes with functional dependencies don't matter (since there is
1801 no evidence for a fundep equality), but equality superclasses do matter (since
1802 they carry evidence).
1803 -}
1804
1805 floatEqualities :: [TcTyVar] -> Bool
1806 -> WantedConstraints
1807 -> TcS (Cts, WantedConstraints)
1808 -- Main idea: see Note [Float Equalities out of Implications]
1809 --
1810 -- Precondition: the wc_simple of the incoming WantedConstraints are
1811 -- fully zonked, so that we can see their free variables
1812 --
1813 -- Postcondition: The returned floated constraints (Cts) are only
1814 -- Wanted or Derived
1815 --
1816 -- Also performs some unifications (via promoteTyVar), adding to
1817 -- monadically-carried ty_binds. These will be used when processing
1818 -- floated_eqs later
1819 --
1820 -- Subtleties: Note [Float equalities from under a skolem binding]
1821 -- Note [Skolem escape]
1822 floatEqualities skols no_given_eqs
1823 wanteds@(WC { wc_simple = simples })
1824 | not no_given_eqs -- There are some given equalities, so don't float
1825 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1826 | otherwise
1827 = do { outer_tclvl <- TcS.getTcLevel
1828 ; mapM_ (promoteTyVarTcS outer_tclvl)
1829 (tyCoVarsOfCtsList float_eqs)
1830 -- See Note [Promoting unification variables]
1831
1832 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1833 , text "Simples =" <+> ppr simples
1834 , text "Floated eqs =" <+> ppr float_eqs])
1835 ; return ( float_eqs
1836 , wanteds { wc_simple = remaining_simples } ) }
1837 where
1838 skol_set = mkVarSet skols
1839 (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
1840
1841 usefulToFloat :: VarSet -> Ct -> Bool
1842 usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
1843 = is_meta_var_eq pred &&
1844 (tyCoVarsOfType pred `disjointVarSet` skol_set)
1845 where
1846 pred = ctPred ct
1847
1848 -- Float out alpha ~ ty, or ty ~ alpha
1849 -- which might be unified outside
1850 -- See Note [Which equalities to float]
1851 is_meta_var_eq pred
1852 | EqPred NomEq ty1 ty2 <- classifyPredType pred
1853 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
1854 (Just tv1, _) -> float_tv_eq tv1 ty2
1855 (_, Just tv2) -> float_tv_eq tv2 ty1
1856 _ -> False
1857 | otherwise
1858 = False
1859
1860 float_tv_eq tv1 ty2 -- See Note [Which equalities to float]
1861 = isMetaTyVar tv1
1862 && (not (isSigTyVar tv1) || isTyVarTy ty2)
1863
1864 {- Note [Float equalities from under a skolem binding]
1865 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1866 Which of the simple equalities can we float out? Obviously, only
1867 ones that don't mention the skolem-bound variables. But that is
1868 over-eager. Consider
1869 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1870 The second constraint doesn't mention 'a'. But if we float it,
1871 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1872 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1873 we left with the constraint
1874 [2] forall a. a ~ gamma'[1]
1875 which is insoluble because gamma became untouchable.
1876
1877 Solution: float only constraints that stand a jolly good chance of
1878 being soluble simply by being floated, namely ones of form
1879 a ~ ty
1880 where 'a' is a currently-untouchable unification variable, but may
1881 become touchable by being floated (perhaps by more than one level).
1882
1883 We had a very complicated rule previously, but this is nice and
1884 simple. (To see the notes, look at this Note in a version of
1885 TcSimplify prior to Oct 2014).
1886
1887 Note [Which equalities to float]
1888 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1889 Which equalities should we float? We want to float ones where there
1890 is a decent chance that floating outwards will allow unification to
1891 happen. In particular:
1892
1893 Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
1894
1895 * alpha is a meta-tyvar.
1896
1897 * And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that
1898 case, floating out won't help either, and it may affect grouping
1899 of error messages.
1900
1901 Note [Skolem escape]
1902 ~~~~~~~~~~~~~~~~~~~~
1903 You might worry about skolem escape with all this floating.
1904 For example, consider
1905 [2] forall a. (a ~ F beta[2] delta,
1906 Maybe beta[2] ~ gamma[1])
1907
1908 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1909 solve with gamma := beta. But what if later delta:=Int, and
1910 F b Int = b.
1911 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1912 skolem has escaped!
1913
1914 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1915 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1916
1917
1918 *********************************************************************************
1919 * *
1920 * Defaulting and disamgiguation *
1921 * *
1922 *********************************************************************************
1923 -}
1924
1925 applyDefaultingRules :: WantedConstraints -> TcS Bool
1926 -- True <=> I did some defaulting, by unifying a meta-tyvar
1927 -- Imput WantedConstraints are not necessarily zonked
1928
1929 applyDefaultingRules wanteds
1930 | isEmptyWC wanteds
1931 = return False
1932 | otherwise
1933 = do { info@(default_tys, _) <- getDefaultInfo
1934 ; wanteds <- TcS.zonkWC wanteds
1935
1936 ; let groups = findDefaultableGroups info wanteds
1937
1938 ; traceTcS "applyDefaultingRules {" $
1939 vcat [ text "wanteds =" <+> ppr wanteds
1940 , text "groups =" <+> ppr groups
1941 , text "info =" <+> ppr info ]
1942
1943 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1944
1945 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1946
1947 ; return (or something_happeneds) }
1948
1949 findDefaultableGroups
1950 :: ( [Type]
1951 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1952 -> WantedConstraints -- Unsolved (wanted or derived)
1953 -> [(TyVar, [Ct])]
1954 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1955 | null default_tys
1956 = []
1957 | otherwise
1958 = [ (tv, map fstOf3 group)
1959 | group@((_,_,tv):_) <- unary_groups
1960 , defaultable_tyvar tv
1961 , defaultable_classes (map sndOf3 group) ]
1962 where
1963 simples = approximateWC wanteds
1964 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
1965 unary_groups = equivClasses cmp_tv unaries
1966
1967 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
1968 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
1969 non_unaries :: [Ct] -- and *other* constraints
1970
1971 -- Finds unary type-class constraints
1972 -- But take account of polykinded classes like Typeable,
1973 -- which may look like (Typeable * (a:*)) (Trac #8931)
1974 find_unary cc
1975 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
1976 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
1977 -- Ignore invisible arguments for this purpose
1978 , Just tv <- tcGetTyVar_maybe ty
1979 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
1980 -- we definitely don't want to try to assign to those!
1981 = Left (cc, cls, tv)
1982 find_unary cc = Right cc -- Non unary or non dictionary
1983
1984 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
1985 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
1986
1987 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1988
1989 defaultable_tyvar tv
1990 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1991 b2 = not (tv `elemVarSet` bad_tvs)
1992 in b1 && b2
1993
1994 defaultable_classes clss
1995 | extended_defaults = any isInteractiveClass clss
1996 | otherwise = all is_std_class clss && (any is_num_class clss)
1997
1998 -- In interactive mode, or with -XExtendedDefaultRules,
1999 -- we default Show a to Show () to avoid graututious errors on "show []"
2000 isInteractiveClass cls
2001 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey
2002 , ordClassKey, foldableClassKey
2003 , traversableClassKey])
2004
2005 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2006 -- is_num_class adds IsString to the standard numeric classes,
2007 -- when -foverloaded-strings is enabled
2008
2009 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2010 -- Similarly is_std_class
2011
2012 ------------------------------
2013 disambigGroup :: [Type] -- The default types
2014 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
2015 -- sharing same type variable
2016 -> TcS Bool -- True <=> something happened, reflected in ty_binds
2017
2018 disambigGroup [] _
2019 = return False
2020 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
2021 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
2022 ; fake_ev_binds_var <- TcS.newTcEvBinds
2023 ; tclvl <- TcS.getTcLevel
2024 ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet
2025 (pushTcLevel tclvl) try_group
2026
2027 ; if success then
2028 -- Success: record the type variable binding, and return
2029 do { unifyTyVar the_tv default_ty
2030 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
2031 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
2032 ; return True }
2033 else
2034 -- Failure: try with the next type
2035 do { traceTcS "disambigGroup failed, will try other default types }"
2036 (ppr default_ty)
2037 ; disambigGroup default_tys group } }
2038 where
2039 try_group
2040 | Just subst <- mb_subst
2041 = do { lcl_env <- TcS.getLclEnv
2042 ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
2043 , ctl_env = lcl_env
2044 , ctl_t_or_k = Nothing
2045 , ctl_depth = initialSubGoalDepth }
2046 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
2047 wanteds
2048 ; fmap isEmptyWC $
2049 solveSimpleWanteds $ listToBag $
2050 map mkNonCanonical wanted_evs }
2051
2052 | otherwise
2053 = return False
2054
2055 the_ty = mkTyVarTy the_tv
2056 mb_subst = tcMatchTy the_ty default_ty
2057 -- Make sure the kinds match too; hence this call to tcMatchTy
2058 -- E.g. suppose the only constraint was (Typeable k (a::k))
2059 -- With the addition of polykinded defaulting we also want to reject
2060 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2061
2062
2063 {-
2064 Note [Avoiding spurious errors]
2065 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2066 When doing the unification for defaulting, we check for skolem
2067 type variables, and simply don't default them. For example:
2068 f = (*) -- Monomorphic
2069 g :: Num a => a -> a
2070 g x = f x x
2071 Here, we get a complaint when checking the type signature for g,
2072 that g isn't polymorphic enough; but then we get another one when
2073 dealing with the (Num a) context arising from f's definition;
2074 we try to unify a with Int (to default it), but find that it's
2075 already been unified with the rigid variable from g's type sig.
2076 -}