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