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