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