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