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