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