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