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