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