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