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