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