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