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