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