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