New handling of overlapping inst in Safe Haskell
[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 TuplePred {} -> False
618
619 pick_cls_pred flex_ctxt tys
620 = tyVarsOfTypes tys `intersectsVarSet` qtvs
621 && (checkValidClsArgs flex_ctxt tys)
622 -- Only quantify over predicates that checkValidType
623 -- will pass! See Trac #10351.
624
625 -- See Note [Quantifying over equality constraints]
626 quant_fun ty
627 = case tcSplitTyConApp_maybe ty of
628 Just (tc, tys) | isTypeFamilyTyCon tc
629 -> tyVarsOfTypes tys `intersectsVarSet` qtvs
630 _ -> False
631
632 ------------------
633 growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
634 -- See Note [Growing the tau-tvs using constraints]
635 growThetaTyVars theta tvs
636 | null theta = tvs
637 | otherwise = transCloVarSet mk_next seed_tvs
638 where
639 seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips
640 (ips, non_ips) = partition isIPPred theta
641 -- See note [Inheriting implicit parameters]
642
643 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
644 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
645 grow_one so_far pred tvs
646 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
647 | otherwise = tvs
648 where
649 pred_tvs = tyVarsOfType pred
650
651 {-
652 Note [Quantifying over equality constraints]
653 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
654 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
655 Doing so may simply postpone a type error from the function definition site to
656 its call site. (At worst, imagine (Int ~ Bool)).
657
658 However, consider this
659 forall a. (F [a] ~ Int) => blah
660 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
661 site we will know 'a', and perhaps we have instance F [Bool] = Int.
662 So we *do* quantify over a type-family equality where the arguments mention
663 the quantified variables.
664
665 Note [Growing the tau-tvs using constraints]
666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
667 (growThetaTyVars insts tvs) is the result of extending the set
668 of tyvars tvs using all conceivable links from pred
669
670 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
671 Then growThetaTyVars preds tvs = {a,b,c}
672
673 Notice that
674 growThetaTyVars is conservative if v might be fixed by vs
675 => v `elem` grow(vs,C)
676
677 Note [Inheriting implicit parameters]
678 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679 Consider this:
680
681 f x = (x::Int) + ?y
682
683 where f is *not* a top-level binding.
684 From the RHS of f we'll get the constraint (?y::Int).
685 There are two types we might infer for f:
686
687 f :: Int -> Int
688
689 (so we get ?y from the context of f's definition), or
690
691 f :: (?y::Int) => Int -> Int
692
693 At first you might think the first was better, because then
694 ?y behaves like a free variable of the definition, rather than
695 having to be passed at each call site. But of course, the WHOLE
696 IDEA is that ?y should be passed at each call site (that's what
697 dynamic binding means) so we'd better infer the second.
698
699 BOTTOM LINE: when *inferring types* you must quantify over implicit
700 parameters, *even if* they don't mention the bound type variables.
701 Reason: because implicit parameters, uniquely, have local instance
702 declarations. See the pickQuantifiablePreds.
703
704 Note [Quantification with errors]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 If we find that the RHS of the definition has some absolutely-insoluble
707 constraints, we abandon all attempts to find a context to quantify
708 over, and instead make the function fully-polymorphic in whatever
709 type we have found. For two reasons
710 a) Minimise downstream errors
711 b) Avoid spurious errors from this function
712
713 But NB that we must include *derived* errors in the check. Example:
714 (a::*) ~ Int#
715 We get an insoluble derived error *~#, and we don't want to discard
716 it before doing the isInsolubleWC test! (Trac #8262)
717
718 Note [Default while Inferring]
719 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 Our current plan is that defaulting only happens at simplifyTop and
721 not simplifyInfer. This may lead to some insoluble deferred constraints
722 Example:
723
724 instance D g => C g Int b
725
726 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
727 type inferred = gamma -> gamma
728
729 Now, if we try to default (alpha := Int) we will be able to refine the implication to
730 (forall b. 0 => C gamma Int b)
731 which can then be simplified further to
732 (forall b. 0 => D gamma)
733 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
734 type: forall g. D g => g -> g
735
736 Instead what will currently happen is that we will get a quantified type
737 (forall g. g -> g) and an implication:
738 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
739
740 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
741 unsolvable implication:
742 forall g. 0 => (forall b. 0 => D g)
743
744 The concrete example would be:
745 h :: C g a s => g -> a -> ST s a
746 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
747
748 But it is quite tedious to do defaulting and resolve the implication constraints and
749 we have not observed code breaking because of the lack of defaulting in inference so
750 we don't do it for now.
751
752
753
754 Note [Minimize by Superclasses]
755 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
756 When we quantify over a constraint, in simplifyInfer we need to
757 quantify over a constraint that is minimal in some sense: For
758 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
759 we'd like to quantify over Ord alpha, because we can just get Eq alpha
760 from superclass selection from Ord alpha. This minimization is what
761 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
762 to check the original wanted.
763
764
765 Note [Avoid unecessary constraint simplification]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 -------- NB NB NB (Jun 12) -------------
768 This note not longer applies; see the notes with Trac #4361.
769 But I'm leaving it in here so we remember the issue.)
770 ----------------------------------------
771 When inferring the type of a let-binding, with simplifyInfer,
772 try to avoid unnecessarily simplifying class constraints.
773 Doing so aids sharing, but it also helps with delicate
774 situations like
775
776 instance C t => C [t] where ..
777
778 f :: C [t] => ....
779 f x = let g y = ...(constraint C [t])...
780 in ...
781 When inferring a type for 'g', we don't want to apply the
782 instance decl, because then we can't satisfy (C t). So we
783 just notice that g isn't quantified over 't' and partition
784 the constraints before simplifying.
785
786 This only half-works, but then let-generalisation only half-works.
787
788
789 *********************************************************************************
790 * *
791 * Main Simplifier *
792 * *
793 ***********************************************************************************
794
795 Note [Deferring coercion errors to runtime]
796 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
797 While developing, sometimes it is desirable to allow compilation to succeed even
798 if there are type errors in the code. Consider the following case:
799
800 module Main where
801
802 a :: Int
803 a = 'a'
804
805 main = print "b"
806
807 Even though `a` is ill-typed, it is not used in the end, so if all that we're
808 interested in is `main` it is handy to be able to ignore the problems in `a`.
809
810 Since we treat type equalities as evidence, this is relatively simple. Whenever
811 we run into a type mismatch in TcUnify, we normally just emit an error. But it
812 is always safe to defer the mismatch to the main constraint solver. If we do
813 that, `a` will get transformed into
814
815 co :: Int ~ Char
816 co = ...
817
818 a :: Int
819 a = 'a' `cast` co
820
821 The constraint solver would realize that `co` is an insoluble constraint, and
822 emit an error with `reportUnsolved`. But we can also replace the right-hand side
823 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
824 to compile, and it will run fine unless we evaluate `a`. This is what
825 `deferErrorsToRuntime` does.
826
827 It does this by keeping track of which errors correspond to which coercion
828 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
829 and does not fail if -fdefer-type-errors is on, so that we can continue
830 compilation. The errors are turned into warnings in `reportUnsolved`.
831 -}
832
833 solveWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
834 -- Simplify the input constraints
835 -- Discard the evidence binds
836 -- Discards all Derived stuff in result
837 -- Result is /not/ guaranteed zonked
838 solveWantedsTcM wanted
839 = do { (wanted1, _binds) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
840 ; return wanted1 }
841
842 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
843 -- Since solveWanteds returns the residual WantedConstraints,
844 -- it should always be called within a runTcS or something similar,
845 -- Result is not zonked
846 solveWantedsAndDrop wanted
847 = do { wc <- solveWanteds wanted
848 ; return (dropDerivedWC wc) }
849
850 solveWanteds :: WantedConstraints -> TcS WantedConstraints
851 -- so that the inert set doesn't mindlessly propagate.
852 -- NB: wc_simples may be wanted /or/ derived now
853 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
854 = do { traceTcS "solveWanteds {" (ppr wc)
855
856 -- Try the simple bit, including insolubles. Solving insolubles a
857 -- second time round is a bit of a waste; but the code is simple
858 -- and the program is wrong anyway, and we don't run the danger
859 -- of adding Derived insolubles twice; see
860 -- TcSMonad Note [Do not add duplicate derived insolubles]
861 ; wc1 <- solveSimpleWanteds simples
862 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
863
864 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
865
866 ; final_wc <- simpl_loop 0 floated_eqs
867 (WC { wc_simple = simples1, wc_impl = implics2
868 , wc_insol = insols `unionBags` insols1 })
869
870 ; bb <- getTcEvBindsMap
871 ; traceTcS "solveWanteds }" $
872 vcat [ text "final wc =" <+> ppr final_wc
873 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
874
875 ; return final_wc }
876
877 simpl_loop :: Int -> Cts
878 -> WantedConstraints
879 -> TcS WantedConstraints
880 simpl_loop n floated_eqs
881 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
882 | n > 10
883 = do { traceTcS "solveWanteds: loop!" (ppr wc); return wc }
884
885 | no_floated_eqs
886 = return wc -- Done!
887
888 | otherwise
889 = do { traceTcS "simpl_loop, iteration" (int n)
890
891 -- solveSimples may make progress if either float_eqs hold
892 ; (unifs_happened1, wc1) <- if no_floated_eqs
893 then return (False, emptyWC)
894 else reportUnifications $
895 solveSimpleWanteds (floated_eqs `unionBags` simples)
896 -- Put floated_eqs first so they get solved first
897 -- NB: the floated_eqs may include /derived/ equalities
898 -- arising from fundeps inside an implication
899
900 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
901
902 -- solveImplications may make progress only if unifs2 holds
903 ; (floated_eqs2, implics2) <- if not unifs_happened1 && isEmptyBag implics1
904 then return (emptyBag, implics)
905 else solveNestedImplications (implics `unionBags` implics1)
906
907 ; simpl_loop (n+1) floated_eqs2
908 (WC { wc_simple = simples1, wc_impl = implics2
909 , wc_insol = insols `unionBags` insols1 }) }
910
911 where
912 no_floated_eqs = isEmptyBag floated_eqs
913
914 solveNestedImplications :: Bag Implication
915 -> TcS (Cts, Bag Implication)
916 -- Precondition: the TcS inerts may contain unsolved simples which have
917 -- to be converted to givens before we go inside a nested implication.
918 solveNestedImplications implics
919 | isEmptyBag implics
920 = return (emptyBag, emptyBag)
921 | otherwise
922 = do { traceTcS "solveNestedImplications starting {" empty
923 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
924 ; let floated_eqs = concatBag floated_eqs_s
925
926 -- ... and we are back in the original TcS inerts
927 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
928 -- them in the beginning of this function.
929 ; traceTcS "solveNestedImplications end }" $
930 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
931 , text "unsolved_implics =" <+> ppr unsolved_implics ]
932
933 ; return (floated_eqs, catBagMaybes unsolved_implics) }
934
935 solveImplication :: Implication -- Wanted
936 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
937 Maybe Implication) -- Simplified implication (empty or singleton)
938 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
939 -- which after trying to solve this implication we must restore to their original value
940 solveImplication imp@(Implic { ic_tclvl = tclvl
941 , ic_binds = ev_binds
942 , ic_skols = skols
943 , ic_given = givens
944 , ic_wanted = wanteds
945 , ic_info = info
946 , ic_status = status
947 , ic_env = env })
948 | IC_Solved {} <- status
949 = return (emptyCts, Just imp) -- Do nothing
950
951 | otherwise -- Even for IC_Insoluble it is worth doing more work
952 -- The insoluble stuff might be in one sub-implication
953 -- and other unsolved goals in another; and we want to
954 -- solve the latter as much as possible
955 = do { inerts <- getTcSInerts
956 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
957
958 -- Solve the nested constraints
959 ; (no_given_eqs, given_insols, residual_wanted)
960 <- nestImplicTcS ev_binds tclvl $
961 do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens
962 ; no_eqs <- getNoGivenEqs tclvl skols
963
964 ; residual_wanted <- solveWanteds wanteds
965 -- solveWanteds, *not* solveWantedsAndDrop, because
966 -- we want to retain derived equalities so we can float
967 -- them out in floatEqualities
968
969 ; return (no_eqs, given_insols, residual_wanted) }
970
971 ; (floated_eqs, residual_wanted)
972 <- floatEqualities skols no_given_eqs residual_wanted
973
974 ; let final_wanted = residual_wanted `addInsols` given_insols
975
976 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
977 , ic_wanted = final_wanted })
978
979 ; evbinds <- getTcEvBindsMap
980 ; traceTcS "solveImplication end }" $ vcat
981 [ text "no_given_eqs =" <+> ppr no_given_eqs
982 , text "floated_eqs =" <+> ppr floated_eqs
983 , text "res_implic =" <+> ppr res_implic
984 , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
985
986 ; return (floated_eqs, res_implic) }
987
988 ----------------------
989 setImplicationStatus :: Implication -> TcS (Maybe Implication)
990 -- Finalise the implication returned from solveImplication:
991 -- * Set the ic_status field
992 -- * Trim the ic_wanted field to remove Derived constraints
993 -- Return Nothing if we can discard the implication altogether
994 setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _
995 , ic_info = info
996 , ic_wanted = wc
997 , ic_given = givens })
998 | some_insoluble
999 = return $ Just $
1000 implic { ic_status = IC_Insoluble
1001 , ic_wanted = wc { wc_simple = pruned_simples
1002 , wc_insol = pruned_insols } }
1003
1004 | some_unsolved
1005 = return $ Just $
1006 implic { ic_status = IC_Unsolved
1007 , ic_wanted = wc { wc_simple = pruned_simples
1008 , wc_insol = pruned_insols } }
1009
1010 | otherwise -- Everything is solved; look at the implications
1011 -- See Note [Tracking redundant constraints]
1012 = do { ev_binds <- TcS.readTcRef ev_binds_var
1013 ; let all_needs = neededEvVars ev_binds implic_needs
1014
1015 dead_givens | warnRedundantGivens info
1016 = filterOut (`elemVarSet` all_needs) givens
1017 | otherwise = [] -- None to report
1018
1019 final_needs = all_needs `delVarSetList` givens
1020
1021 discard_entire_implication -- Can we discard the entire implication?
1022 = null dead_givens -- No warning from this implication
1023 && isEmptyBag pruned_implics -- No live children
1024 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
1025
1026 final_status = IC_Solved { ics_need = final_needs
1027 , ics_dead = dead_givens }
1028 final_implic = implic { ic_status = final_status
1029 , ic_wanted = wc { wc_simple = pruned_simples
1030 , wc_insol = pruned_insols
1031 , wc_impl = pruned_implics } }
1032 -- We can only prune the child implications (pruned_implics)
1033 -- in the IC_Solved status case, because only then we can
1034 -- accumulate their needed evidence variales into the
1035 -- IC_Solved final_status field of the parent implication.
1036
1037 ; return $ if discard_entire_implication
1038 then Nothing
1039 else Just final_implic }
1040 where
1041 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
1042
1043 some_insoluble = insolubleWC wc
1044 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
1045 || isNothing mb_implic_needs
1046
1047 pruned_simples = dropDerivedSimples simples
1048 pruned_insols = dropDerivedInsols insols
1049 pruned_implics = filterBag need_to_keep_implic implics
1050
1051 mb_implic_needs :: Maybe VarSet
1052 -- Just vs => all implics are IC_Solved, with 'vs' needed
1053 -- Nothing => at least one implic is not IC_Solved
1054 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
1055 Just implic_needs = mb_implic_needs
1056
1057 add_implic implic acc
1058 | Just vs_acc <- acc
1059 , IC_Solved { ics_need = vs } <- ic_status implic
1060 = Just (vs `unionVarSet` vs_acc)
1061 | otherwise = Nothing
1062
1063 need_to_keep_implic ic
1064 | IC_Solved { ics_dead = [] } <- ic_status ic
1065 -- Fully solved, and no redundant givens to report
1066 , isEmptyBag (wc_impl (ic_wanted ic))
1067 -- And no children that might have things to report
1068 = False
1069 | otherwise
1070 = True
1071
1072 warnRedundantGivens :: SkolemInfo -> Bool
1073 warnRedundantGivens (SigSkol ctxt _)
1074 = case ctxt of
1075 FunSigCtxt _ warn_redundant -> warn_redundant
1076 ExprSigCtxt -> True
1077 _ -> False
1078 warnRedundantGivens InstSkol = True
1079 warnRedundantGivens _ = False
1080
1081 neededEvVars :: EvBindMap -> VarSet -> VarSet
1082 -- Find all the evidence variables that are "needed",
1083 -- and then delete all those bound by the evidence bindings
1084 -- A variable is "needed" if
1085 -- a) it is free in the RHS of a Wanted EvBind (add_wanted)
1086 -- b) it is free in the RHS of an EvBind whose LHS is needed (transClo)
1087 -- c) it is in the ic_need_evs of a nested implication (initial_seeds)
1088 -- (after removing the givens)
1089 neededEvVars ev_binds initial_seeds
1090 = needed `minusVarSet` bndrs
1091 where
1092 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
1093 needed = transCloVarSet also_needs seeds
1094 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
1095
1096 add_wanted :: EvBind -> VarSet -> VarSet
1097 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1098 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1099 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1100
1101 also_needs :: VarSet -> VarSet
1102 also_needs needs
1103 = foldVarSet add emptyVarSet needs
1104 where
1105 add v needs
1106 | Just ev_bind <- lookupEvBind ev_binds v
1107 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
1108 , is_given
1109 = evVarsOfTerm rhs `unionVarSet` needs
1110 | otherwise
1111 = needs
1112
1113 add_bndr :: EvBind -> VarSet -> VarSet
1114 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
1115
1116
1117 {-
1118 Note [Tracking redundant constraints]
1119 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1120 With Opt_WarnRedundantConstraints, GHC can report which
1121 constraints of a type signature (or instance declaration) are
1122 redundant, and can be omitted. Here is an overview of how it
1123 works:
1124
1125 ----- What is a redudant constraint?
1126
1127 * The things that can be redundant are precisely the Given
1128 constraints of an implication.
1129
1130 * A constraint can be redundant in two different ways:
1131 a) It is implied by other givens. E.g.
1132 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1133 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1134 b) It is not needed by the Wanted constraints covered by the
1135 implication E.g.
1136 f :: Eq a => a -> Bool
1137 f x = True -- Equality not uesd
1138
1139 * To find (a), when we have two Given constraints,
1140 we must be careful to drop the one that is a naked variable (if poss).
1141 So if we have
1142 f :: (Eq a, Ord a) => blah
1143 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1144 [G] d2 :: Eq a
1145 We want to discard d2 in favour of the superclass selection from
1146 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1147 See Note [Replacement vs keeping].
1148
1149 * To find (b) we need to know which evidence bindings are 'wanted';
1150 hence the eb_is_given field on an EvBind.
1151
1152 ----- How tracking works
1153
1154 * When the constraint solver finishes solving all the wanteds in
1155 an implication, it sets its status to IC_Solved
1156
1157 - The ics_dead field of IC_Solved records the subset of the ic_given
1158 of this implication that are redundant (not needed).
1159
1160 - The ics_need field of IC_Solved then records all the
1161 in-scope (given) evidence variables, bound by the context, that
1162 were needed to solve this implication, including all its nested
1163 implications. (We remove the ic_given of this implication from
1164 the set, of course.)
1165
1166 * We compute which evidence variables are needed by an implication
1167 in setImplicationStatus. A variable is needed if
1168 a) it is free in the RHS of a Wanted EvBind
1169 b) it is free in the RHS of an EvBind whose LHS is needed
1170 c) it is in the ics_need of a nested implication
1171
1172 * We need to be careful not to discard an implication
1173 prematurely, even one that is fully solved, because we might
1174 thereby forget which variables it needs, and hence wrongly
1175 report a constraint as redundant. But we can discard it once
1176 its free vars have been incorporated into its parent; or if it
1177 simply has no free vars. This careful discarding is also
1178 handled in setImplicationStatus
1179
1180 ----- Reporting redundant constraints
1181
1182 * TcErrors does the actual warning, in warnRedundantConstraints.
1183
1184 * We don't report redundant givens for *every* implication; only
1185 for those which reply True to TcSimplify.warnRedundantGivens:
1186
1187 - For example, in a class declaration, the default method *can*
1188 use the class constraint, but it certainly doesn't *have* to,
1189 and we don't want to report an error there.
1190
1191 - More subtly, in a function definition
1192 f :: (Ord a, Ord a, Ix a) => a -> a
1193 f x = rhs
1194 we do an ambiguity check on the type (which would find that one
1195 of the Ord a constraints was redundant), and then we check that
1196 the definition has that type (which might find that both are
1197 redundant). We don't want to report the same error twice, so
1198 we disable it for the ambiguity check. Hence the flag in
1199 TcType.FunSigCtxt.
1200
1201 This decision is taken in setImplicationStatus, rather than TcErrors
1202 so that we can discard implication constraints that we don't need.
1203 So ics_dead consists only of the *reportable* redundant givens.
1204
1205 ----- Shortcomings
1206
1207 Consider (see Trac #9939)
1208 f2 :: (Eq a, Ord a) => a -> a -> Bool
1209 -- Ord a redundant, but Eq a is reported
1210 f2 x y = (x == y)
1211
1212 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1213 really not easy to detect that!
1214
1215
1216 Note [Cutting off simpl_loop]
1217 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1218 It is very important not to iterate in simpl_loop unless there is a chance
1219 of progress. Trac #8474 is a classic example:
1220
1221 * There's a deeply-nested chain of implication constraints.
1222 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1223
1224 * From the innermost one we get a [D] alpha ~ Int,
1225 but alpha is untouchable until we get out to the outermost one
1226
1227 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1228 is untouchable, the solveInteract in simpl_loop makes no progress
1229
1230 * So there is no point in attempting to re-solve
1231 ?yn:betan => [W] ?x:Int
1232 because we'll just get the same [D] again
1233
1234 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1235 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1236 exponentially many) iterations!
1237
1238 Conclusion: we should iterate simpl_loop iff we will get more 'givens'
1239 in the inert set when solving the nested implications. That is the
1240 result of prepareInertsForImplications is larger. How can we tell
1241 this?
1242
1243 Consider floated_eqs (all wanted or derived):
1244
1245 (a) [W/D] CTyEqCan (a ~ ty). This can give rise to a new given only by causing
1246 a unification. So we count those unifications.
1247
1248 (b) [W] CFunEqCan (F tys ~ xi). Even though these are wanted, they
1249 are pushed in as givens by prepareInertsForImplications. See Note
1250 [Preparing inert set for implications] in TcSMonad. But because
1251 of that very fact, we won't generate another copy if we iterate
1252 simpl_loop. So we iterate if there any of these
1253 -}
1254
1255 promoteTyVar :: TcLevel -> TcTyVar -> TcS TcTyVar
1256 -- When we float a constraint out of an implication we must restore
1257 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1258 -- See Note [Promoting unification variables]
1259 promoteTyVar tclvl tv
1260 | isFloatedTouchableMetaTyVar tclvl tv
1261 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1262 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1263 ; unifyTyVar tv (mkTyVarTy rhs_tv)
1264 ; return rhs_tv }
1265 | otherwise
1266 = return tv
1267
1268 promoteAndDefaultTyVar :: TcLevel -> TcTyVarSet -> TcTyVar -> TcS TcTyVar
1269 -- See Note [Promote _and_ default when inferring]
1270 promoteAndDefaultTyVar tclvl gbl_tvs tv
1271 = do { tv1 <- if tv `elemVarSet` gbl_tvs
1272 then return tv
1273 else defaultTyVar tv
1274 ; promoteTyVar tclvl tv1 }
1275
1276 defaultTyVar :: TcTyVar -> TcS TcTyVar
1277 -- Precondition: MetaTyVars only
1278 -- See Note [DefaultTyVar]
1279 defaultTyVar the_tv
1280 | Just default_k <- defaultKind_maybe (tyVarKind the_tv)
1281 = do { tv' <- TcS.cloneMetaTyVar the_tv
1282 ; let new_tv = setTyVarKind tv' default_k
1283 ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
1284 ; unifyTyVar the_tv (mkTyVarTy new_tv)
1285 ; return new_tv }
1286 -- Why not directly derived_pred = mkTcEqPred k default_k?
1287 -- See Note [DefaultTyVar]
1288 -- We keep the same TcLevel on tv'
1289
1290 | otherwise = return the_tv -- The common case
1291
1292 approximateWC :: WantedConstraints -> Cts
1293 -- Postcondition: Wanted or Derived Cts
1294 -- See Note [ApproximateWC]
1295 approximateWC wc
1296 = float_wc emptyVarSet wc
1297 where
1298 float_wc :: TcTyVarSet -> WantedConstraints -> Cts
1299 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1300 = filterBag is_floatable simples `unionBags`
1301 do_bag (float_implic new_trapping_tvs) implics
1302 where
1303 is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs
1304 new_trapping_tvs = transCloVarSet grow trapping_tvs
1305
1306 grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
1307 grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
1308 grow_one so_far ct tvs
1309 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
1310 | otherwise = tvs
1311 where
1312 ct_tvs = tyVarsOfCt ct
1313
1314 float_implic :: TcTyVarSet -> Implication -> Cts
1315 float_implic trapping_tvs imp
1316 | ic_no_eqs imp -- No equalities, so float
1317 = float_wc new_trapping_tvs (ic_wanted imp)
1318 | otherwise -- Don't float out of equalities
1319 = emptyCts -- See Note [ApproximateWC]
1320 where
1321 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1322 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1323 do_bag f = foldrBag (unionBags.f) emptyBag
1324
1325 {-
1326 Note [ApproximateWC]
1327 ~~~~~~~~~~~~~~~~~~~~
1328 approximateWC takes a constraint, typically arising from the RHS of a
1329 let-binding whose type we are *inferring*, and extracts from it some
1330 *simple* constraints that we might plausibly abstract over. Of course
1331 the top-level simple constraints are plausible, but we also float constraints
1332 out from inside, if they are not captured by skolems.
1333
1334 The same function is used when doing type-class defaulting (see the call
1335 to applyDefaultingRules) to extract constraints that that might be defaulted.
1336
1337 There are two caveats:
1338
1339 1. We do *not* float anything out if the implication binds equality
1340 constraints, because that defeats the OutsideIn story. Consider
1341 data T a where
1342 TInt :: T Int
1343 MkT :: T a
1344
1345 f TInt = 3::Int
1346
1347 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1348 f :: T a -> res
1349 We don't want to float (res~Int) out because then we'll infer
1350 f :: T a -> Int
1351 which is only on of the possible types. (GHC 7.6 accidentally *did*
1352 float out of such implications, which meant it would happily infer
1353 non-principal types.)
1354
1355 2. We do not float out an inner constraint that shares a type variable
1356 (transitively) with one that is trapped by a skolem. Eg
1357 forall a. F a ~ beta, Integral beta
1358 We don't want to float out (Integral beta). Doing so would be bad
1359 when defaulting, because then we'll default beta:=Integer, and that
1360 makes the error message much worse; we'd get
1361 Can't solve F a ~ Integer
1362 rather than
1363 Can't solve Integral (F a)
1364
1365 Moreover, floating out these "contaminated" constraints doesn't help
1366 when generalising either. If we generalise over (Integral b), we still
1367 can't solve the retained implication (forall a. F a ~ b). Indeed,
1368 arguably that too would be a harder error to understand.
1369
1370 Note [DefaultTyVar]
1371 ~~~~~~~~~~~~~~~~~~~
1372 defaultTyVar is used on any un-instantiated meta type variables to
1373 default the kind of OpenKind and ArgKind etc to *. This is important
1374 to ensure that instance declarations match. For example consider
1375
1376 instance Show (a->b)
1377 foo x = show (\_ -> True)
1378
1379 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1380 and that won't match the typeKind (*) in the instance decl. See tests
1381 tc217 and tc175.
1382
1383 We look only at touchable type variables. No further constraints
1384 are going to affect these type variables, so it's time to do it by
1385 hand. However we aren't ready to default them fully to () or
1386 whatever, because the type-class defaulting rules have yet to run.
1387
1388 An important point is that if the type variable tv has kind k and the
1389 default is default_k we do not simply generate [D] (k ~ default_k) because:
1390
1391 (1) k may be ArgKind and default_k may be * so we will fail
1392
1393 (2) We need to rewrite all occurrences of the tv to be a type
1394 variable with the right kind and we choose to do this by rewriting
1395 the type variable /itself/ by a new variable which does have the
1396 right kind.
1397
1398 Note [Promote _and_ default when inferring]
1399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1400 When we are inferring a type, we simplify the constraint, and then use
1401 approximateWC to produce a list of candidate constraints. Then we MUST
1402
1403 a) Promote any meta-tyvars that have been floated out by
1404 approximateWC, to restore invariant (MetaTvInv) described in
1405 Note [TcLevel and untouchable type variables] in TcType.
1406
1407 b) Default the kind of any meta-tyyvars that are not mentioned in
1408 in the environment.
1409
1410 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1411 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1412 should! If we don't solve the constraint, we'll stupidly quantify over
1413 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1414 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1415 Trac #7641 is a simpler example.
1416
1417 Note [Promoting unification variables]
1418 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1419 When we float an equality out of an implication we must "promote" free
1420 unification variables of the equality, in order to maintain Invariant
1421 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1422 leftover implication.
1423
1424 This is absolutely necessary. Consider the following example. We start
1425 with two implications and a class with a functional dependency.
1426
1427 class C x y | x -> y
1428 instance C [a] [a]
1429
1430 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1431 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1432
1433 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1434 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1435 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1436 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1437 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1438
1439 class C x y | x -> y where
1440 op :: x -> y -> ()
1441
1442 instance C [a] [a]
1443
1444 type family F a :: *
1445
1446 h :: F Int -> ()
1447 h = undefined
1448
1449 data TEx where
1450 TEx :: a -> TEx
1451
1452 f (x::beta) =
1453 let g1 :: forall b. b -> ()
1454 g1 _ = h [x]
1455 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1456 in (g1 '3', g2 undefined)
1457
1458
1459 Note [Solving Family Equations]
1460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1461 After we are done with simplification we may be left with constraints of the form:
1462 [Wanted] F xis ~ beta
1463 If 'beta' is a touchable unification variable not already bound in the TyBinds
1464 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1465
1466 When is it ok to do so?
1467 1) 'beta' must not already be defaulted to something. Example:
1468
1469 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1470 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1471 have to report this as unsolved.
1472
1473 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1474 set [beta := F xis] only if beta is not among the free variables of xis.
1475
1476 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1477 of type family equations. See Inert Set invariants in TcInteract.
1478
1479 This solving is now happening during zonking, see Note [Unflattening while zonking]
1480 in TcMType.
1481
1482
1483 *********************************************************************************
1484 * *
1485 * Floating equalities *
1486 * *
1487 *********************************************************************************
1488
1489 Note [Float Equalities out of Implications]
1490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1491 For ordinary pattern matches (including existentials) we float
1492 equalities out of implications, for instance:
1493 data T where
1494 MkT :: Eq a => a -> T
1495 f x y = case x of MkT _ -> (y::Int)
1496 We get the implication constraint (x::T) (y::alpha):
1497 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1498 We want to float out the equality into a scope where alpha is no
1499 longer untouchable, to solve the implication!
1500
1501 But we cannot float equalities out of implications whose givens may
1502 yield or contain equalities:
1503
1504 data T a where
1505 T1 :: T Int
1506 T2 :: T Bool
1507 T3 :: T a
1508
1509 h :: T a -> a -> Int
1510
1511 f x y = case x of
1512 T1 -> y::Int
1513 T2 -> y::Bool
1514 T3 -> h x y
1515
1516 We generate constraint, for (x::T alpha) and (y :: beta):
1517 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1518 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1519 (alpha ~ beta) -- From 3rd branch
1520
1521 If we float the equality (beta ~ Int) outside of the first implication and
1522 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1523 But if we just leave them inside the implications we unify alpha := beta and
1524 solve everything.
1525
1526 Principle:
1527 We do not want to float equalities out which may
1528 need the given *evidence* to become soluble.
1529
1530 Consequence: classes with functional dependencies don't matter (since there is
1531 no evidence for a fundep equality), but equality superclasses do matter (since
1532 they carry evidence).
1533 -}
1534
1535 floatEqualities :: [TcTyVar] -> Bool
1536 -> WantedConstraints
1537 -> TcS (Cts, WantedConstraints)
1538 -- Main idea: see Note [Float Equalities out of Implications]
1539 --
1540 -- Precondition: the wc_simple of the incoming WantedConstraints are
1541 -- fully zonked, so that we can see their free variables
1542 --
1543 -- Postcondition: The returned floated constraints (Cts) are only
1544 -- Wanted or Derived and come from the input wanted
1545 -- ev vars or deriveds
1546 --
1547 -- Also performs some unifications (via promoteTyVar), adding to
1548 -- monadically-carried ty_binds. These will be used when processing
1549 -- floated_eqs later
1550 --
1551 -- Subtleties: Note [Float equalities from under a skolem binding]
1552 -- Note [Skolem escape]
1553 floatEqualities skols no_given_eqs wanteds@(WC { wc_simple = simples })
1554 | not no_given_eqs -- There are some given equalities, so don't float
1555 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1556 | otherwise
1557 = do { outer_tclvl <- TcS.getTcLevel
1558 ; mapM_ (promoteTyVar outer_tclvl) (varSetElems (tyVarsOfCts float_eqs))
1559 -- See Note [Promoting unification variables]
1560 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1561 , text "Simples =" <+> ppr simples
1562 , text "Floated eqs =" <+> ppr float_eqs ])
1563 ; return (float_eqs, wanteds { wc_simple = remaining_simples }) }
1564 where
1565 skol_set = mkVarSet skols
1566 (float_eqs, remaining_simples) = partitionBag (usefulToFloat is_useful) simples
1567 is_useful pred = tyVarsOfType pred `disjointVarSet` skol_set
1568
1569 {- Note [Float equalities from under a skolem binding]
1570 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1571 Which of the simple equalities can we float out? Obviously, only
1572 ones that don't mention the skolem-bound variables. But that is
1573 over-eager. Consider
1574 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1575 The second constraint doesn't mention 'a'. But if we float it
1576 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1577 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1578 we left with the constraint
1579 [2] forall a. a ~ gamma'[1]
1580 which is insoluble because gamma became untouchable.
1581
1582 Solution: float only constraints that stand a jolly good chance of
1583 being soluble simply by being floated, namely ones of form
1584 a ~ ty
1585 where 'a' is a currently-untouchable unification variable, but may
1586 become touchable by being floated (perhaps by more than one level).
1587
1588 We had a very complicated rule previously, but this is nice and
1589 simple. (To see the notes, look at this Note in a version of
1590 TcSimplify prior to Oct 2014).
1591
1592 Note [Skolem escape]
1593 ~~~~~~~~~~~~~~~~~~~~
1594 You might worry about skolem escape with all this floating.
1595 For example, consider
1596 [2] forall a. (a ~ F beta[2] delta,
1597 Maybe beta[2] ~ gamma[1])
1598
1599 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1600 solve with gamma := beta. But what if later delta:=Int, and
1601 F b Int = b.
1602 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1603 skolem has escaped!
1604
1605 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1606 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1607
1608
1609 *********************************************************************************
1610 * *
1611 * Defaulting and disamgiguation *
1612 * *
1613 *********************************************************************************
1614 -}
1615
1616 applyDefaultingRules :: WantedConstraints -> TcS Bool
1617 -- True <=> I did some defaulting, by unifying a meta-tyvar
1618 -- Imput WantedConstraints are not necessarily zonked
1619
1620 applyDefaultingRules wanteds
1621 | isEmptyWC wanteds
1622 = return False
1623 | otherwise
1624 = do { info@(default_tys, _) <- getDefaultInfo
1625 ; wanteds <- TcS.zonkWC wanteds
1626
1627 ; let groups = findDefaultableGroups info wanteds
1628
1629 ; traceTcS "applyDefaultingRules {" $
1630 vcat [ text "wanteds =" <+> ppr wanteds
1631 , text "groups =" <+> ppr groups
1632 , text "info =" <+> ppr info ]
1633
1634 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1635
1636 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1637
1638 ; return (or something_happeneds) }
1639
1640 findDefaultableGroups
1641 :: ( [Type]
1642 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1643 -> WantedConstraints -- Unsolved (wanted or derived)
1644 -> [(TyVar, [Ct])]
1645 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1646 | null default_tys
1647 = []
1648 | otherwise
1649 = [ (tv, map fstOf3 group)
1650 | group@((_,_,tv):_) <- unary_groups
1651 , defaultable_tyvar tv
1652 , defaultable_classes (map sndOf3 group) ]
1653 where
1654 simples = approximateWC wanteds
1655 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
1656 unary_groups = equivClasses cmp_tv unaries
1657
1658 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
1659 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
1660 non_unaries :: [Ct] -- and *other* constraints
1661
1662 -- Finds unary type-class constraints
1663 -- But take account of polykinded classes like Typeable,
1664 -- which may look like (Typeable * (a:*)) (Trac #8931)
1665 find_unary cc
1666 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
1667 , Just (kinds, ty) <- snocView tys -- Ignore kind arguments
1668 , all isKind kinds -- for this purpose
1669 , Just tv <- tcGetTyVar_maybe ty
1670 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
1671 -- we definitely don't want to try to assign to those!
1672 = Left (cc, cls, tv)
1673 find_unary cc = Right cc -- Non unary or non dictionary
1674
1675 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1676 bad_tvs = mapUnionVarSet tyVarsOfCt non_unaries
1677
1678 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1679
1680 defaultable_tyvar tv
1681 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1682 b2 = not (tv `elemVarSet` bad_tvs)
1683 in b1 && b2
1684
1685 defaultable_classes clss
1686 | extended_defaults = any isInteractiveClass clss
1687 | otherwise = all is_std_class clss && (any is_num_class clss)
1688
1689 -- In interactive mode, or with -XExtendedDefaultRules,
1690 -- we default Show a to Show () to avoid graututious errors on "show []"
1691 isInteractiveClass cls
1692 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1693
1694 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1695 -- is_num_class adds IsString to the standard numeric classes,
1696 -- when -foverloaded-strings is enabled
1697
1698 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1699 -- Similarly is_std_class
1700
1701 ------------------------------
1702 disambigGroup :: [Type] -- The default types
1703 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
1704 -- sharing same type variable
1705 -> TcS Bool -- True <=> something happened, reflected in ty_binds
1706
1707 disambigGroup [] _
1708 = return False
1709 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
1710 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
1711 ; fake_ev_binds_var <- TcS.newTcEvBinds
1712 ; tclvl <- TcS.getTcLevel
1713 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl)
1714 try_group
1715
1716 ; if success then
1717 -- Success: record the type variable binding, and return
1718 do { unifyTyVar the_tv default_ty
1719 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
1720 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
1721 ; return True }
1722 else
1723 -- Failure: try with the next type
1724 do { traceTcS "disambigGroup failed, will try other default types }"
1725 (ppr default_ty)
1726 ; disambigGroup default_tys group } }
1727 where
1728 try_group
1729 | Just subst <- mb_subst
1730 = do { wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
1731 wanteds
1732 ; residual_wanted <- solveSimpleWanteds $ listToBag $
1733 map mkNonCanonical wanted_evs
1734 ; return (isEmptyWC residual_wanted) }
1735 | otherwise
1736 = return False
1737
1738 tmpl_tvs = extendVarSet (tyVarsOfType (tyVarKind the_tv)) the_tv
1739 mb_subst = tcMatchTy tmpl_tvs (mkTyVarTy the_tv) default_ty
1740 -- Make sure the kinds match too; hence this call to tcMatchTy
1741 -- E.g. suppose the only constraint was (Typeable k (a::k))
1742
1743 loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
1744 , ctl_env = panic "disambigGroup:env"
1745 , ctl_depth = initialSubGoalDepth }
1746
1747 {-
1748 Note [Avoiding spurious errors]
1749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1750 When doing the unification for defaulting, we check for skolem
1751 type variables, and simply don't default them. For example:
1752 f = (*) -- Monomorphic
1753 g :: Num a => a -> a
1754 g x = f x x
1755 Here, we get a complaint when checking the type signature for g,
1756 that g isn't polymorphic enough; but then we get another one when
1757 dealing with the (Num a) context arising from f's definition;
1758 we try to unify a with Int (to default it), but find that it's
1759 already been unified with the rigid variable from g's type sig
1760 -}