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