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