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