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