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