Fix #11974 by adding a more smarts to TcDefaults.
[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 )
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 "simplifyDefault" 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 ; let given_cts = mkGivens 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 -> [TcIdSigInst] -- 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_inst_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 = mkGivens 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 -- extra_qtvs: see Note [Quantification and partial signatures]
658 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
659 ; psig_theta_vars <- mapM zonkId psig_theta_vars
660 ; all_qtvs <- add_psig_tvs qtvs
661 [ tv | sig <- partial_sigs
662 , (_,tv) <- sig_inst_skols sig ]
663
664 ; let full_theta = psig_theta ++ bound_theta
665 full_theta_vars = psig_theta_vars ++ bound_theta_vars
666 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
667 | (name, ty) <- name_taus ]
668 -- Don't add the quantified variables here, because
669 -- they are also bound in ic_skols and we want them
670 -- to be tidied uniformly
671
672 implic = Implic { ic_tclvl = rhs_tclvl
673 , ic_skols = all_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 where
695 add_psig_tvs qtvs [] = return qtvs
696 add_psig_tvs qtvs (tv:tvs)
697 = do { tv <- zonkTcTyVarToTyVar tv
698 ; if tv `elem` qtvs
699 then add_psig_tvs qtvs tvs
700 else do { mb_tv <- zonkQuantifiedTyVar False tv
701 ; case mb_tv of
702 Nothing -> add_psig_tvs qtvs tvs
703 Just tv -> add_psig_tvs (tv:qtvs) tvs } }
704
705 {- Note [Add signature contexts as givens]
706 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
707 Consider this (Trac #11016):
708 f2 :: (?x :: Int) => _
709 f2 = ?x
710 or this
711 f3 :: a ~ Bool => (a, _)
712 f3 = (True, False)
713 or theis
714 f4 :: (Ord a, _) => a -> Bool
715 f4 x = x==x
716
717 We'll use plan InferGen because there are holes in the type. But:
718 * For f2 we want to have the (?x :: Int) constraint floating around
719 so that the functional dependencies kick in. Otherwise the
720 occurrence of ?x on the RHS produces constraint (?x :: alpha), and
721 we won't unify alpha:=Int.
722 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
723 in the RHS
724 * For f4 we want to use the (Ord a) in the signature to solve the Eq a
725 constraint.
726
727 Solution: in simplifyInfer, just before simplifying the constraints
728 gathered from the RHS, add Given constraints for the context of any
729 type signatures.
730
731 ************************************************************************
732 * *
733 Quantification
734 * *
735 ************************************************************************
736
737 Note [Deciding quantification]
738 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
739 If the monomorphism restriction does not apply, then we quantify as follows:
740
741 * Take the global tyvars, and "grow" them using the equality constraints
742 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
743 happen because alpha is untouchable here) then do not quantify over
744 beta, because alpha fixes beta, and beta is effectively free in
745 the environment too
746 These are the mono_tvs
747
748 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
749 using all the constraints. These are tau_tvs_plus
750
751 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
752 careful to close over kinds, and to skolemise the quantified tyvars.
753 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
754 Result is qtvs.
755
756 * Filter the constraints using pickQuantifiablePreds and the qtvs.
757 We have to zonk the constraints first, so they "see" the freshly
758 created skolems.
759
760 If the MR does apply, mono_tvs includes all the constrained tyvars --
761 including all covars -- and the quantified constraints are empty/insoluble.
762
763 -}
764
765 decideQuantification
766 :: Bool -- try the MR restriction?
767 -> [(Name, TcTauType)] -- Variables to be generalised
768 -> [PredType] -- All annotated constraints from signatures
769 -> [PredType] -- Candidate theta
770 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
771 , [PredType] ) -- and this context (fully zonked)
772 -- See Note [Deciding quantification]
773 decideQuantification apply_mr name_taus psig_theta candidates
774 = do { gbl_tvs <- tcGetGlobalTyCoVars
775 ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
776 -- psig_theta: see Note [Quantification and partial signatures]
777 ; let DV { dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
778 (gbl_cand, quant_cand) -- gbl_cand = do not quantify me
779 = case apply_mr of -- quant_cand = try to quantify me
780 True -> (candidates, [])
781 False -> ([], candidates)
782 zonked_tkvs = dVarSetToVarSet zkvs `unionVarSet` dVarSetToVarSet ztvs
783 eq_constraints = filter isEqPred quant_cand
784 constrained_tvs = tyCoVarsOfTypes gbl_cand
785 mono_tvs = growThetaTyVars eq_constraints $
786 gbl_tvs `unionVarSet` constrained_tvs
787 tau_tvs_plus = growThetaTyVarsDSet quant_cand ztvs
788 dvs_plus = DV { dv_kvs = zkvs, dv_tvs = tau_tvs_plus }
789
790 ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
791 -- We don't grow the kvs, as there's no real need to. Recall
792 -- that quantifyTyVars uses the separation between kvs and tvs
793 -- only for defaulting, and we don't want (ever) to default a tv
794 -- to *. So, don't grow the kvs.
795
796 ; quant_cand <- TcM.zonkTcTypes quant_cand
797 -- quantifyTyVars turned some meta tyvars into
798 -- quantified skolems, so we have to zonk again
799
800 ; let qtv_set = mkVarSet qtvs
801 theta = pickQuantifiablePreds qtv_set quant_cand
802 min_theta = mkMinimalBySCs theta
803 -- See Note [Minimize by Superclasses]
804
805 -- Warn about the monomorphism restriction
806 ; warn_mono <- woptM Opt_WarnMonomorphism
807 ; let mr_bites = constrained_tvs `intersectsVarSet` zonked_tkvs
808 ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
809 hang (text "The Monomorphism Restriction applies to the binding"
810 <> plural bndrs <+> text "for" <+> pp_bndrs)
811 2 (text "Consider giving a type signature for"
812 <+> if isSingleton bndrs then pp_bndrs
813 else text "these binders")
814
815 ; traceTc "decideQuantification 2"
816 (vcat [ text "gbl_cand:" <+> ppr gbl_cand
817 , text "quant_cand:" <+> ppr quant_cand
818 , text "gbl_tvs:" <+> ppr gbl_tvs
819 , text "mono_tvs:" <+> ppr mono_tvs
820 , text "tau_tvs_plus:" <+> ppr tau_tvs_plus
821 , text "qtvs:" <+> ppr qtvs
822 , text "min_theta:" <+> ppr min_theta ])
823 ; return (qtvs, min_theta) }
824 where
825 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
826 (bndrs, taus) = unzip name_taus
827
828 ------------------
829 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
830 -- See Note [Growing the tau-tvs using constraints]
831 -- NB: only returns tyvars, never covars
832 growThetaTyVars theta tvs
833 | null theta = tvs_only
834 | otherwise = filterVarSet isTyVar $
835 transCloVarSet mk_next seed_tvs
836 where
837 tvs_only = filterVarSet isTyVar tvs
838 seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
839 (ips, non_ips) = partition isIPPred theta
840 -- See Note [Inheriting implicit parameters] in TcType
841
842 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
843 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
844 grow_one so_far pred tvs
845 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
846 | otherwise = tvs
847 where
848 pred_tvs = tyCoVarsOfType pred
849
850 ------------------
851 growThetaTyVarsDSet :: ThetaType -> DTyCoVarSet -> DTyVarSet
852 -- See Note [Growing the tau-tvs using constraints]
853 -- NB: only returns tyvars, never covars
854 -- It takes a deterministic set of TyCoVars and returns a deterministic set
855 -- of TyVars.
856 -- The implementation mirrors growThetaTyVars, the only difference is that
857 -- it avoids unionDVarSet and uses more efficient extendDVarSetList.
858 growThetaTyVarsDSet theta tvs
859 | null theta = tvs_only
860 | otherwise = filterDVarSet isTyVar $
861 transCloDVarSet mk_next seed_tvs
862 where
863 tvs_only = filterDVarSet isTyVar tvs
864 seed_tvs = tvs `extendDVarSetList` tyCoVarsOfTypesList ips
865 (ips, non_ips) = partition isIPPred theta
866 -- See Note [Inheriting implicit parameters] in TcType
867
868 mk_next :: DVarSet -> DVarSet -- Maps current set to newly-grown ones
869 mk_next so_far = foldr (grow_one so_far) emptyDVarSet non_ips
870 grow_one so_far pred tvs
871 | any (`elemDVarSet` so_far) pred_tvs = tvs `extendDVarSetList` pred_tvs
872 | otherwise = tvs
873 where
874 pred_tvs = tyCoVarsOfTypeList pred
875
876 {- Note [Quantification and partial signatures]
877 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
878 When choosing type variables to quantify, the basic plan is to
879 quantify over all type variables that are
880 * free in the tau_tvs, and
881 * not forced to be monomorphic (mono_tvs),
882 for example by being free in the environment.
883
884 However, in the case of a partial type signature, be doing inference
885 *in the presence of a type signature*. For example:
886 f :: _ -> a
887 f x = ...
888 or
889 g :: (Eq _a) => _b -> _b
890 In both cases we use plan InferGen, and hence call simplifyInfer.
891 But those 'a' variables are skolems, and we should be sure to quantify
892 over them, for two reasons
893
894 * In the case of a type error
895 f :: _ -> Maybe a
896 f x = True && x
897 The inferred type of 'f' is f :: Bool -> Bool, but there's a
898 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
899 machine expects to find a binding site for the skolem 'a', so we
900 add it to the ic_skols of the residual implication.
901
902 Note that we /only/ do this to the residual implication. We don't
903 complicate the quantified type varialbes of 'f' for downstream code;
904 it's just a device to make the error message generator know what to
905 report.
906
907 * Consider the partial type signature
908 f :: (Eq _) => Int -> Int
909 f x = x
910 In normal cases that makes sense; e.g.
911 g :: Eq _a => _a -> _a
912 g x = x
913 where the signature makes the type less general than it could
914 be. But for 'f' we must therefore quantify over the user-annotated
915 constraints, to get
916 f :: forall a. Eq a => Int -> Int
917 (thereby correctly triggering an ambiguity error later). If we don't
918 we'll end up with a strange open type
919 f :: Eq alpha => Int -> Int
920 which isn't ambiguous but is still very wrong. That's why include
921 psig_theta in the variables to quantify over, passed to
922 decideQuantification.
923
924 Note [Quantifying over equality constraints]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
927 Doing so may simply postpone a type error from the function definition site to
928 its call site. (At worst, imagine (Int ~ Bool)).
929
930 However, consider this
931 forall a. (F [a] ~ Int) => blah
932 Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
933 site we will know 'a', and perhaps we have instance F [Bool] = Int.
934 So we *do* quantify over a type-family equality where the arguments mention
935 the quantified variables.
936
937 Note [Growing the tau-tvs using constraints]
938 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
939 (growThetaTyVars insts tvs) is the result of extending the set
940 of tyvars, tvs, using all conceivable links from pred
941
942 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
943 Then growThetaTyVars preds tvs = {a,b,c}
944
945 Notice that
946 growThetaTyVars is conservative if v might be fixed by vs
947 => v `elem` grow(vs,C)
948
949 Note [Quantification with errors]
950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
951 If we find that the RHS of the definition has some absolutely-insoluble
952 constraints, we abandon all attempts to find a context to quantify
953 over, and instead make the function fully-polymorphic in whatever
954 type we have found. For two reasons
955 a) Minimise downstream errors
956 b) Avoid spurious errors from this function
957
958 But NB that we must include *derived* errors in the check. Example:
959 (a::*) ~ Int#
960 We get an insoluble derived error *~#, and we don't want to discard
961 it before doing the isInsolubleWC test! (Trac #8262)
962
963 Note [Default while Inferring]
964 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
965 Our current plan is that defaulting only happens at simplifyTop and
966 not simplifyInfer. This may lead to some insoluble deferred constraints.
967 Example:
968
969 instance D g => C g Int b
970
971 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
972 type inferred = gamma -> gamma
973
974 Now, if we try to default (alpha := Int) we will be able to refine the implication to
975 (forall b. 0 => C gamma Int b)
976 which can then be simplified further to
977 (forall b. 0 => D gamma)
978 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
979 type: forall g. D g => g -> g
980
981 Instead what will currently happen is that we will get a quantified type
982 (forall g. g -> g) and an implication:
983 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
984
985 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
986 unsolvable implication:
987 forall g. 0 => (forall b. 0 => D g)
988
989 The concrete example would be:
990 h :: C g a s => g -> a -> ST s a
991 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
992
993 But it is quite tedious to do defaulting and resolve the implication constraints, and
994 we have not observed code breaking because of the lack of defaulting in inference, so
995 we don't do it for now.
996
997
998
999 Note [Minimize by Superclasses]
1000 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1001 When we quantify over a constraint, in simplifyInfer we need to
1002 quantify over a constraint that is minimal in some sense: For
1003 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
1004 we'd like to quantify over Ord alpha, because we can just get Eq alpha
1005 from superclass selection from Ord alpha. This minimization is what
1006 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
1007 to check the original wanted.
1008
1009
1010 Note [Avoid unnecessary constraint simplification]
1011 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1012 -------- NB NB NB (Jun 12) -------------
1013 This note not longer applies; see the notes with Trac #4361.
1014 But I'm leaving it in here so we remember the issue.)
1015 ----------------------------------------
1016 When inferring the type of a let-binding, with simplifyInfer,
1017 try to avoid unnecessarily simplifying class constraints.
1018 Doing so aids sharing, but it also helps with delicate
1019 situations like
1020
1021 instance C t => C [t] where ..
1022
1023 f :: C [t] => ....
1024 f x = let g y = ...(constraint C [t])...
1025 in ...
1026 When inferring a type for 'g', we don't want to apply the
1027 instance decl, because then we can't satisfy (C t). So we
1028 just notice that g isn't quantified over 't' and partition
1029 the constraints before simplifying.
1030
1031 This only half-works, but then let-generalisation only half-works.
1032
1033 *********************************************************************************
1034 * *
1035 * Main Simplifier *
1036 * *
1037 ***********************************************************************************
1038
1039 -}
1040
1041 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
1042 -- Solve the specified Wanted constraints
1043 -- Discard the evidence binds
1044 -- Discards all Derived stuff in result
1045 -- Postcondition: fully zonked and unflattened constraints
1046 simplifyWantedsTcM wanted
1047 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
1048 ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted)
1049 ; result <- TcM.zonkWC result
1050 ; traceTc "simplifyWantedsTcM }" (ppr result)
1051 ; return result }
1052
1053 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1054 -- Since solveWanteds returns the residual WantedConstraints,
1055 -- it should always be called within a runTcS or something similar,
1056 -- Result is not zonked
1057 solveWantedsAndDrop wanted
1058 = do { wc <- solveWanteds wanted
1059 ; return (dropDerivedWC wc) }
1060
1061 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1062 -- so that the inert set doesn't mindlessly propagate.
1063 -- NB: wc_simples may be wanted /or/ derived now
1064 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1065 = do { traceTcS "solveWanteds {" (ppr wc)
1066
1067 -- Try the simple bit, including insolubles. Solving insolubles a
1068 -- second time round is a bit of a waste; but the code is simple
1069 -- and the program is wrong anyway, and we don't run the danger
1070 -- of adding Derived insolubles twice; see
1071 -- TcSMonad Note [Do not add duplicate derived insolubles]
1072 ; wc1 <- solveSimpleWanteds simples
1073 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1074 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1075
1076 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
1077
1078 ; dflags <- getDynFlags
1079 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
1080 (WC { wc_simple = simples1, wc_impl = implics2
1081 , wc_insol = insols `unionBags` insols1 })
1082
1083 ; bb <- TcS.getTcEvBindsMap
1084 ; traceTcS "solveWanteds }" $
1085 vcat [ text "final wc =" <+> ppr final_wc
1086 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1087
1088 ; return final_wc }
1089
1090 simpl_loop :: Int -> IntWithInf -> Cts -> Bool
1091 -> WantedConstraints
1092 -> TcS WantedConstraints
1093 simpl_loop n limit floated_eqs no_new_scs
1094 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1095 | isEmptyBag floated_eqs && no_new_scs
1096 = return wc -- Done!
1097
1098 | n `intGtLimit` limit
1099 = do { -- Add an error (not a warning) if we blow the limit,
1100 -- Typically if we blow the limit we are going to report some other error
1101 -- (an unsolved constraint), and we don't want that error to suppress
1102 -- the iteration limit warning!
1103 addErrTcS (hang (text "solveWanteds: too many iterations"
1104 <+> parens (text "limit =" <+> ppr limit))
1105 2 (vcat [ text "Unsolved:" <+> ppr wc
1106 , ppUnless (isEmptyBag floated_eqs) $
1107 text "Floated equalities:" <+> ppr floated_eqs
1108 , ppUnless no_new_scs $
1109 text "New superclasses found"
1110 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
1111 ]))
1112 ; return wc }
1113
1114 | otherwise
1115 = do { let n_floated = lengthBag floated_eqs
1116 ; csTraceTcS $
1117 text "simpl_loop iteration=" <> int n
1118 <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma
1119 , int n_floated <+> text "floated eqs" <> comma
1120 , int (lengthBag simples) <+> text "simples to solve" ])
1121
1122 -- solveSimples may make progress if either float_eqs hold
1123 ; (unifs1, wc1) <- reportUnifications $
1124 solveSimpleWanteds (floated_eqs `unionBags` simples)
1125 -- Put floated_eqs first so they get solved first
1126 -- NB: the floated_eqs may include /derived/ equalities
1127 -- arising from fundeps inside an implication
1128
1129 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1130 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1131
1132 -- We have already tried to solve the nested implications once
1133 -- Try again only if we have unified some meta-variables
1134 -- (which is a bit like adding more givens
1135 -- See Note [Cutting off simpl_loop]
1136 ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
1137 then return (emptyBag, implics)
1138 else solveNestedImplications (implics `unionBags` implics1)
1139
1140 ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
1141 (WC { wc_simple = simples1, wc_impl = implics2
1142 , wc_insol = insols `unionBags` insols1 }) }
1143
1144 expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
1145 -- If there are any unsolved wanteds, expand one step of superclasses for
1146 -- unsolved wanteds or givens
1147 -- See Note [The superclass story] in TcCanonical
1148 expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
1149 | not (anyBag superClassesMightHelp unsolved)
1150 = return (True, wc)
1151 | otherwise
1152 = do { traceTcS "expandSuperClasses {" empty
1153 ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
1154 get acc ct = case isPendingScDict ct of
1155 Just ct' -> (ct':acc, ct')
1156 Nothing -> (acc, ct)
1157 ; pending_given <- getPendingScDicts
1158 ; if null pending_given && null pending_wanted
1159 then do { traceTcS "End expandSuperClasses no-op }" empty
1160 ; return (True, wc) }
1161 else
1162 do { new_given <- makeSuperClasses pending_given
1163 ; new_insols <- solveSimpleGivens new_given
1164 ; new_wanted <- makeSuperClasses pending_wanted
1165 ; traceTcS "End expandSuperClasses }"
1166 (vcat [ text "Given:" <+> ppr pending_given
1167 , text "Insols from given:" <+> ppr new_insols
1168 , text "Wanted:" <+> ppr new_wanted ])
1169 ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
1170 , wc_insol = insols `unionBags` new_insols }) } }
1171
1172 solveNestedImplications :: Bag Implication
1173 -> TcS (Cts, Bag Implication)
1174 -- Precondition: the TcS inerts may contain unsolved simples which have
1175 -- to be converted to givens before we go inside a nested implication.
1176 solveNestedImplications implics
1177 | isEmptyBag implics
1178 = return (emptyBag, emptyBag)
1179 | otherwise
1180 = do { traceTcS "solveNestedImplications starting {" empty
1181 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
1182 ; let floated_eqs = concatBag floated_eqs_s
1183
1184 -- ... and we are back in the original TcS inerts
1185 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1186 -- them in the beginning of this function.
1187 ; traceTcS "solveNestedImplications end }" $
1188 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
1189 , text "unsolved_implics =" <+> ppr unsolved_implics ]
1190
1191 ; return (floated_eqs, catBagMaybes unsolved_implics) }
1192
1193 solveImplication :: Implication -- Wanted
1194 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
1195 Maybe Implication) -- Simplified implication (empty or singleton)
1196 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1197 -- which after trying to solve this implication we must restore to their original value
1198 solveImplication imp@(Implic { ic_tclvl = tclvl
1199 , ic_binds = m_ev_binds
1200 , ic_skols = skols
1201 , ic_given = given_ids
1202 , ic_wanted = wanteds
1203 , ic_info = info
1204 , ic_status = status
1205 , ic_env = env })
1206 | IC_Solved {} <- status
1207 = return (emptyCts, Just imp) -- Do nothing
1208
1209 | otherwise -- Even for IC_Insoluble it is worth doing more work
1210 -- The insoluble stuff might be in one sub-implication
1211 -- and other unsolved goals in another; and we want to
1212 -- solve the latter as much as possible
1213 = do { inerts <- getTcSInerts
1214 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1215
1216 -- Solve the nested constraints
1217 ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
1218 <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
1219 do { let loc = mkGivenLoc tclvl info env
1220 givens = mkGivens loc given_ids
1221 ; given_insols <- solveSimpleGivens givens
1222
1223 ; residual_wanted <- solveWanteds wanteds
1224 -- solveWanteds, *not* solveWantedsAndDrop, because
1225 -- we want to retain derived equalities so we can float
1226 -- them out in floatEqualities
1227
1228 ; no_eqs <- getNoGivenEqs tclvl skols
1229 -- Call getNoGivenEqs /after/ solveWanteds, because
1230 -- solveWanteds can augment the givens, via expandSuperClasses,
1231 -- to reveal given superclass equalities
1232
1233 ; return (no_eqs, given_insols, residual_wanted) }
1234
1235 ; (floated_eqs, residual_wanted)
1236 <- floatEqualities skols no_given_eqs residual_wanted
1237
1238 ; traceTcS "solveImplication 2"
1239 (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs)
1240 ; let final_wanted = residual_wanted `addInsols` given_insols
1241
1242 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
1243 , ic_wanted = final_wanted })
1244 used_tcvs
1245
1246 ; evbinds <- TcS.getTcEvBindsMap
1247 ; traceTcS "solveImplication end }" $ vcat
1248 [ text "no_given_eqs =" <+> ppr no_given_eqs
1249 , text "floated_eqs =" <+> ppr floated_eqs
1250 , text "res_implic =" <+> ppr res_implic
1251 , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
1252
1253 ; return (floated_eqs, res_implic) }
1254
1255 ----------------------
1256 setImplicationStatus :: Implication -> TyCoVarSet -- needed variables
1257 -> TcS (Maybe Implication)
1258 -- Finalise the implication returned from solveImplication:
1259 -- * Set the ic_status field
1260 -- * Trim the ic_wanted field to remove Derived constraints
1261 -- Return Nothing if we can discard the implication altogether
1262 setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
1263 , ic_info = info
1264 , ic_tclvl = tc_lvl
1265 , ic_wanted = wc
1266 , ic_given = givens })
1267 used_tcvs
1268 | some_insoluble
1269 = return $ Just $
1270 implic { ic_status = IC_Insoluble
1271 , ic_wanted = wc { wc_simple = pruned_simples
1272 , wc_insol = pruned_insols } }
1273
1274 | some_unsolved
1275 = return $ Just $
1276 implic { ic_status = IC_Unsolved
1277 , ic_wanted = wc { wc_simple = pruned_simples
1278 , wc_insol = pruned_insols } }
1279
1280 | otherwise -- Everything is solved; look at the implications
1281 -- See Note [Tracking redundant constraints]
1282 = do { ev_binds <- case m_ev_binds_var of
1283 Just (EvBindsVar ref _) -> TcS.readTcRef ref
1284 Nothing -> return emptyEvBindMap
1285 ; let all_needs = neededEvVars ev_binds
1286 (used_tcvs `unionVarSet` implic_needs)
1287
1288 dead_givens | warnRedundantGivens info
1289 = filterOut (`elemVarSet` all_needs) givens
1290 | otherwise = [] -- None to report
1291
1292 final_needs = all_needs `delVarSetList` givens
1293
1294 discard_entire_implication -- Can we discard the entire implication?
1295 = null dead_givens -- No warning from this implication
1296 && isEmptyBag pruned_implics -- No live children
1297 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
1298
1299 final_status = IC_Solved { ics_need = final_needs
1300 , ics_dead = dead_givens }
1301 final_implic = implic { ic_status = final_status
1302 , ic_wanted = wc { wc_simple = pruned_simples
1303 , wc_insol = pruned_insols
1304 , wc_impl = pruned_implics } }
1305 -- We can only prune the child implications (pruned_implics)
1306 -- in the IC_Solved status case, because only then we can
1307 -- accumulate their needed evidence variales into the
1308 -- IC_Solved final_status field of the parent implication.
1309
1310 ; return $ if discard_entire_implication
1311 then Nothing
1312 else Just final_implic }
1313 where
1314 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
1315
1316 some_insoluble = insolubleWC tc_lvl wc
1317 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
1318 || isNothing mb_implic_needs
1319
1320 pruned_simples = dropDerivedSimples simples
1321 pruned_insols = dropDerivedInsols insols
1322 pruned_implics = filterBag need_to_keep_implic implics
1323
1324 mb_implic_needs :: Maybe VarSet
1325 -- Just vs => all implics are IC_Solved, with 'vs' needed
1326 -- Nothing => at least one implic is not IC_Solved
1327 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
1328 Just implic_needs = mb_implic_needs
1329
1330 add_implic implic acc
1331 | Just vs_acc <- acc
1332 , IC_Solved { ics_need = vs } <- ic_status implic
1333 = Just (vs `unionVarSet` vs_acc)
1334 | otherwise = Nothing
1335
1336 need_to_keep_implic ic
1337 | IC_Solved { ics_dead = [] } <- ic_status ic
1338 -- Fully solved, and no redundant givens to report
1339 , isEmptyBag (wc_impl (ic_wanted ic))
1340 -- And no children that might have things to report
1341 = False
1342 | otherwise
1343 = True
1344
1345 warnRedundantGivens :: SkolemInfo -> Bool
1346 warnRedundantGivens (SigSkol ctxt _)
1347 = case ctxt of
1348 FunSigCtxt _ warn_redundant -> warn_redundant
1349 ExprSigCtxt -> True
1350 _ -> False
1351
1352 -- To think about: do we want to report redundant givens for
1353 -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
1354 warnRedundantGivens (InstSkol {}) = True
1355 warnRedundantGivens _ = False
1356
1357 neededEvVars :: EvBindMap -> VarSet -> VarSet
1358 -- Find all the evidence variables that are "needed",
1359 -- and then delete all those bound by the evidence bindings
1360 -- See note [Tracking redundant constraints]
1361 neededEvVars ev_binds initial_seeds
1362 = needed `minusVarSet` bndrs
1363 where
1364 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
1365 needed = transCloVarSet also_needs seeds
1366 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
1367
1368 add_wanted :: EvBind -> VarSet -> VarSet
1369 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1370 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1371 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1372
1373 also_needs :: VarSet -> VarSet
1374 also_needs needs
1375 = nonDetFoldUFM add emptyVarSet needs
1376 -- It's OK to use nonDetFoldUFM here because we immediately forget
1377 -- about the ordering by creating a set
1378 where
1379 add v needs
1380 | Just ev_bind <- lookupEvBind ev_binds v
1381 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
1382 , is_given
1383 = evVarsOfTerm rhs `unionVarSet` needs
1384 | otherwise
1385 = needs
1386
1387 add_bndr :: EvBind -> VarSet -> VarSet
1388 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
1389
1390
1391 {-
1392 Note [Tracking redundant constraints]
1393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1394 With Opt_WarnRedundantConstraints, GHC can report which
1395 constraints of a type signature (or instance declaration) are
1396 redundant, and can be omitted. Here is an overview of how it
1397 works:
1398
1399 ----- What is a redundant constraint?
1400
1401 * The things that can be redundant are precisely the Given
1402 constraints of an implication.
1403
1404 * A constraint can be redundant in two different ways:
1405 a) It is implied by other givens. E.g.
1406 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1407 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1408 b) It is not needed by the Wanted constraints covered by the
1409 implication E.g.
1410 f :: Eq a => a -> Bool
1411 f x = True -- Equality not used
1412
1413 * To find (a), when we have two Given constraints,
1414 we must be careful to drop the one that is a naked variable (if poss).
1415 So if we have
1416 f :: (Eq a, Ord a) => blah
1417 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1418 [G] d2 :: Eq a
1419 We want to discard d2 in favour of the superclass selection from
1420 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1421 See Note [Replacement vs keeping].
1422
1423 * To find (b) we need to know which evidence bindings are 'wanted';
1424 hence the eb_is_given field on an EvBind.
1425
1426 ----- How tracking works
1427
1428 * When the constraint solver finishes solving all the wanteds in
1429 an implication, it sets its status to IC_Solved
1430
1431 - The ics_dead field, of IC_Solved, records the subset of this implication's
1432 ic_given that are redundant (not needed).
1433
1434 - The ics_need field of IC_Solved then records all the
1435 in-scope (given) evidence variables bound by the context, that
1436 were needed to solve this implication, including all its nested
1437 implications. (We remove the ic_given of this implication from
1438 the set, of course.)
1439
1440 * We compute which evidence variables are needed by an implication
1441 in setImplicationStatus. A variable is needed if
1442 a) it is free in the RHS of a Wanted EvBind,
1443 b) it is free in the RHS of an EvBind whose LHS is needed,
1444 c) it is in the ics_need of a nested implication.
1445 d) it is listed in the tcs_used_tcvs field of the nested TcSEnv
1446
1447 * We need to be careful not to discard an implication
1448 prematurely, even one that is fully solved, because we might
1449 thereby forget which variables it needs, and hence wrongly
1450 report a constraint as redundant. But we can discard it once
1451 its free vars have been incorporated into its parent; or if it
1452 simply has no free vars. This careful discarding is also
1453 handled in setImplicationStatus.
1454
1455 ----- Reporting redundant constraints
1456
1457 * TcErrors does the actual warning, in warnRedundantConstraints.
1458
1459 * We don't report redundant givens for *every* implication; only
1460 for those which reply True to TcSimplify.warnRedundantGivens:
1461
1462 - For example, in a class declaration, the default method *can*
1463 use the class constraint, but it certainly doesn't *have* to,
1464 and we don't want to report an error there.
1465
1466 - More subtly, in a function definition
1467 f :: (Ord a, Ord a, Ix a) => a -> a
1468 f x = rhs
1469 we do an ambiguity check on the type (which would find that one
1470 of the Ord a constraints was redundant), and then we check that
1471 the definition has that type (which might find that both are
1472 redundant). We don't want to report the same error twice, so we
1473 disable it for the ambiguity check. Hence using two different
1474 FunSigCtxts, one with the warn-redundant field set True, and the
1475 other set False in
1476 - TcBinds.tcSpecPrag
1477 - TcBinds.tcTySig
1478
1479 This decision is taken in setImplicationStatus, rather than TcErrors
1480 so that we can discard implication constraints that we don't need.
1481 So ics_dead consists only of the *reportable* redundant givens.
1482
1483 ----- Shortcomings
1484
1485 Consider (see Trac #9939)
1486 f2 :: (Eq a, Ord a) => a -> a -> Bool
1487 -- Ord a redundant, but Eq a is reported
1488 f2 x y = (x == y)
1489
1490 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1491 really not easy to detect that!
1492
1493
1494 Note [Cutting off simpl_loop]
1495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1496 It is very important not to iterate in simpl_loop unless there is a chance
1497 of progress. Trac #8474 is a classic example:
1498
1499 * There's a deeply-nested chain of implication constraints.
1500 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1501
1502 * From the innermost one we get a [D] alpha ~ Int,
1503 but alpha is untouchable until we get out to the outermost one
1504
1505 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1506 is untouchable, the solveInteract in simpl_loop makes no progress
1507
1508 * So there is no point in attempting to re-solve
1509 ?yn:betan => [W] ?x:Int
1510 via solveNestedImplications, because we'll just get the
1511 same [D] again
1512
1513 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1514 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1515 exponentially many) iterations!
1516
1517 Conclusion: we should call solveNestedImplications only if we did
1518 some unifiction in solveSimpleWanteds; because that's the only way
1519 we'll get more Givens (a unificaiton is like adding a Given) to
1520 allow the implication to make progress.
1521 -}
1522
1523 promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
1524 -- When we float a constraint out of an implication we must restore
1525 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1526 -- See Note [Promoting unification variables]
1527 promoteTyVar tclvl tv
1528 | isFloatedTouchableMetaTyVar tclvl tv
1529 = do { cloned_tv <- TcM.cloneMetaTyVar tv
1530 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1531 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
1532 | otherwise
1533 = return ()
1534
1535 promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
1536 -- When we float a constraint out of an implication we must restore
1537 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1538 -- See Note [Promoting unification variables]
1539 -- We don't just call promoteTyVar because we want to use unifyTyVar,
1540 -- not writeMetaTyVar
1541 promoteTyVarTcS tclvl tv
1542 | isFloatedTouchableMetaTyVar tclvl tv
1543 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1544 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1545 ; unifyTyVar tv (mkTyVarTy rhs_tv) }
1546 | otherwise
1547 = return ()
1548
1549 -- | If the tyvar is a RuntimeRep var, set it to PtrRepLifted. Returns whether or
1550 -- not this happened.
1551 defaultTyVar :: TcTyVar -> TcM ()
1552 -- Precondition: MetaTyVars only
1553 -- See Note [DefaultTyVar]
1554 defaultTyVar the_tv
1555 | isRuntimeRepVar the_tv
1556 = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
1557 ; writeMetaTyVar the_tv ptrRepLiftedTy }
1558
1559 | otherwise = return () -- The common case
1560
1561 -- | Like 'defaultTyVar', but in the TcS monad.
1562 defaultTyVarTcS :: TcTyVar -> TcS Bool
1563 defaultTyVarTcS the_tv
1564 | isRuntimeRepVar the_tv
1565 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
1566 ; unifyTyVar the_tv ptrRepLiftedTy
1567 ; return True }
1568 | otherwise
1569 = return False -- the common case
1570
1571 approximateWC :: WantedConstraints -> Cts
1572 -- Postcondition: Wanted or Derived Cts
1573 -- See Note [ApproximateWC]
1574 approximateWC wc
1575 = float_wc emptyVarSet wc
1576 where
1577 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
1578 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1579 = filterBag is_floatable simples `unionBags`
1580 do_bag (float_implic new_trapping_tvs) implics
1581 where
1582 is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` new_trapping_tvs
1583 new_trapping_tvs = transCloVarSet grow trapping_tvs
1584
1585 grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
1586 grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
1587 grow_one so_far ct tvs
1588 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
1589 | otherwise = tvs
1590 where
1591 ct_tvs = tyCoVarsOfCt ct
1592
1593 float_implic :: TcTyCoVarSet -> Implication -> Cts
1594 float_implic trapping_tvs imp
1595 | ic_no_eqs imp -- No equalities, so float
1596 = float_wc new_trapping_tvs (ic_wanted imp)
1597 | otherwise -- Don't float out of equalities
1598 = emptyCts -- See Note [ApproximateWC]
1599 where
1600 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1601 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1602 do_bag f = foldrBag (unionBags.f) emptyBag
1603
1604 {-
1605 Note [ApproximateWC]
1606 ~~~~~~~~~~~~~~~~~~~~
1607 approximateWC takes a constraint, typically arising from the RHS of a
1608 let-binding whose type we are *inferring*, and extracts from it some
1609 *simple* constraints that we might plausibly abstract over. Of course
1610 the top-level simple constraints are plausible, but we also float constraints
1611 out from inside, if they are not captured by skolems.
1612
1613 The same function is used when doing type-class defaulting (see the call
1614 to applyDefaultingRules) to extract constraints that that might be defaulted.
1615
1616 There are two caveats:
1617
1618 1. We do *not* float anything out if the implication binds equality
1619 constraints, because that defeats the OutsideIn story. Consider
1620 data T a where
1621 TInt :: T Int
1622 MkT :: T a
1623
1624 f TInt = 3::Int
1625
1626 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1627 f :: T a -> res
1628 We don't want to float (res~Int) out because then we'll infer
1629 f :: T a -> Int
1630 which is only on of the possible types. (GHC 7.6 accidentally *did*
1631 float out of such implications, which meant it would happily infer
1632 non-principal types.)
1633
1634 2. We do not float out an inner constraint that shares a type variable
1635 (transitively) with one that is trapped by a skolem. Eg
1636 forall a. F a ~ beta, Integral beta
1637 We don't want to float out (Integral beta). Doing so would be bad
1638 when defaulting, because then we'll default beta:=Integer, and that
1639 makes the error message much worse; we'd get
1640 Can't solve F a ~ Integer
1641 rather than
1642 Can't solve Integral (F a)
1643
1644 Moreover, floating out these "contaminated" constraints doesn't help
1645 when generalising either. If we generalise over (Integral b), we still
1646 can't solve the retained implication (forall a. F a ~ b). Indeed,
1647 arguably that too would be a harder error to understand.
1648
1649 Note [DefaultTyVar]
1650 ~~~~~~~~~~~~~~~~~~~
1651 defaultTyVar is used on any un-instantiated meta type variables to
1652 default any RuntimeRep variables to PtrRepLifted. This is important
1653 to ensure that instance declarations match. For example consider
1654
1655 instance Show (a->b)
1656 foo x = show (\_ -> True)
1657
1658 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
1659 and that won't match the typeKind (*) in the instance decl. See tests
1660 tc217 and tc175.
1661
1662 We look only at touchable type variables. No further constraints
1663 are going to affect these type variables, so it's time to do it by
1664 hand. However we aren't ready to default them fully to () or
1665 whatever, because the type-class defaulting rules have yet to run.
1666
1667 An alternate implementation would be to emit a derived constraint setting
1668 the RuntimeRep variable to PtrRepLifted, but this seems unnecessarily indirect.
1669
1670 Note [Promote _and_ default when inferring]
1671 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1672 When we are inferring a type, we simplify the constraint, and then use
1673 approximateWC to produce a list of candidate constraints. Then we MUST
1674
1675 a) Promote any meta-tyvars that have been floated out by
1676 approximateWC, to restore invariant (MetaTvInv) described in
1677 Note [TcLevel and untouchable type variables] in TcType.
1678
1679 b) Default the kind of any meta-tyyvars that are not mentioned in
1680 in the environment.
1681
1682 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1683 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1684 should! If we don't solve the constraint, we'll stupidly quantify over
1685 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1686 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1687 Trac #7641 is a simpler example.
1688
1689 Note [Promoting unification variables]
1690 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1691 When we float an equality out of an implication we must "promote" free
1692 unification variables of the equality, in order to maintain Invariant
1693 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1694 leftover implication.
1695
1696 This is absolutely necessary. Consider the following example. We start
1697 with two implications and a class with a functional dependency.
1698
1699 class C x y | x -> y
1700 instance C [a] [a]
1701
1702 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1703 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1704
1705 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1706 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1707 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1708 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1709 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1710
1711 class C x y | x -> y where
1712 op :: x -> y -> ()
1713
1714 instance C [a] [a]
1715
1716 type family F a :: *
1717
1718 h :: F Int -> ()
1719 h = undefined
1720
1721 data TEx where
1722 TEx :: a -> TEx
1723
1724 f (x::beta) =
1725 let g1 :: forall b. b -> ()
1726 g1 _ = h [x]
1727 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1728 in (g1 '3', g2 undefined)
1729
1730
1731 Note [Solving Family Equations]
1732 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1733 After we are done with simplification we may be left with constraints of the form:
1734 [Wanted] F xis ~ beta
1735 If 'beta' is a touchable unification variable not already bound in the TyBinds
1736 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1737
1738 When is it ok to do so?
1739 1) 'beta' must not already be defaulted to something. Example:
1740
1741 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1742 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1743 have to report this as unsolved.
1744
1745 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1746 set [beta := F xis] only if beta is not among the free variables of xis.
1747
1748 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1749 of type family equations. See Inert Set invariants in TcInteract.
1750
1751 This solving is now happening during zonking, see Note [Unflattening while zonking]
1752 in TcMType.
1753
1754
1755 *********************************************************************************
1756 * *
1757 * Floating equalities *
1758 * *
1759 *********************************************************************************
1760
1761 Note [Float Equalities out of Implications]
1762 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1763 For ordinary pattern matches (including existentials) we float
1764 equalities out of implications, for instance:
1765 data T where
1766 MkT :: Eq a => a -> T
1767 f x y = case x of MkT _ -> (y::Int)
1768 We get the implication constraint (x::T) (y::alpha):
1769 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1770 We want to float out the equality into a scope where alpha is no
1771 longer untouchable, to solve the implication!
1772
1773 But we cannot float equalities out of implications whose givens may
1774 yield or contain equalities:
1775
1776 data T a where
1777 T1 :: T Int
1778 T2 :: T Bool
1779 T3 :: T a
1780
1781 h :: T a -> a -> Int
1782
1783 f x y = case x of
1784 T1 -> y::Int
1785 T2 -> y::Bool
1786 T3 -> h x y
1787
1788 We generate constraint, for (x::T alpha) and (y :: beta):
1789 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1790 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1791 (alpha ~ beta) -- From 3rd branch
1792
1793 If we float the equality (beta ~ Int) outside of the first implication and
1794 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1795 But if we just leave them inside the implications, we unify alpha := beta and
1796 solve everything.
1797
1798 Principle:
1799 We do not want to float equalities out which may
1800 need the given *evidence* to become soluble.
1801
1802 Consequence: classes with functional dependencies don't matter (since there is
1803 no evidence for a fundep equality), but equality superclasses do matter (since
1804 they carry evidence).
1805 -}
1806
1807 floatEqualities :: [TcTyVar] -> Bool
1808 -> WantedConstraints
1809 -> TcS (Cts, WantedConstraints)
1810 -- Main idea: see Note [Float Equalities out of Implications]
1811 --
1812 -- Precondition: the wc_simple of the incoming WantedConstraints are
1813 -- fully zonked, so that we can see their free variables
1814 --
1815 -- Postcondition: The returned floated constraints (Cts) are only
1816 -- Wanted or Derived
1817 --
1818 -- Also performs some unifications (via promoteTyVar), adding to
1819 -- monadically-carried ty_binds. These will be used when processing
1820 -- floated_eqs later
1821 --
1822 -- Subtleties: Note [Float equalities from under a skolem binding]
1823 -- Note [Skolem escape]
1824 floatEqualities skols no_given_eqs
1825 wanteds@(WC { wc_simple = simples })
1826 | not no_given_eqs -- There are some given equalities, so don't float
1827 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1828 | otherwise
1829 = do { outer_tclvl <- TcS.getTcLevel
1830 ; mapM_ (promoteTyVarTcS outer_tclvl)
1831 (tyCoVarsOfCtsList float_eqs)
1832 -- See Note [Promoting unification variables]
1833
1834 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1835 , text "Simples =" <+> ppr simples
1836 , text "Floated eqs =" <+> ppr float_eqs])
1837 ; return ( float_eqs
1838 , wanteds { wc_simple = remaining_simples } ) }
1839 where
1840 skol_set = mkVarSet skols
1841 (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
1842
1843 usefulToFloat :: VarSet -> Ct -> Bool
1844 usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
1845 = is_meta_var_eq pred &&
1846 (tyCoVarsOfType pred `disjointVarSet` skol_set)
1847 where
1848 pred = ctPred ct
1849
1850 -- Float out alpha ~ ty, or ty ~ alpha
1851 -- which might be unified outside
1852 -- See Note [Which equalities to float]
1853 is_meta_var_eq pred
1854 | EqPred NomEq ty1 ty2 <- classifyPredType pred
1855 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
1856 (Just tv1, _) -> float_tv_eq tv1 ty2
1857 (_, Just tv2) -> float_tv_eq tv2 ty1
1858 _ -> False
1859 | otherwise
1860 = False
1861
1862 float_tv_eq tv1 ty2 -- See Note [Which equalities to float]
1863 = isMetaTyVar tv1
1864 && (not (isSigTyVar tv1) || isTyVarTy ty2)
1865
1866 {- Note [Float equalities from under a skolem binding]
1867 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1868 Which of the simple equalities can we float out? Obviously, only
1869 ones that don't mention the skolem-bound variables. But that is
1870 over-eager. Consider
1871 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1872 The second constraint doesn't mention 'a'. But if we float it,
1873 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1874 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1875 we left with the constraint
1876 [2] forall a. a ~ gamma'[1]
1877 which is insoluble because gamma became untouchable.
1878
1879 Solution: float only constraints that stand a jolly good chance of
1880 being soluble simply by being floated, namely ones of form
1881 a ~ ty
1882 where 'a' is a currently-untouchable unification variable, but may
1883 become touchable by being floated (perhaps by more than one level).
1884
1885 We had a very complicated rule previously, but this is nice and
1886 simple. (To see the notes, look at this Note in a version of
1887 TcSimplify prior to Oct 2014).
1888
1889 Note [Which equalities to float]
1890 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1891 Which equalities should we float? We want to float ones where there
1892 is a decent chance that floating outwards will allow unification to
1893 happen. In particular:
1894
1895 Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
1896
1897 * alpha is a meta-tyvar.
1898
1899 * And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that
1900 case, floating out won't help either, and it may affect grouping
1901 of error messages.
1902
1903 Note [Skolem escape]
1904 ~~~~~~~~~~~~~~~~~~~~
1905 You might worry about skolem escape with all this floating.
1906 For example, consider
1907 [2] forall a. (a ~ F beta[2] delta,
1908 Maybe beta[2] ~ gamma[1])
1909
1910 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1911 solve with gamma := beta. But what if later delta:=Int, and
1912 F b Int = b.
1913 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1914 skolem has escaped!
1915
1916 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1917 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1918
1919
1920 *********************************************************************************
1921 * *
1922 * Defaulting and disamgiguation *
1923 * *
1924 *********************************************************************************
1925 -}
1926
1927 applyDefaultingRules :: WantedConstraints -> TcS Bool
1928 -- True <=> I did some defaulting, by unifying a meta-tyvar
1929 -- Imput WantedConstraints are not necessarily zonked
1930
1931 applyDefaultingRules wanteds
1932 | isEmptyWC wanteds
1933 = return False
1934 | otherwise
1935 = do { info@(default_tys, _) <- getDefaultInfo
1936 ; wanteds <- TcS.zonkWC wanteds
1937
1938 ; let groups = findDefaultableGroups info wanteds
1939
1940 ; traceTcS "applyDefaultingRules {" $
1941 vcat [ text "wanteds =" <+> ppr wanteds
1942 , text "groups =" <+> ppr groups
1943 , text "info =" <+> ppr info ]
1944
1945 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1946
1947 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1948
1949 ; return (or something_happeneds) }
1950
1951 findDefaultableGroups
1952 :: ( [Type]
1953 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1954 -> WantedConstraints -- Unsolved (wanted or derived)
1955 -> [(TyVar, [Ct])]
1956 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1957 | null default_tys
1958 = []
1959 | otherwise
1960 = [ (tv, map fstOf3 group)
1961 | group@((_,_,tv):_) <- unary_groups
1962 , defaultable_tyvar tv
1963 , defaultable_classes (map sndOf3 group) ]
1964 where
1965 simples = approximateWC wanteds
1966 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
1967 unary_groups = equivClasses cmp_tv unaries
1968
1969 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
1970 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
1971 non_unaries :: [Ct] -- and *other* constraints
1972
1973 -- Finds unary type-class constraints
1974 -- But take account of polykinded classes like Typeable,
1975 -- which may look like (Typeable * (a:*)) (Trac #8931)
1976 find_unary cc
1977 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
1978 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
1979 -- Ignore invisible arguments for this purpose
1980 , Just tv <- tcGetTyVar_maybe ty
1981 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
1982 -- we definitely don't want to try to assign to those!
1983 = Left (cc, cls, tv)
1984 find_unary cc = Right cc -- Non unary or non dictionary
1985
1986 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
1987 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
1988
1989 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1990
1991 defaultable_tyvar tv
1992 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1993 b2 = not (tv `elemVarSet` bad_tvs)
1994 in b1 && b2
1995
1996 defaultable_classes clss
1997 | extended_defaults = any isInteractiveClass clss
1998 | otherwise = all is_std_class clss && (any is_num_class clss)
1999
2000 -- In interactive mode, or with -XExtendedDefaultRules,
2001 -- we default Show a to Show () to avoid graututious errors on "show []"
2002 isInteractiveClass cls
2003 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey
2004 , ordClassKey, foldableClassKey
2005 , traversableClassKey])
2006
2007 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2008 -- is_num_class adds IsString to the standard numeric classes,
2009 -- when -foverloaded-strings is enabled
2010
2011 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2012 -- Similarly is_std_class
2013
2014 ------------------------------
2015 disambigGroup :: [Type] -- The default types
2016 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
2017 -- sharing same type variable
2018 -> TcS Bool -- True <=> something happened, reflected in ty_binds
2019
2020 disambigGroup [] _
2021 = return False
2022 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
2023 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
2024 ; fake_ev_binds_var <- TcS.newTcEvBinds
2025 ; tclvl <- TcS.getTcLevel
2026 ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet
2027 (pushTcLevel tclvl) try_group
2028
2029 ; if success then
2030 -- Success: record the type variable binding, and return
2031 do { unifyTyVar the_tv default_ty
2032 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
2033 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
2034 ; return True }
2035 else
2036 -- Failure: try with the next type
2037 do { traceTcS "disambigGroup failed, will try other default types }"
2038 (ppr default_ty)
2039 ; disambigGroup default_tys group } }
2040 where
2041 try_group
2042 | Just subst <- mb_subst
2043 = do { lcl_env <- TcS.getLclEnv
2044 ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
2045 , ctl_env = lcl_env
2046 , ctl_t_or_k = Nothing
2047 , ctl_depth = initialSubGoalDepth }
2048 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
2049 wanteds
2050 ; fmap isEmptyWC $
2051 solveSimpleWanteds $ listToBag $
2052 map mkNonCanonical wanted_evs }
2053
2054 | otherwise
2055 = return False
2056
2057 the_ty = mkTyVarTy the_tv
2058 mb_subst = tcMatchTy the_ty default_ty
2059 -- Make sure the kinds match too; hence this call to tcMatchTy
2060 -- E.g. suppose the only constraint was (Typeable k (a::k))
2061 -- With the addition of polykinded defaulting we also want to reject
2062 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2063
2064
2065 {-
2066 Note [Avoiding spurious errors]
2067 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2068 When doing the unification for defaulting, we check for skolem
2069 type variables, and simply don't default them. For example:
2070 f = (*) -- Monomorphic
2071 g :: Num a => a -> a
2072 g x = f x x
2073 Here, we get a complaint when checking the type signature for g,
2074 that g isn't polymorphic enough; but then we get another one when
2075 dealing with the (Num a) context arising from f's definition;
2076 we try to unify a with Int (to default it), but find that it's
2077 already been unified with the rigid variable from g's type sig.
2078 -}