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