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