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