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