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