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