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