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