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