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