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