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