Refactor computing dependent type vars
[ghc.git] / compiler / typecheck / TcSimplify.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcSimplify(
4 simplifyInfer,
5 growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, simplifyInteractive, solveEqualities,
9 simplifyWantedsTcM,
10 tcCheckSatisfiability,
11
12 -- For Rules we need these
13 solveWanteds, runTcSDeriveds
14 ) where
15
16 #include "HsVersions.h"
17
18 import Bag
19 import Class ( Class, classKey, classTyCon )
20 import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
21 , WarnReason ( Reason )
22 , DynFlags( solverIterations ) )
23 import Inst
24 import ListSetOps
25 import Maybes
26 import Name
27 import Outputable
28 import PrelInfo
29 import PrelNames
30 import TcErrors
31 import TcEvidence
32 import TcInteract
33 import TcCanonical ( makeSuperClasses, mkGivensWithSuperClasses )
34 import TcMType as TcM
35 import TcRnMonad as TcM
36 import TcSMonad as TcS
37 import TcType
38 import TrieMap () -- DV: for now
39 import Type
40 import TysWiredIn ( ptrRepLiftedTy )
41 import Unify ( tcMatchTy )
42 import Util
43 import Var
44 import VarSet
45 import BasicTypes ( IntWithInf, intGtLimit )
46 import ErrUtils ( emptyMessages )
47 import qualified GHC.LanguageExtensions as LangExt
48
49 import Control.Monad ( when, unless )
50 import Data.List ( partition )
51
52 {-
53 *********************************************************************************
54 * *
55 * External interface *
56 * *
57 *********************************************************************************
58 -}
59
60 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
61 -- Simplify top-level constraints
62 -- Usually these will be implications,
63 -- but when there is nothing to quantify we don't wrap
64 -- in a degenerate implication, so we do that here instead
65 simplifyTop wanteds
66 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
67 ; ((final_wc, unsafe_ol), binds1) <- runTcS $
68 do { final_wc <- simpl_top wanteds
69 ; unsafe_ol <- getSafeOverlapFailures
70 ; return (final_wc, unsafe_ol) }
71 ; traceTc "End simplifyTop }" empty
72
73 ; traceTc "reportUnsolved {" empty
74 ; binds2 <- reportUnsolved final_wc
75 ; traceTc "reportUnsolved }" empty
76
77 ; traceTc "reportUnsolved (unsafe overlapping) {" empty
78 ; unless (isEmptyCts unsafe_ol) $ do {
79 -- grab current error messages and clear, warnAllUnsolved will
80 -- update error messages which we'll grab and then restore saved
81 -- messages.
82 ; errs_var <- getErrsVar
83 ; saved_msg <- TcM.readTcRef errs_var
84 ; TcM.writeTcRef errs_var emptyMessages
85
86 ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
87 , wc_insol = emptyCts
88 , wc_impl = emptyBag }
89
90 ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
91 ; TcM.writeTcRef errs_var saved_msg
92 ; recordUnsafeInfer whyUnsafe
93 }
94 ; traceTc "reportUnsolved (unsafe overlapping) }" empty
95
96 ; return (evBindMapBinds binds1 `unionBags` binds2) }
97
98 -- | Type-check a thing that emits only equality constraints, then
99 -- solve those constraints. Fails outright if there is trouble.
100 solveEqualities :: TcM a -> TcM a
101 solveEqualities thing_inside
102 = checkNoErrs $ -- See Note [Fail fast on kind errors]
103 do { (result, wanted) <- captureConstraints thing_inside
104 ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
105 ; final_wc <- runTcSEqualities $ simpl_top wanted
106 ; traceTc "End solveEqualities }" empty
107
108 ; traceTc "reportAllUnsolved {" empty
109 ; reportAllUnsolved final_wc
110 ; traceTc "reportAllUnsolved }" empty
111 ; return result }
112
113 simpl_top :: WantedConstraints -> TcS WantedConstraints
114 -- See Note [Top-level Defaulting Plan]
115 simpl_top wanteds
116 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
117 -- This is where the main work happens
118 ; try_tyvar_defaulting wc_first_go }
119 where
120 try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
121 try_tyvar_defaulting wc
122 | isEmptyWC wc
123 = return wc
124 | otherwise
125 = do { free_tvs <- TcS.zonkTyCoVarsAndFV (tyCoVarsOfWC wc)
126 ; let meta_tvs = varSetElems $
127 filterVarSet (isTyVar <&&> isMetaTyVar) free_tvs
128 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
129 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
130 -- and we definitely don't want to try to assign to those!
131 -- the isTyVar needs to weed out coercion variables
132
133 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
134 ; if or defaulted
135 then do { wc_residual <- nestTcS (solveWanteds wc)
136 -- See Note [Must simplify after defaulting]
137 ; try_class_defaulting wc_residual }
138 else try_class_defaulting wc } -- No defaulting took place
139
140 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
141 try_class_defaulting wc
142 | isEmptyWC wc
143 = return wc
144 | otherwise -- See Note [When to do type-class defaulting]
145 = do { something_happened <- applyDefaultingRules wc
146 -- See Note [Top-level Defaulting Plan]
147 ; if something_happened
148 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
149 ; try_class_defaulting wc_residual }
150 -- See Note [Overview of implicit CallStacks] in TcEvidence
151 else try_callstack_defaulting wc }
152
153 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
154 try_callstack_defaulting wc
155 | isEmptyWC wc
156 = return wc
157 | otherwise
158 = defaultCallStacks wc
159
160 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
161 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
162 -- See Note [Overview of implicit CallStacks] in TcEvidence
163 defaultCallStacks wanteds
164 = do simples <- handle_simples (wc_simple wanteds)
165 implics <- mapBagM handle_implic (wc_impl wanteds)
166 return (wanteds { wc_simple = simples, wc_impl = implics })
167
168 where
169
170 handle_simples simples
171 = catBagMaybes <$> mapBagM defaultCallStack simples
172
173 handle_implic implic = do
174 wanteds <- defaultCallStacks (ic_wanted implic)
175 return (implic { ic_wanted = wanteds })
176
177 defaultCallStack ct
178 | Just _ <- isCallStackPred (ctPred ct)
179 = do { solveCallStack (cc_ev ct) EvCsEmpty
180 ; return Nothing }
181
182 defaultCallStack ct
183 = return (Just ct)
184
185
186 {- Note [Fail fast on kind errors]
187 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
188 solveEqualities is used to solve kind equalities when kind-checking
189 user-written types. If solving fails we should fail outright, rather
190 than just accumulate an error message, for two reasons:
191
192 * A kind-bogus type signature may cause a cascade of knock-on
193 errors if we let it pass
194
195 * More seriously, we don't have a convenient term-level place to add
196 deferred bindings for unsolved kind-equality constraints, so we
197 don't build evidence bindings (by usine reportAllUnsolved). That
198 means that we'll be left with with a type that has coercion holes
199 in it, something like
200 <type> |> co-hole
201 where co-hole is not filled in. Eeek! That un-filled-in
202 hole actually causes GHC to crash with "fvProv falls into a hole"
203 See Trac #11563, #11520, #11516, #11399
204
205 So it's important to use 'checkNoErrs' here!
206
207 Note [When to do type-class defaulting]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
210 was false, on the grounds that defaulting can't help solve insoluble
211 constraints. But if we *don't* do defaulting we may report a whole
212 lot of errors that would be solved by defaulting; these errors are
213 quite spurious because fixing the single insoluble error means that
214 defaulting happens again, which makes all the other errors go away.
215 This is jolly confusing: Trac #9033.
216
217 So it seems better to always do type-class defaulting.
218
219 However, always doing defaulting does mean that we'll do it in
220 situations like this (Trac #5934):
221 run :: (forall s. GenST s) -> Int
222 run = fromInteger 0
223 We don't unify the return type of fromInteger with the given function
224 type, because the latter involves foralls. So we're left with
225 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
226 Now we do defaulting, get alpha := Integer, and report that we can't
227 match Integer with (forall s. GenST s) -> Int. That's not totally
228 stupid, but perhaps a little strange.
229
230 Another potential alternative would be to suppress *all* non-insoluble
231 errors if there are *any* insoluble errors, anywhere, but that seems
232 too drastic.
233
234 Note [Must simplify after defaulting]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 We may have a deeply buried constraint
237 (t:*) ~ (a:Open)
238 which we couldn't solve because of the kind incompatibility, and 'a' is free.
239 Then when we default 'a' we can solve the constraint. And we want to do
240 that before starting in on type classes. We MUST do it before reporting
241 errors, because it isn't an error! Trac #7967 was due to this.
242
243 Note [Top-level Defaulting Plan]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 We have considered two design choices for where/when to apply defaulting.
246 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
247 simple constraints, maybe deep inside the context of implications.
248 This used to be the case in GHC 7.4.1.
249 (ii) Do it in a tight loop at simplifyTop, once all other constraints have
250 finished. This is the current story.
251
252 Option (i) had many disadvantages:
253 a) Firstly, it was deep inside the actual solver.
254 b) Secondly, it was dependent on the context (Infer a type signature,
255 or Check a type signature, or Interactive) since we did not want
256 to always start defaulting when inferring (though there is an exception to
257 this, see Note [Default while Inferring]).
258 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
259 f :: Int -> Bool
260 f x = const True (\y -> let w :: a -> a
261 w a = const a (y+1)
262 in w y)
263 We will get an implication constraint (for beta the type of y):
264 [untch=beta] forall a. 0 => Num beta
265 which we really cannot default /while solving/ the implication, since beta is
266 untouchable.
267
268 Instead our new defaulting story is to pull defaulting out of the solver loop and
269 go with option (ii), implemented at SimplifyTop. Namely:
270 - First, have a go at solving the residual constraint of the whole
271 program
272 - Try to approximate it with a simple constraint
273 - Figure out derived defaulting equations for that simple constraint
274 - Go round the loop again if you did manage to get some equations
275
276 Now, that has to do with class defaulting. However there exists type variable /kind/
277 defaulting. Again this is done at the top-level and the plan is:
278 - At the top-level, once you had a go at solving the constraint, do
279 figure out /all/ the touchable unification variables of the wanted constraints.
280 - Apply defaulting to their kinds
281
282 More details in Note [DefaultTyVar].
283
284 Note [Safe Haskell Overlapping Instances]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 In Safe Haskell, we apply an extra restriction to overlapping instances. The
287 motive is to prevent untrusted code provided by a third-party, changing the
288 behavior of trusted code through type-classes. This is due to the global and
289 implicit nature of type-classes that can hide the source of the dictionary.
290
291 Another way to state this is: if a module M compiles without importing another
292 module N, changing M to import N shouldn't change the behavior of M.
293
294 Overlapping instances with type-classes can violate this principle. However,
295 overlapping instances aren't always unsafe. They are just unsafe when the most
296 selected dictionary comes from untrusted code (code compiled with -XSafe) and
297 overlaps instances provided by other modules.
298
299 In particular, in Safe Haskell at a call site with overlapping instances, we
300 apply the following rule to determine if it is a 'unsafe' overlap:
301
302 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
303 2) I1 is an orphan instance or a MPTC.
304 3) At least one overlapped instance, Ix, is both:
305 A) from a different module than I1
306 B) Ix is not marked `OVERLAPPABLE`
307
308 This is a slightly involved heuristic, but captures the situation of an
309 imported module N changing the behavior of existing code. For example, if
310 condition (2) isn't violated, then the module author M must depend either on a
311 type-class or type defined in N.
312
313 Secondly, when should these heuristics be enforced? We enforced them when the
314 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
315 This allows `-XUnsafe` modules to operate without restriction, and for Safe
316 Haskell inferrence to infer modules with unsafe overlaps as unsafe.
317
318 One alternative design would be to also consider if an instance was imported as
319 a `safe` import or not and only apply the restriction to instances imported
320 safely. However, since instances are global and can be imported through more
321 than one path, this alternative doesn't work.
322
323 Note [Safe Haskell Overlapping Instances Implementation]
324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
325
326 How is this implemented? It's complicated! So we'll step through it all:
327
328 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
329 we check if a particular type-class method call is safe or unsafe. We do this
330 through the return type, `ClsInstLookupResult`, where the last parameter is a
331 list of instances that are unsafe to overlap. When the method call is safe,
332 the list is null.
333
334 2) `TcInteract.matchClassInst` -- This module drives the instance resolution
335 / dictionary generation. The return type is `LookupInstResult`, which either
336 says no instance matched, or one found, and if it was a safe or unsafe
337 overlap.
338
339 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
340 tries to resolve it by calling (in part) `matchClassInst`. The resolving
341 mechanism has a work list (of constraints) that it process one at a time. If
342 the constraint can't be resolved, it's added to an inert set. When compiling
343 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
344 compilation should fail. These are handled as normal constraint resolution
345 failures from here-on (see step 6).
346
347 Otherwise, we may be inferring safety (or using `-Wunsafe`), and
348 compilation should succeed, but print warnings and/or mark the compiled module
349 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
350 the unsafe (but resolved!) constraint to the `inert_safehask` field of
351 `InertCans`.
352
353 4) `TcSimplify.simplifyTop`:
354 * Call simpl_top, the top-level function for driving the simplifier for
355 constraint resolution.
356
357 * Once finished, call `getSafeOverlapFailures` to retrieve the
358 list of overlapping instances that were successfully resolved,
359 but unsafe. Remember, this is only applicable for generating warnings
360 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
361 cause compilation failure by not resolving the unsafe constraint at all.
362
363 * For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
364 while for resolved but unsafe overlapping dictionary constraints, call
365 `TcErrors.warnAllUnsolved`. Both functions convert constraints into a
366 warning message for the user.
367
368 * In the case of `warnAllUnsolved` for resolved, but unsafe
369 dictionary constraints, we collect the generated warning
370 message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
371 mark the module we are compiling as unsafe, passing the
372 warning message along as the reason.
373
374 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by
375 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
376 know is the constraint that is unresolved or unsafe. For dictionary, all we
377 know is that we need a dictionary of type C, but not what instances are
378 available and how they overlap. So we once again call `lookupInstEnv` to
379 figure that out so we can generate a helpful error message.
380
381 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an
382 IORef called `tcg_safeInfer`.
383
384 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
385 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
386 failed.
387 -}
388
389 ------------------
390 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
391 simplifyAmbiguityCheck ty wanteds
392 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
393 ; (final_wc, _) <- runTcS $ simpl_top wanteds
394 ; traceTc "End simplifyAmbiguityCheck }" empty
395
396 -- Normally report all errors; but with -XAllowAmbiguousTypes
397 -- report only insoluble ones, since they represent genuinely
398 -- inaccessible code
399 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
400 ; traceTc "reportUnsolved(ambig) {" empty
401 ; tc_lvl <- TcM.getTcLevel
402 ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc))
403 (discardResult (reportUnsolved final_wc))
404 ; traceTc "reportUnsolved(ambig) }" empty
405
406 ; return () }
407
408 ------------------
409 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
410 simplifyInteractive wanteds
411 = traceTc "simplifyInteractive" empty >>
412 simplifyTop wanteds
413
414 ------------------
415 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
416 -> TcM () -- Succeeds if the constraint is soluble
417 simplifyDefault theta
418 = do { traceTc "simplifyInteractive" empty
419 ; loc <- getCtLocM DefaultOrigin Nothing
420 ; let wanted = [ CtDerived { ctev_pred = pred
421 , ctev_loc = loc }
422 | pred <- theta ]
423 ; unsolved <- runTcSDeriveds (solveWanteds (mkSimpleWC wanted))
424 ; traceTc "reportUnsolved {" empty
425 ; reportAllUnsolved unsolved
426 ; traceTc "reportUnsolved }" empty
427 ; return () }
428
429 ------------------
430 tcCheckSatisfiability :: Bag EvVar -> TcM Bool
431 -- Return True if satisfiable, False if definitely contradictory
432 tcCheckSatisfiability given_ids
433 = do { lcl_env <- TcM.getLclEnv
434 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
435 ; (res, _ev_binds) <- runTcS $
436 do { traceTcS "checkSatisfiability {" (ppr given_ids)
437 ; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
438 -- See Note [Superclases and satisfiability]
439 ; insols <- solveSimpleGivens given_cts
440 ; insols <- try_harder insols
441 ; traceTcS "checkSatisfiability }" (ppr insols)
442 ; return (isEmptyBag insols) }
443 ; return res }
444 where
445 try_harder :: Cts -> TcS Cts
446 -- Maybe we have to search up the superclass chain to find
447 -- an unsatisfiable constraint. Example: pmcheck/T3927b.
448 -- At the moment we try just once
449 try_harder insols
450 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
451 = return insols -- Hurrah -- stop now.
452 | otherwise
453 = do { pending_given <- getPendingScDicts
454 ; new_given <- makeSuperClasses pending_given
455 ; solveSimpleGivens new_given }
456
457 {- Note [Superclases and satisfiability]
458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
459 Expand superclasses before starting, because (Int ~ Bool), has
460 (Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
461 as a superclass, and it's the latter that is insoluble. See
462 Note [The equality types story] in TysPrim.
463
464 If we fail to prove unsatisfiability we (arbitrarily) try just once to
465 find superclasses, using try_harder. Reason: we might have a type
466 signature
467 f :: F op (Implements push) => ..
468 where F is a type function. This happened in Trac #3972.
469
470 We could do more than once but we'd have to have /some/ limit: in the
471 the recurisve case, we would go on forever in the common case where
472 the constraints /are/ satisfiable (Trac #10592 comment:12!).
473
474 For stratightforard situations without type functions the try_harder
475 step does nothing.
476
477
478 ***********************************************************************************
479 * *
480 * Inference
481 * *
482 ***********************************************************************************
483
484 Note [Inferring the type of a let-bound variable]
485 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
486 Consider
487 f x = rhs
488
489 To infer f's type we do the following:
490 * Gather the constraints for the RHS with ambient level *one more than*
491 the current one. This is done by the call
492 pushLevelAndCaptureConstraints (tcMonoBinds...)
493 in TcBinds.tcPolyInfer
494
495 * Call simplifyInfer to simplify the constraints and decide what to
496 quantify over. We pass in the level used for the RHS constraints,
497 here called rhs_tclvl.
498
499 This ensures that the implication constraint we generate, if any,
500 has a strictly-increased level compared to the ambient level outside
501 the let binding.
502
503 -}
504
505 simplifyInfer :: TcLevel -- Used when generating the constraints
506 -> Bool -- Apply monomorphism restriction
507 -> [TcIdSigInfo] -- Any signatures (possibly partial)
508 -> [(Name, TcTauType)] -- Variables to be generalised,
509 -- and their tau-types
510 -> WantedConstraints
511 -> TcM ([TcTyVar], -- Quantify over these type variables
512 [EvVar], -- ... and these constraints (fully zonked)
513 TcEvBinds) -- ... binding these evidence variables
514 simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
515 | isEmptyWC wanteds
516 = do { gbl_tvs <- tcGetGlobalTyCoVars
517 ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
518 ; qtkvs <- quantify_tvs sigs gbl_tvs dep_vars
519 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
520 ; return (qtkvs, [], emptyTcEvBinds) }
521
522 | otherwise
523 = do { traceTc "simplifyInfer {" $ vcat
524 [ text "sigs =" <+> ppr sigs
525 , text "binds =" <+> ppr name_taus
526 , text "rhs_tclvl =" <+> ppr rhs_tclvl
527 , text "apply_mr =" <+> ppr apply_mr
528 , text "(unzonked) wanted =" <+> ppr wanteds
529 ]
530
531 -- First do full-blown solving
532 -- NB: we must gather up all the bindings from doing
533 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
534 -- And note that since there are nested implications,
535 -- calling solveWanteds will side-effect their evidence
536 -- bindings, so we can't just revert to the input
537 -- constraint.
538
539 ; ev_binds_var <- TcM.newTcEvBinds
540 ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $
541 do { sig_derived <- concatMapM mkSigDerivedWanteds sigs
542 -- the False says we don't really need to solve all Deriveds
543 ; runTcSWithEvBinds False (Just ev_binds_var) $
544 solveWanteds (wanteds `addSimples` listToBag sig_derived) }
545 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
546
547 -- Find quant_pred_candidates, the predicates that
548 -- we'll consider quantifying over
549 -- NB: We do not do any defaulting when inferring a type, this can lead
550 -- to less polymorphic types, see Note [Default while Inferring]
551
552 ; tc_lcl_env <- TcM.getLclEnv
553 ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
554 ; quant_pred_candidates -- Fully zonked
555 <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs
556 then return [] -- See Note [Quantification with errors]
557 -- NB: must include derived errors in this test,
558 -- hence "incl_derivs"
559
560 else do { let quant_cand = approximateWC wanted_transformed
561 meta_tvs = filter isMetaTyVar $
562 tyCoVarsOfCtsList quant_cand
563
564 ; gbl_tvs <- tcGetGlobalTyCoVars
565 -- Miminise quant_cand. We are not interested in any evidence
566 -- produced, because we are going to simplify wanted_transformed
567 -- again later. All we want here are the predicates over which to
568 -- quantify.
569 --
570 -- If any meta-tyvar unifications take place (unlikely),
571 -- we'll pick that up later.
572
573 -- See Note [Promote _and_ default when inferring]
574 ; let def_tyvar tv
575 = when (not $ tv `elemVarSet` gbl_tvs) $
576 defaultTyVar tv
577 ; mapM_ def_tyvar meta_tvs
578 ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
579
580 ; WC { wc_simple = simples }
581 <- setTcLevel rhs_tclvl $
582 runTcSDeriveds $
583 solveSimpleWanteds $
584 mapBag toDerivedCt quant_cand
585 -- NB: we don't want evidence,
586 -- so use Derived constraints
587
588 ; simples <- TcM.zonkSimples simples
589
590 ; return [ ctEvPred ev | ct <- bagToList simples
591 , let ev = ctEvidence ct ] }
592
593 -- NB: quant_pred_candidates is already fully zonked
594
595 -- Decide what type variables and constraints to quantify
596 ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
597 ; let zonked_tau_tkvs = splitDepVarsOfTypes zonked_taus
598 ; (qtvs, bound_theta)
599 <- decideQuantification apply_mr sigs name_taus
600 quant_pred_candidates zonked_tau_tkvs
601
602 -- Promote any type variables that are free in the inferred type
603 -- of the function:
604 -- f :: forall qtvs. bound_theta => zonked_tau
605 -- These variables now become free in the envt, and hence will show
606 -- up whenever 'f' is called. They may currently at rhs_tclvl, but
607 -- they had better be unifiable at the outer_tclvl!
608 -- Example: envt mentions alpha[1]
609 -- tau_ty = beta[2] -> beta[2]
610 -- consraints = alpha ~ [beta]
611 -- we don't quantify over beta (since it is fixed by envt)
612 -- so we must promote it! The inferred type is just
613 -- f :: beta -> beta
614 ; zonked_tau_tvs <- TcM.zonkTyCoVarsAndFV (dv_tvs zonked_tau_tkvs)
615 -- decideQuantification turned some meta tyvars into
616 -- quantified skolems, so we have to zonk again
617
618 ; let phi_tvs = tyCoVarsOfTypes bound_theta
619 `unionVarSet` zonked_tau_tvs
620
621 promote_tvs = closeOverKinds phi_tvs `delVarSetList` qtvs
622 ; MASSERT2( closeOverKinds promote_tvs `subVarSet` promote_tvs
623 , ppr phi_tvs $$
624 ppr (closeOverKinds phi_tvs) $$
625 ppr promote_tvs $$
626 ppr (closeOverKinds promote_tvs) )
627 -- we really don't want a type to be promoted when its kind isn't!
628
629 -- promoteTyVar ignores coercion variables
630 ; outer_tclvl <- TcM.getTcLevel
631 ; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tvs)
632
633 -- Emit an implication constraint for the
634 -- remaining constraints from the RHS
635 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
636 ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty)
637 | (name, ty) <- name_taus ]
638 -- Don't add the quantified variables here, because
639 -- they are also bound in ic_skols and we want them
640 -- to be tidied uniformly
641
642 implic = Implic { ic_tclvl = rhs_tclvl
643 , ic_skols = qtvs
644 , ic_no_eqs = False
645 , ic_given = bound_theta_vars
646 , ic_wanted = wanted_transformed
647 , ic_status = IC_Unsolved
648 , ic_binds = Just ev_binds_var
649 , ic_info = skol_info
650 , ic_env = tc_lcl_env }
651 ; emitImplication implic
652
653 -- All done!
654 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
655 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
656 , text "zonked_taus" <+> ppr zonked_taus
657 , text "zonked_tau_tvs=" <+> ppr zonked_tau_tvs
658 , text "promote_tvs=" <+> ppr promote_tvs
659 , text "bound_theta =" <+> ppr bound_theta
660 , text "qtvs =" <+> ppr qtvs
661 , text "implic =" <+> ppr implic ]
662
663 ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var ) }
664
665 mkSigDerivedWanteds :: TcIdSigInfo -> TcM [Ct]
666 -- See Note [Add deriveds for signature contexts]
667 mkSigDerivedWanteds (TISI { sig_bndr = PartialSig { sig_name = name }
668 , sig_theta = theta, sig_tau = tau })
669 = do { let skol_info = InferSkol [(name, mkSigmaTy [] theta tau)]
670 ; loc <- getCtLocM (GivenOrigin skol_info) (Just TypeLevel)
671 ; return [ mkNonCanonical (CtDerived { ctev_pred = pred
672 , ctev_loc = loc })
673 | pred <- theta ] }
674 mkSigDerivedWanteds _ = return []
675
676 {- Note [Add deriveds for signature contexts]
677 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678 Consider this (Trac #11016):
679 f2 :: (?x :: Int) => _
680 f2 = ?x
681 We'll use plan InferGen because there are holes in the type. But we want
682 to have the (?x :: Int) constraint floating around so that the functional
683 dependencies kick in. Otherwise the occurrence of ?x on the RHS produces
684 constraint (?x :: alpha), and we wont unify alpha:=Int.
685
686 Solution: in simplifyInfer, just before simplifying the constraints
687 gathered from the RHS, add Derived constraints for the context of any
688 type signatures. This is rare; if there is a type signature we'll usually
689 be doing CheckGen. But it happens for signatures with holes.
690
691 ************************************************************************
692 * *
693 Quantification
694 * *
695 ************************************************************************
696
697 Note [Deciding quantification]
698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
699 If the monomorphism restriction does not apply, then we quantify as follows:
700 * Take the global tyvars, and "grow" them using the equality constraints
701 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
702 happen because alpha is untouchable here) then do not quantify over
703 beta, because alpha fixes beta, and beta is effectively free in
704 the environment too
705 These are the mono_tvs
706
707 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
708 using all the constraints. These are tau_tvs_plus
709
710 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
711 careful to close over kinds, and to skolemise the quantified tyvars.
712 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
713 Result is qtvs.
714
715 * Filter the constraints using pickQuantifiablePreds and the qtvs.
716 We have to zonk the constraints first, so they "see" the freshly
717 created skolems.
718
719 If the MR does apply, mono_tvs includes all the constrained tyvars --
720 including all covars -- and the quantified constraints are empty/insoluble.
721
722 -}
723
724 decideQuantification
725 :: Bool -- try the MR restriction?
726 -> [TcIdSigInfo]
727 -> [(Name, TcTauType)] -- variables to be generalised (for errors only)
728 -> [PredType] -- candidate theta
729 -> TcDepVars
730 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
731 , [PredType] ) -- and this context (fully zonked)
732 -- See Note [Deciding quantification]
733 decideQuantification apply_mr sigs name_taus constraints
734 zonked_dvs@(DV { dv_kvs = zonked_tau_kvs, dv_tvs = zonked_tau_tvs })
735 | apply_mr -- Apply the Monomorphism restriction
736 = do { gbl_tvs <- tcGetGlobalTyCoVars
737 ; let zonked_tkvs = zonked_tau_kvs `unionVarSet` zonked_tau_tvs
738 constrained_tvs = tyCoVarsOfTypes constraints `unionVarSet`
739 filterVarSet isCoVar zonked_tkvs
740 mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
741 ; qtvs <- quantify_tvs sigs mono_tvs zonked_dvs
742
743 -- Warn about the monomorphism restriction
744 ; warn_mono <- woptM Opt_WarnMonomorphism
745 ; let mr_bites = constrained_tvs `intersectsVarSet` zonked_tkvs
746 ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
747 hang (text "The Monomorphism Restriction applies to the binding"
748 <> plural bndrs <+> text "for" <+> pp_bndrs)
749 2 (text "Consider giving a type signature for"
750 <+> if isSingleton bndrs then pp_bndrs
751 else text "these binders")
752
753 -- All done
754 ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
755 , ppr qtvs, ppr mr_bites])
756 ; return (qtvs, []) }
757
758 | otherwise
759 = do { gbl_tvs <- tcGetGlobalTyCoVars
760 ; let mono_tvs = growThetaTyVars equality_constraints gbl_tvs
761 tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
762 dvs_plus = DV { dv_kvs = zonked_tau_kvs, dv_tvs = tau_tvs_plus }
763 ; qtvs <- quantify_tvs sigs mono_tvs dvs_plus
764 -- We don't grow the kvs, as there's no real need to. Recall
765 -- that quantifyTyVars uses the separation between kvs and tvs
766 -- only for defaulting, and we don't want (ever) to default a tv
767 -- to *. So, don't grow the kvs.
768
769 ; constraints <- TcM.zonkTcTypes constraints
770 -- quantifyTyVars turned some meta tyvars into
771 -- quantified skolems, so we have to zonk again
772
773 ; let theta = pickQuantifiablePreds
774 (mkVarSet qtvs) (concatMap sig_theta sigs) constraints
775 min_theta = mkMinimalBySCs theta
776 -- See Note [Minimize by Superclasses]
777
778 ; traceTc "decideQuantification 2"
779 (vcat [ text "constraints:" <+> ppr constraints
780 , text "gbl_tvs:" <+> ppr gbl_tvs
781 , text "mono_tvs:" <+> ppr mono_tvs
782 , text "zonked_kvs:" <+> ppr zonked_tau_kvs
783 , text "tau_tvs_plus:" <+> ppr tau_tvs_plus
784 , text "qtvs:" <+> ppr qtvs
785 , text "min_theta:" <+> ppr min_theta ])
786 ; return (qtvs, min_theta) }
787 where
788 bndrs = map fst name_taus
789 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
790 equality_constraints = filter isEqPred constraints
791
792 quantify_tvs :: [TcIdSigInfo]
793 -> TcTyVarSet -- the monomorphic tvs
794 -> TcDepVars
795 -> TcM [TcTyVar]
796 -- See Note [Which type variables to quantify]
797 quantify_tvs sigs mono_tvs dep_tvs@(DV { dv_tvs = tau_tvs })
798 -- NB: don't use quantifyZonkedTyVars because the sig stuff might
799 -- be unzonked
800 = quantifyTyVars (mono_tvs `delVarSetList` sig_qtvs)
801 (dep_tvs { dv_tvs = tau_tvs `extendVarSetList` sig_qtvs
802 `extendVarSetList` sig_wcs })
803 -- NB: quantifyTyVars zonks its arguments
804 where
805 sig_qtvs = [ skol | sig <- sigs, (_, skol) <- sig_skols sig ]
806 sig_wcs = [ wc | TISI { sig_bndr = PartialSig { sig_wcs = wcs } } <- sigs
807 , (_, wc) <- wcs ]
808
809
810 ------------------
811 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
812 -- See Note [Growing the tau-tvs using constraints]
813 -- NB: only returns tyvars, never covars
814 growThetaTyVars theta tvs
815 | null theta = tvs_only
816 | otherwise = filterVarSet isTyVar $
817 transCloVarSet mk_next seed_tvs
818 where
819 tvs_only = filterVarSet isTyVar tvs
820 seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
821 (ips, non_ips) = partition isIPPred theta
822 -- See Note [Inheriting implicit parameters] in TcType
823
824 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
825 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
826 grow_one so_far pred tvs
827 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
828 | otherwise = tvs
829 where
830 pred_tvs = tyCoVarsOfType pred
831
832 {- Note [Which type variables to quantify]
833 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
834 When choosing type variables to quantify, the basic plan is to
835 quantify over all type variables that are
836 * free in the tau_tvs, and
837 * not forced to be monomorphic (mono_tvs),
838 for example by being free in the environment.
839
840 However, for a pattern binding, or with wildcards, we might
841 be doing inference *in the presence of a type signature*.
842 Mostly, if there is a signature we use CheckGen, not InferGen,
843 but with pattern bindings or wildcards we might do InferGen
844 and still have a type signature. For example:
845 f :: _ -> a
846 f x = ...
847 or
848 g :: (Eq _a) => _b -> _b
849 or
850 p :: a -> a
851 (p,q) = e
852 In all these cases we use plan InferGen, and hence call simplifyInfer.
853 But those 'a' variables are skolems, and we should be sure to quantify
854 over them, regardless of the monomorphism restriction etc. If we
855 don't, when reporting a type error we panic when we find that a
856 skolem isn't bound by any enclosing implication.
857
858 Moreover we must quantify over all wildcards that are not free in
859 the environment. In the case of 'g' for example, silly though it is,
860 we want to get the inferred type
861 g :: forall t. Eq t => Int -> Int
862 and then report ambiguity, rather than *not* quantifying over 't'
863 and getting some much more mysterious error later. A similar case
864 is
865 h :: F _a -> Int
866
867 That's why we pass sigs to simplifyInfer, and make sure (in
868 quantify_tvs) that we do quantify over them. Trac #10615 is
869 a case in point.
870
871 Note [Quantifying over equality constraints]
872 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
873 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
874 Doing so may simply postpone a type error from the function definition site to
875 its call site. (At worst, imagine (Int ~ Bool)).
876
877 However, consider this
878 forall a. (F [a] ~ Int) => blah
879 Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
880 site we will know 'a', and perhaps we have instance F [Bool] = Int.
881 So we *do* quantify over a type-family equality where the arguments mention
882 the quantified variables.
883
884 Note [Growing the tau-tvs using constraints]
885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
886 (growThetaTyVars insts tvs) is the result of extending the set
887 of tyvars, tvs, using all conceivable links from pred
888
889 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
890 Then growThetaTyVars preds tvs = {a,b,c}
891
892 Notice that
893 growThetaTyVars is conservative if v might be fixed by vs
894 => v `elem` grow(vs,C)
895
896 Note [Quantification with errors]
897 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
898 If we find that the RHS of the definition has some absolutely-insoluble
899 constraints, we abandon all attempts to find a context to quantify
900 over, and instead make the function fully-polymorphic in whatever
901 type we have found. For two reasons
902 a) Minimise downstream errors
903 b) Avoid spurious errors from this function
904
905 But NB that we must include *derived* errors in the check. Example:
906 (a::*) ~ Int#
907 We get an insoluble derived error *~#, and we don't want to discard
908 it before doing the isInsolubleWC test! (Trac #8262)
909
910 Note [Default while Inferring]
911 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
912 Our current plan is that defaulting only happens at simplifyTop and
913 not simplifyInfer. This may lead to some insoluble deferred constraints.
914 Example:
915
916 instance D g => C g Int b
917
918 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
919 type inferred = gamma -> gamma
920
921 Now, if we try to default (alpha := Int) we will be able to refine the implication to
922 (forall b. 0 => C gamma Int b)
923 which can then be simplified further to
924 (forall b. 0 => D gamma)
925 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
926 type: forall g. D g => g -> g
927
928 Instead what will currently happen is that we will get a quantified type
929 (forall g. g -> g) and an implication:
930 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
931
932 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
933 unsolvable implication:
934 forall g. 0 => (forall b. 0 => D g)
935
936 The concrete example would be:
937 h :: C g a s => g -> a -> ST s a
938 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
939
940 But it is quite tedious to do defaulting and resolve the implication constraints, and
941 we have not observed code breaking because of the lack of defaulting in inference, so
942 we don't do it for now.
943
944
945
946 Note [Minimize by Superclasses]
947 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
948 When we quantify over a constraint, in simplifyInfer we need to
949 quantify over a constraint that is minimal in some sense: For
950 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
951 we'd like to quantify over Ord alpha, because we can just get Eq alpha
952 from superclass selection from Ord alpha. This minimization is what
953 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
954 to check the original wanted.
955
956
957 Note [Avoid unnecessary constraint simplification]
958 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
959 -------- NB NB NB (Jun 12) -------------
960 This note not longer applies; see the notes with Trac #4361.
961 But I'm leaving it in here so we remember the issue.)
962 ----------------------------------------
963 When inferring the type of a let-binding, with simplifyInfer,
964 try to avoid unnecessarily simplifying class constraints.
965 Doing so aids sharing, but it also helps with delicate
966 situations like
967
968 instance C t => C [t] where ..
969
970 f :: C [t] => ....
971 f x = let g y = ...(constraint C [t])...
972 in ...
973 When inferring a type for 'g', we don't want to apply the
974 instance decl, because then we can't satisfy (C t). So we
975 just notice that g isn't quantified over 't' and partition
976 the constraints before simplifying.
977
978 This only half-works, but then let-generalisation only half-works.
979
980 *********************************************************************************
981 * *
982 * Main Simplifier *
983 * *
984 ***********************************************************************************
985
986 -}
987
988 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
989 -- Solve the specified Wanted constraints
990 -- Discard the evidence binds
991 -- Discards all Derived stuff in result
992 -- Postcondition: fully zonked and unflattened constraints
993 simplifyWantedsTcM wanted
994 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
995 ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted)
996 ; result <- TcM.zonkWC result
997 ; traceTc "simplifyWantedsTcM }" (ppr result)
998 ; return result }
999
1000 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1001 -- Since solveWanteds returns the residual WantedConstraints,
1002 -- it should always be called within a runTcS or something similar,
1003 -- Result is not zonked
1004 solveWantedsAndDrop wanted
1005 = do { wc <- solveWanteds wanted
1006 ; return (dropDerivedWC wc) }
1007
1008 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1009 -- so that the inert set doesn't mindlessly propagate.
1010 -- NB: wc_simples may be wanted /or/ derived now
1011 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1012 = do { traceTcS "solveWanteds {" (ppr wc)
1013
1014 -- Try the simple bit, including insolubles. Solving insolubles a
1015 -- second time round is a bit of a waste; but the code is simple
1016 -- and the program is wrong anyway, and we don't run the danger
1017 -- of adding Derived insolubles twice; see
1018 -- TcSMonad Note [Do not add duplicate derived insolubles]
1019 ; wc1 <- solveSimpleWanteds simples
1020 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1021 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1022
1023 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
1024
1025 ; dflags <- getDynFlags
1026 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
1027 (WC { wc_simple = simples1, wc_impl = implics2
1028 , wc_insol = insols `unionBags` insols1 })
1029
1030 ; bb <- TcS.getTcEvBindsMap
1031 ; traceTcS "solveWanteds }" $
1032 vcat [ text "final wc =" <+> ppr final_wc
1033 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1034
1035 ; return final_wc }
1036
1037 simpl_loop :: Int -> IntWithInf -> Cts -> Bool
1038 -> WantedConstraints
1039 -> TcS WantedConstraints
1040 simpl_loop n limit floated_eqs no_new_scs
1041 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1042 | isEmptyBag floated_eqs && no_new_scs
1043 = return wc -- Done!
1044
1045 | n `intGtLimit` limit
1046 = do { -- Add an error (not a warning) if we blow the limit,
1047 -- Typically if we blow the limit we are going to report some other error
1048 -- (an unsolved constraint), and we don't want that error to suppress
1049 -- the iteration limit warning!
1050 addErrTcS (hang (text "solveWanteds: too many iterations"
1051 <+> parens (text "limit =" <+> ppr limit))
1052 2 (vcat [ text "Unsolved:" <+> ppr wc
1053 , ppUnless (isEmptyBag floated_eqs) $
1054 text "Floated equalities:" <+> ppr floated_eqs
1055 , ppUnless no_new_scs $
1056 text "New superclasses found"
1057 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
1058 ]))
1059 ; return wc }
1060
1061 | otherwise
1062 = do { let n_floated = lengthBag floated_eqs
1063 ; csTraceTcS $
1064 text "simpl_loop iteration=" <> int n
1065 <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma
1066 , int n_floated <+> text "floated eqs" <> comma
1067 , int (lengthBag simples) <+> text "simples to solve" ])
1068
1069 -- solveSimples may make progress if either float_eqs hold
1070 ; (unifs1, wc1) <- reportUnifications $
1071 solveSimpleWanteds (floated_eqs `unionBags` simples)
1072 -- Put floated_eqs first so they get solved first
1073 -- NB: the floated_eqs may include /derived/ equalities
1074 -- arising from fundeps inside an implication
1075
1076 ; (no_new_scs, wc1) <- expandSuperClasses wc1
1077 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1078
1079 -- We have already tried to solve the nested implications once
1080 -- Try again only if we have unified some meta-variables
1081 -- (which is a bit like adding more givens
1082 -- See Note [Cutting off simpl_loop]
1083 ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
1084 then return (emptyBag, implics)
1085 else solveNestedImplications (implics `unionBags` implics1)
1086
1087 ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
1088 (WC { wc_simple = simples1, wc_impl = implics2
1089 , wc_insol = insols `unionBags` insols1 }) }
1090
1091 expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
1092 -- If there are any unsolved wanteds, expand one step of superclasses for
1093 -- unsolved wanteds or givens
1094 -- See Note [The superclass story] in TcCanonical
1095 expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
1096 | not (anyBag superClassesMightHelp unsolved)
1097 = return (True, wc)
1098 | otherwise
1099 = do { traceTcS "expandSuperClasses {" empty
1100 ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
1101 get acc ct = case isPendingScDict ct of
1102 Just ct' -> (ct':acc, ct')
1103 Nothing -> (acc, ct)
1104 ; pending_given <- getPendingScDicts
1105 ; if null pending_given && null pending_wanted
1106 then do { traceTcS "End expandSuperClasses no-op }" empty
1107 ; return (True, wc) }
1108 else
1109 do { new_given <- makeSuperClasses pending_given
1110 ; new_insols <- solveSimpleGivens new_given
1111 ; new_wanted <- makeSuperClasses pending_wanted
1112 ; traceTcS "End expandSuperClasses }"
1113 (vcat [ text "Given:" <+> ppr pending_given
1114 , text "Insols from given:" <+> ppr new_insols
1115 , text "Wanted:" <+> ppr new_wanted ])
1116 ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
1117 , wc_insol = insols `unionBags` new_insols }) } }
1118
1119 solveNestedImplications :: Bag Implication
1120 -> TcS (Cts, Bag Implication)
1121 -- Precondition: the TcS inerts may contain unsolved simples which have
1122 -- to be converted to givens before we go inside a nested implication.
1123 solveNestedImplications implics
1124 | isEmptyBag implics
1125 = return (emptyBag, emptyBag)
1126 | otherwise
1127 = do { traceTcS "solveNestedImplications starting {" empty
1128 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
1129 ; let floated_eqs = concatBag floated_eqs_s
1130
1131 -- ... and we are back in the original TcS inerts
1132 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1133 -- them in the beginning of this function.
1134 ; traceTcS "solveNestedImplications end }" $
1135 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
1136 , text "unsolved_implics =" <+> ppr unsolved_implics ]
1137
1138 ; return (floated_eqs, catBagMaybes unsolved_implics) }
1139
1140 solveImplication :: Implication -- Wanted
1141 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
1142 Maybe Implication) -- Simplified implication (empty or singleton)
1143 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1144 -- which after trying to solve this implication we must restore to their original value
1145 solveImplication imp@(Implic { ic_tclvl = tclvl
1146 , ic_binds = m_ev_binds
1147 , ic_skols = skols
1148 , ic_given = given_ids
1149 , ic_wanted = wanteds
1150 , ic_info = info
1151 , ic_status = status
1152 , ic_env = env })
1153 | IC_Solved {} <- status
1154 = return (emptyCts, Just imp) -- Do nothing
1155
1156 | otherwise -- Even for IC_Insoluble it is worth doing more work
1157 -- The insoluble stuff might be in one sub-implication
1158 -- and other unsolved goals in another; and we want to
1159 -- solve the latter as much as possible
1160 = do { inerts <- getTcSInerts
1161 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1162
1163 -- Solve the nested constraints
1164 ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
1165 <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
1166 do { let loc = mkGivenLoc tclvl info env
1167 ; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
1168 ; given_insols <- solveSimpleGivens givens_w_scs
1169
1170 ; residual_wanted <- solveWanteds wanteds
1171 -- solveWanteds, *not* solveWantedsAndDrop, because
1172 -- we want to retain derived equalities so we can float
1173 -- them out in floatEqualities
1174
1175 ; no_eqs <- getNoGivenEqs tclvl skols
1176 -- Call getNoGivenEqs /after/ solveWanteds, because
1177 -- solveWanteds can augment the givens, via expandSuperClasses,
1178 -- to reveal given superclass equalities
1179
1180 ; return (no_eqs, given_insols, residual_wanted) }
1181
1182 ; (floated_eqs, residual_wanted)
1183 <- floatEqualities skols no_given_eqs residual_wanted
1184
1185 ; traceTcS "solveImplication 2"
1186 (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs)
1187 ; let final_wanted = residual_wanted `addInsols` given_insols
1188
1189 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
1190 , ic_wanted = final_wanted })
1191 used_tcvs
1192
1193 ; evbinds <- TcS.getTcEvBindsMap
1194 ; traceTcS "solveImplication end }" $ vcat
1195 [ text "no_given_eqs =" <+> ppr no_given_eqs
1196 , text "floated_eqs =" <+> ppr floated_eqs
1197 , text "res_implic =" <+> ppr res_implic
1198 , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
1199
1200 ; return (floated_eqs, res_implic) }
1201
1202 ----------------------
1203 setImplicationStatus :: Implication -> TyCoVarSet -- needed variables
1204 -> TcS (Maybe Implication)
1205 -- Finalise the implication returned from solveImplication:
1206 -- * Set the ic_status field
1207 -- * Trim the ic_wanted field to remove Derived constraints
1208 -- Return Nothing if we can discard the implication altogether
1209 setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
1210 , ic_info = info
1211 , ic_tclvl = tc_lvl
1212 , ic_wanted = wc
1213 , ic_given = givens })
1214 used_tcvs
1215 | some_insoluble
1216 = return $ Just $
1217 implic { ic_status = IC_Insoluble
1218 , ic_wanted = wc { wc_simple = pruned_simples
1219 , wc_insol = pruned_insols } }
1220
1221 | some_unsolved
1222 = return $ Just $
1223 implic { ic_status = IC_Unsolved
1224 , ic_wanted = wc { wc_simple = pruned_simples
1225 , wc_insol = pruned_insols } }
1226
1227 | otherwise -- Everything is solved; look at the implications
1228 -- See Note [Tracking redundant constraints]
1229 = do { ev_binds <- case m_ev_binds_var of
1230 Just (EvBindsVar ref _) -> TcS.readTcRef ref
1231 Nothing -> return emptyEvBindMap
1232 ; let all_needs = neededEvVars ev_binds
1233 (used_tcvs `unionVarSet` implic_needs)
1234
1235 dead_givens | warnRedundantGivens info
1236 = filterOut (`elemVarSet` all_needs) givens
1237 | otherwise = [] -- None to report
1238
1239 final_needs = all_needs `delVarSetList` givens
1240
1241 discard_entire_implication -- Can we discard the entire implication?
1242 = null dead_givens -- No warning from this implication
1243 && isEmptyBag pruned_implics -- No live children
1244 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
1245
1246 final_status = IC_Solved { ics_need = final_needs
1247 , ics_dead = dead_givens }
1248 final_implic = implic { ic_status = final_status
1249 , ic_wanted = wc { wc_simple = pruned_simples
1250 , wc_insol = pruned_insols
1251 , wc_impl = pruned_implics } }
1252 -- We can only prune the child implications (pruned_implics)
1253 -- in the IC_Solved status case, because only then we can
1254 -- accumulate their needed evidence variales into the
1255 -- IC_Solved final_status field of the parent implication.
1256
1257 ; return $ if discard_entire_implication
1258 then Nothing
1259 else Just final_implic }
1260 where
1261 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
1262
1263 some_insoluble = insolubleWC tc_lvl wc
1264 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
1265 || isNothing mb_implic_needs
1266
1267 pruned_simples = dropDerivedSimples simples
1268 pruned_insols = dropDerivedInsols insols
1269 pruned_implics = filterBag need_to_keep_implic implics
1270
1271 mb_implic_needs :: Maybe VarSet
1272 -- Just vs => all implics are IC_Solved, with 'vs' needed
1273 -- Nothing => at least one implic is not IC_Solved
1274 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
1275 Just implic_needs = mb_implic_needs
1276
1277 add_implic implic acc
1278 | Just vs_acc <- acc
1279 , IC_Solved { ics_need = vs } <- ic_status implic
1280 = Just (vs `unionVarSet` vs_acc)
1281 | otherwise = Nothing
1282
1283 need_to_keep_implic ic
1284 | IC_Solved { ics_dead = [] } <- ic_status ic
1285 -- Fully solved, and no redundant givens to report
1286 , isEmptyBag (wc_impl (ic_wanted ic))
1287 -- And no children that might have things to report
1288 = False
1289 | otherwise
1290 = True
1291
1292 warnRedundantGivens :: SkolemInfo -> Bool
1293 warnRedundantGivens (SigSkol ctxt _)
1294 = case ctxt of
1295 FunSigCtxt _ warn_redundant -> warn_redundant
1296 ExprSigCtxt -> True
1297 _ -> False
1298
1299 -- To think about: do we want to report redundant givens for
1300 -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
1301 warnRedundantGivens (InstSkol {}) = True
1302 warnRedundantGivens _ = False
1303
1304 neededEvVars :: EvBindMap -> VarSet -> VarSet
1305 -- Find all the evidence variables that are "needed",
1306 -- and then delete all those bound by the evidence bindings
1307 -- See note [Tracking redundant constraints]
1308 neededEvVars ev_binds initial_seeds
1309 = needed `minusVarSet` bndrs
1310 where
1311 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
1312 needed = transCloVarSet also_needs seeds
1313 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
1314
1315 add_wanted :: EvBind -> VarSet -> VarSet
1316 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1317 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1318 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1319
1320 also_needs :: VarSet -> VarSet
1321 also_needs needs
1322 = foldVarSet add emptyVarSet needs
1323 where
1324 add v needs
1325 | Just ev_bind <- lookupEvBind ev_binds v
1326 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
1327 , is_given
1328 = evVarsOfTerm rhs `unionVarSet` needs
1329 | otherwise
1330 = needs
1331
1332 add_bndr :: EvBind -> VarSet -> VarSet
1333 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
1334
1335
1336 {-
1337 Note [Tracking redundant constraints]
1338 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1339 With Opt_WarnRedundantConstraints, GHC can report which
1340 constraints of a type signature (or instance declaration) are
1341 redundant, and can be omitted. Here is an overview of how it
1342 works:
1343
1344 ----- What is a redundant constraint?
1345
1346 * The things that can be redundant are precisely the Given
1347 constraints of an implication.
1348
1349 * A constraint can be redundant in two different ways:
1350 a) It is implied by other givens. E.g.
1351 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1352 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1353 b) It is not needed by the Wanted constraints covered by the
1354 implication E.g.
1355 f :: Eq a => a -> Bool
1356 f x = True -- Equality not used
1357
1358 * To find (a), when we have two Given constraints,
1359 we must be careful to drop the one that is a naked variable (if poss).
1360 So if we have
1361 f :: (Eq a, Ord a) => blah
1362 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1363 [G] d2 :: Eq a
1364 We want to discard d2 in favour of the superclass selection from
1365 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1366 See Note [Replacement vs keeping].
1367
1368 * To find (b) we need to know which evidence bindings are 'wanted';
1369 hence the eb_is_given field on an EvBind.
1370
1371 ----- How tracking works
1372
1373 * When the constraint solver finishes solving all the wanteds in
1374 an implication, it sets its status to IC_Solved
1375
1376 - The ics_dead field, of IC_Solved, records the subset of this implication's
1377 ic_given that are redundant (not needed).
1378
1379 - The ics_need field of IC_Solved then records all the
1380 in-scope (given) evidence variables bound by the context, that
1381 were needed to solve this implication, including all its nested
1382 implications. (We remove the ic_given of this implication from
1383 the set, of course.)
1384
1385 * We compute which evidence variables are needed by an implication
1386 in setImplicationStatus. A variable is needed if
1387 a) it is free in the RHS of a Wanted EvBind,
1388 b) it is free in the RHS of an EvBind whose LHS is needed,
1389 c) it is in the ics_need of a nested implication.
1390 d) it is listed in the tcs_used_tcvs field of the nested TcSEnv
1391
1392 * We need to be careful not to discard an implication
1393 prematurely, even one that is fully solved, because we might
1394 thereby forget which variables it needs, and hence wrongly
1395 report a constraint as redundant. But we can discard it once
1396 its free vars have been incorporated into its parent; or if it
1397 simply has no free vars. This careful discarding is also
1398 handled in setImplicationStatus.
1399
1400 ----- Reporting redundant constraints
1401
1402 * TcErrors does the actual warning, in warnRedundantConstraints.
1403
1404 * We don't report redundant givens for *every* implication; only
1405 for those which reply True to TcSimplify.warnRedundantGivens:
1406
1407 - For example, in a class declaration, the default method *can*
1408 use the class constraint, but it certainly doesn't *have* to,
1409 and we don't want to report an error there.
1410
1411 - More subtly, in a function definition
1412 f :: (Ord a, Ord a, Ix a) => a -> a
1413 f x = rhs
1414 we do an ambiguity check on the type (which would find that one
1415 of the Ord a constraints was redundant), and then we check that
1416 the definition has that type (which might find that both are
1417 redundant). We don't want to report the same error twice, so we
1418 disable it for the ambiguity check. Hence using two different
1419 FunSigCtxts, one with the warn-redundant field set True, and the
1420 other set False in
1421 - TcBinds.tcSpecPrag
1422 - TcBinds.tcTySig
1423
1424 This decision is taken in setImplicationStatus, rather than TcErrors
1425 so that we can discard implication constraints that we don't need.
1426 So ics_dead consists only of the *reportable* redundant givens.
1427
1428 ----- Shortcomings
1429
1430 Consider (see Trac #9939)
1431 f2 :: (Eq a, Ord a) => a -> a -> Bool
1432 -- Ord a redundant, but Eq a is reported
1433 f2 x y = (x == y)
1434
1435 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1436 really not easy to detect that!
1437
1438
1439 Note [Cutting off simpl_loop]
1440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1441 It is very important not to iterate in simpl_loop unless there is a chance
1442 of progress. Trac #8474 is a classic example:
1443
1444 * There's a deeply-nested chain of implication constraints.
1445 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1446
1447 * From the innermost one we get a [D] alpha ~ Int,
1448 but alpha is untouchable until we get out to the outermost one
1449
1450 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1451 is untouchable, the solveInteract in simpl_loop makes no progress
1452
1453 * So there is no point in attempting to re-solve
1454 ?yn:betan => [W] ?x:Int
1455 via solveNestedImplications, because we'll just get the
1456 same [D] again
1457
1458 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1459 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1460 exponentially many) iterations!
1461
1462 Conclusion: we should call solveNestedImplications only if we did
1463 some unifiction in solveSimpleWanteds; because that's the only way
1464 we'll get more Givens (a unificaiton is like adding a Given) to
1465 allow the implication to make progress.
1466 -}
1467
1468 promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
1469 -- When we float a constraint out of an implication we must restore
1470 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1471 -- See Note [Promoting unification variables]
1472 promoteTyVar tclvl tv
1473 | isFloatedTouchableMetaTyVar tclvl tv
1474 = do { cloned_tv <- TcM.cloneMetaTyVar tv
1475 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1476 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
1477 | otherwise
1478 = return ()
1479
1480 promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
1481 -- When we float a constraint out of an implication we must restore
1482 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1483 -- See Note [Promoting unification variables]
1484 -- We don't just call promoteTyVar because we want to use unifyTyVar,
1485 -- not writeMetaTyVar
1486 promoteTyVarTcS tclvl tv
1487 | isFloatedTouchableMetaTyVar tclvl tv
1488 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1489 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1490 ; unifyTyVar tv (mkTyVarTy rhs_tv) }
1491 | otherwise
1492 = return ()
1493
1494 -- | If the tyvar is a RuntimeRep var, set it to PtrRepLifted. Returns whether or
1495 -- not this happened.
1496 defaultTyVar :: TcTyVar -> TcM ()
1497 -- Precondition: MetaTyVars only
1498 -- See Note [DefaultTyVar]
1499 defaultTyVar the_tv
1500 | isRuntimeRepVar the_tv
1501 = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
1502 ; writeMetaTyVar the_tv ptrRepLiftedTy }
1503
1504 | otherwise = return () -- The common case
1505
1506 -- | Like 'defaultTyVar', but in the TcS monad.
1507 defaultTyVarTcS :: TcTyVar -> TcS Bool
1508 defaultTyVarTcS the_tv
1509 | isRuntimeRepVar the_tv
1510 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
1511 ; unifyTyVar the_tv ptrRepLiftedTy
1512 ; return True }
1513 | otherwise
1514 = return False -- the common case
1515
1516 approximateWC :: WantedConstraints -> Cts
1517 -- Postcondition: Wanted or Derived Cts
1518 -- See Note [ApproximateWC]
1519 approximateWC wc
1520 = float_wc emptyVarSet wc
1521 where
1522 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
1523 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1524 = filterBag is_floatable simples `unionBags`
1525 do_bag (float_implic new_trapping_tvs) implics
1526 where
1527 is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` new_trapping_tvs
1528 new_trapping_tvs = transCloVarSet grow trapping_tvs
1529
1530 grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
1531 grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
1532 grow_one so_far ct tvs
1533 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
1534 | otherwise = tvs
1535 where
1536 ct_tvs = tyCoVarsOfCt ct
1537
1538 float_implic :: TcTyCoVarSet -> Implication -> Cts
1539 float_implic trapping_tvs imp
1540 | ic_no_eqs imp -- No equalities, so float
1541 = float_wc new_trapping_tvs (ic_wanted imp)
1542 | otherwise -- Don't float out of equalities
1543 = emptyCts -- See Note [ApproximateWC]
1544 where
1545 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1546 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1547 do_bag f = foldrBag (unionBags.f) emptyBag
1548
1549 {-
1550 Note [ApproximateWC]
1551 ~~~~~~~~~~~~~~~~~~~~
1552 approximateWC takes a constraint, typically arising from the RHS of a
1553 let-binding whose type we are *inferring*, and extracts from it some
1554 *simple* constraints that we might plausibly abstract over. Of course
1555 the top-level simple constraints are plausible, but we also float constraints
1556 out from inside, if they are not captured by skolems.
1557
1558 The same function is used when doing type-class defaulting (see the call
1559 to applyDefaultingRules) to extract constraints that that might be defaulted.
1560
1561 There are two caveats:
1562
1563 1. We do *not* float anything out if the implication binds equality
1564 constraints, because that defeats the OutsideIn story. Consider
1565 data T a where
1566 TInt :: T Int
1567 MkT :: T a
1568
1569 f TInt = 3::Int
1570
1571 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1572 f :: T a -> res
1573 We don't want to float (res~Int) out because then we'll infer
1574 f :: T a -> Int
1575 which is only on of the possible types. (GHC 7.6 accidentally *did*
1576 float out of such implications, which meant it would happily infer
1577 non-principal types.)
1578
1579 2. We do not float out an inner constraint that shares a type variable
1580 (transitively) with one that is trapped by a skolem. Eg
1581 forall a. F a ~ beta, Integral beta
1582 We don't want to float out (Integral beta). Doing so would be bad
1583 when defaulting, because then we'll default beta:=Integer, and that
1584 makes the error message much worse; we'd get
1585 Can't solve F a ~ Integer
1586 rather than
1587 Can't solve Integral (F a)
1588
1589 Moreover, floating out these "contaminated" constraints doesn't help
1590 when generalising either. If we generalise over (Integral b), we still
1591 can't solve the retained implication (forall a. F a ~ b). Indeed,
1592 arguably that too would be a harder error to understand.
1593
1594 Note [DefaultTyVar]
1595 ~~~~~~~~~~~~~~~~~~~
1596 defaultTyVar is used on any un-instantiated meta type variables to
1597 default any RuntimeRep variables to PtrRepLifted. This is important
1598 to ensure that instance declarations match. For example consider
1599
1600 instance Show (a->b)
1601 foo x = show (\_ -> True)
1602
1603 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
1604 and that won't match the typeKind (*) in the instance decl. See tests
1605 tc217 and tc175.
1606
1607 We look only at touchable type variables. No further constraints
1608 are going to affect these type variables, so it's time to do it by
1609 hand. However we aren't ready to default them fully to () or
1610 whatever, because the type-class defaulting rules have yet to run.
1611
1612 An alternate implementation would be to emit a derived constraint setting
1613 the RuntimeRep variable to PtrRepLifted, but this seems unnecessarily indirect.
1614
1615 Note [Promote _and_ default when inferring]
1616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1617 When we are inferring a type, we simplify the constraint, and then use
1618 approximateWC to produce a list of candidate constraints. Then we MUST
1619
1620 a) Promote any meta-tyvars that have been floated out by
1621 approximateWC, to restore invariant (MetaTvInv) described in
1622 Note [TcLevel and untouchable type variables] in TcType.
1623
1624 b) Default the kind of any meta-tyyvars that are not mentioned in
1625 in the environment.
1626
1627 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1628 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1629 should! If we don't solve the constraint, we'll stupidly quantify over
1630 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1631 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1632 Trac #7641 is a simpler example.
1633
1634 Note [Promoting unification variables]
1635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1636 When we float an equality out of an implication we must "promote" free
1637 unification variables of the equality, in order to maintain Invariant
1638 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1639 leftover implication.
1640
1641 This is absolutely necessary. Consider the following example. We start
1642 with two implications and a class with a functional dependency.
1643
1644 class C x y | x -> y
1645 instance C [a] [a]
1646
1647 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1648 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1649
1650 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1651 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1652 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1653 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1654 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1655
1656 class C x y | x -> y where
1657 op :: x -> y -> ()
1658
1659 instance C [a] [a]
1660
1661 type family F a :: *
1662
1663 h :: F Int -> ()
1664 h = undefined
1665
1666 data TEx where
1667 TEx :: a -> TEx
1668
1669 f (x::beta) =
1670 let g1 :: forall b. b -> ()
1671 g1 _ = h [x]
1672 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1673 in (g1 '3', g2 undefined)
1674
1675
1676 Note [Solving Family Equations]
1677 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1678 After we are done with simplification we may be left with constraints of the form:
1679 [Wanted] F xis ~ beta
1680 If 'beta' is a touchable unification variable not already bound in the TyBinds
1681 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1682
1683 When is it ok to do so?
1684 1) 'beta' must not already be defaulted to something. Example:
1685
1686 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1687 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1688 have to report this as unsolved.
1689
1690 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1691 set [beta := F xis] only if beta is not among the free variables of xis.
1692
1693 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1694 of type family equations. See Inert Set invariants in TcInteract.
1695
1696 This solving is now happening during zonking, see Note [Unflattening while zonking]
1697 in TcMType.
1698
1699
1700 *********************************************************************************
1701 * *
1702 * Floating equalities *
1703 * *
1704 *********************************************************************************
1705
1706 Note [Float Equalities out of Implications]
1707 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1708 For ordinary pattern matches (including existentials) we float
1709 equalities out of implications, for instance:
1710 data T where
1711 MkT :: Eq a => a -> T
1712 f x y = case x of MkT _ -> (y::Int)
1713 We get the implication constraint (x::T) (y::alpha):
1714 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1715 We want to float out the equality into a scope where alpha is no
1716 longer untouchable, to solve the implication!
1717
1718 But we cannot float equalities out of implications whose givens may
1719 yield or contain equalities:
1720
1721 data T a where
1722 T1 :: T Int
1723 T2 :: T Bool
1724 T3 :: T a
1725
1726 h :: T a -> a -> Int
1727
1728 f x y = case x of
1729 T1 -> y::Int
1730 T2 -> y::Bool
1731 T3 -> h x y
1732
1733 We generate constraint, for (x::T alpha) and (y :: beta):
1734 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1735 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1736 (alpha ~ beta) -- From 3rd branch
1737
1738 If we float the equality (beta ~ Int) outside of the first implication and
1739 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1740 But if we just leave them inside the implications, we unify alpha := beta and
1741 solve everything.
1742
1743 Principle:
1744 We do not want to float equalities out which may
1745 need the given *evidence* to become soluble.
1746
1747 Consequence: classes with functional dependencies don't matter (since there is
1748 no evidence for a fundep equality), but equality superclasses do matter (since
1749 they carry evidence).
1750 -}
1751
1752 floatEqualities :: [TcTyVar] -> Bool
1753 -> WantedConstraints
1754 -> TcS (Cts, WantedConstraints)
1755 -- Main idea: see Note [Float Equalities out of Implications]
1756 --
1757 -- Precondition: the wc_simple of the incoming WantedConstraints are
1758 -- fully zonked, so that we can see their free variables
1759 --
1760 -- Postcondition: The returned floated constraints (Cts) are only
1761 -- Wanted or Derived
1762 --
1763 -- Also performs some unifications (via promoteTyVar), adding to
1764 -- monadically-carried ty_binds. These will be used when processing
1765 -- floated_eqs later
1766 --
1767 -- Subtleties: Note [Float equalities from under a skolem binding]
1768 -- Note [Skolem escape]
1769 floatEqualities skols no_given_eqs
1770 wanteds@(WC { wc_simple = simples })
1771 | not no_given_eqs -- There are some given equalities, so don't float
1772 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1773 | otherwise
1774 = do { outer_tclvl <- TcS.getTcLevel
1775 ; mapM_ (promoteTyVarTcS outer_tclvl)
1776 (tyCoVarsOfCtsList float_eqs)
1777 -- See Note [Promoting unification variables]
1778
1779 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1780 , text "Simples =" <+> ppr simples
1781 , text "Floated eqs =" <+> ppr float_eqs])
1782 ; return ( float_eqs
1783 , wanteds { wc_simple = remaining_simples } ) }
1784 where
1785 skol_set = mkVarSet skols
1786 (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
1787
1788 usefulToFloat :: VarSet -> Ct -> Bool
1789 usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
1790 = is_meta_var_eq pred &&
1791 (tyCoVarsOfType pred `disjointVarSet` skol_set)
1792 where
1793 pred = ctPred ct
1794
1795 -- Float out alpha ~ ty, or ty ~ alpha
1796 -- which might be unified outside
1797 -- See Note [Which equalities to float]
1798 is_meta_var_eq pred
1799 | EqPred NomEq ty1 ty2 <- classifyPredType pred
1800 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
1801 (Just tv1, _) -> float_tv_eq tv1 ty2
1802 (_, Just tv2) -> float_tv_eq tv2 ty1
1803 _ -> False
1804 | otherwise
1805 = False
1806
1807 float_tv_eq tv1 ty2 -- See Note [Which equalities to float]
1808 = isMetaTyVar tv1
1809 && (not (isSigTyVar tv1) || isTyVarTy ty2)
1810
1811 {- Note [Float equalities from under a skolem binding]
1812 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1813 Which of the simple equalities can we float out? Obviously, only
1814 ones that don't mention the skolem-bound variables. But that is
1815 over-eager. Consider
1816 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1817 The second constraint doesn't mention 'a'. But if we float it,
1818 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1819 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1820 we left with the constraint
1821 [2] forall a. a ~ gamma'[1]
1822 which is insoluble because gamma became untouchable.
1823
1824 Solution: float only constraints that stand a jolly good chance of
1825 being soluble simply by being floated, namely ones of form
1826 a ~ ty
1827 where 'a' is a currently-untouchable unification variable, but may
1828 become touchable by being floated (perhaps by more than one level).
1829
1830 We had a very complicated rule previously, but this is nice and
1831 simple. (To see the notes, look at this Note in a version of
1832 TcSimplify prior to Oct 2014).
1833
1834 Note [Which equalities to float]
1835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1836 Which equalities should we float? We want to float ones where there
1837 is a decent chance that floating outwards will allow unification to
1838 happen. In particular:
1839
1840 Float out equalities of form (alpaha ~ ty) or (ty ~ alpha), where
1841
1842 * alpha is a meta-tyvar.
1843
1844 * And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that
1845 case, floating out won't help either, and it may affect grouping
1846 of error messages.
1847
1848 Note [Skolem escape]
1849 ~~~~~~~~~~~~~~~~~~~~
1850 You might worry about skolem escape with all this floating.
1851 For example, consider
1852 [2] forall a. (a ~ F beta[2] delta,
1853 Maybe beta[2] ~ gamma[1])
1854
1855 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1856 solve with gamma := beta. But what if later delta:=Int, and
1857 F b Int = b.
1858 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1859 skolem has escaped!
1860
1861 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1862 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1863
1864
1865 *********************************************************************************
1866 * *
1867 * Defaulting and disamgiguation *
1868 * *
1869 *********************************************************************************
1870 -}
1871
1872 applyDefaultingRules :: WantedConstraints -> TcS Bool
1873 -- True <=> I did some defaulting, by unifying a meta-tyvar
1874 -- Imput WantedConstraints are not necessarily zonked
1875
1876 applyDefaultingRules wanteds
1877 | isEmptyWC wanteds
1878 = return False
1879 | otherwise
1880 = do { info@(default_tys, _) <- getDefaultInfo
1881 ; wanteds <- TcS.zonkWC wanteds
1882
1883 ; let groups = findDefaultableGroups info wanteds
1884
1885 ; traceTcS "applyDefaultingRules {" $
1886 vcat [ text "wanteds =" <+> ppr wanteds
1887 , text "groups =" <+> ppr groups
1888 , text "info =" <+> ppr info ]
1889
1890 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1891
1892 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1893
1894 ; return (or something_happeneds) }
1895
1896 findDefaultableGroups
1897 :: ( [Type]
1898 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1899 -> WantedConstraints -- Unsolved (wanted or derived)
1900 -> [(TyVar, [Ct])]
1901 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1902 | null default_tys
1903 = []
1904 | otherwise
1905 = [ (tv, map fstOf3 group)
1906 | group@((_,_,tv):_) <- unary_groups
1907 , defaultable_tyvar tv
1908 , defaultable_classes (map sndOf3 group) ]
1909 where
1910 simples = approximateWC wanteds
1911 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
1912 unary_groups = equivClasses cmp_tv unaries
1913
1914 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
1915 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
1916 non_unaries :: [Ct] -- and *other* constraints
1917
1918 -- Finds unary type-class constraints
1919 -- But take account of polykinded classes like Typeable,
1920 -- which may look like (Typeable * (a:*)) (Trac #8931)
1921 find_unary cc
1922 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
1923 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
1924 -- Ignore invisible arguments for this purpose
1925 , Just tv <- tcGetTyVar_maybe ty
1926 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
1927 -- we definitely don't want to try to assign to those!
1928 = Left (cc, cls, tv)
1929 find_unary cc = Right cc -- Non unary or non dictionary
1930
1931 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
1932 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
1933
1934 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1935
1936 defaultable_tyvar tv
1937 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1938 b2 = not (tv `elemVarSet` bad_tvs)
1939 in b1 && b2
1940
1941 defaultable_classes clss
1942 | extended_defaults = any isInteractiveClass clss
1943 | otherwise = all is_std_class clss && (any is_num_class clss)
1944
1945 -- In interactive mode, or with -XExtendedDefaultRules,
1946 -- we default Show a to Show () to avoid graututious errors on "show []"
1947 isInteractiveClass cls
1948 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey
1949 , ordClassKey, foldableClassKey
1950 , traversableClassKey])
1951
1952 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1953 -- is_num_class adds IsString to the standard numeric classes,
1954 -- when -foverloaded-strings is enabled
1955
1956 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1957 -- Similarly is_std_class
1958
1959 ------------------------------
1960 disambigGroup :: [Type] -- The default types
1961 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
1962 -- sharing same type variable
1963 -> TcS Bool -- True <=> something happened, reflected in ty_binds
1964
1965 disambigGroup [] _
1966 = return False
1967 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
1968 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
1969 ; fake_ev_binds_var <- TcS.newTcEvBinds
1970 ; tclvl <- TcS.getTcLevel
1971 ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet
1972 (pushTcLevel tclvl) try_group
1973
1974 ; if success then
1975 -- Success: record the type variable binding, and return
1976 do { unifyTyVar the_tv default_ty
1977 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
1978 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
1979 ; return True }
1980 else
1981 -- Failure: try with the next type
1982 do { traceTcS "disambigGroup failed, will try other default types }"
1983 (ppr default_ty)
1984 ; disambigGroup default_tys group } }
1985 where
1986 try_group
1987 | Just subst <- mb_subst
1988 = do { lcl_env <- TcS.getLclEnv
1989 ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
1990 , ctl_env = lcl_env
1991 , ctl_t_or_k = Nothing
1992 , ctl_depth = initialSubGoalDepth }
1993 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
1994 wanteds
1995 ; fmap isEmptyWC $
1996 solveSimpleWanteds $ listToBag $
1997 map mkNonCanonical wanted_evs }
1998
1999 | otherwise
2000 = return False
2001
2002 the_ty = mkTyVarTy the_tv
2003 mb_subst = tcMatchTy the_ty default_ty
2004 -- Make sure the kinds match too; hence this call to tcMatchTy
2005 -- E.g. suppose the only constraint was (Typeable k (a::k))
2006 -- With the addition of polykinded defaulting we also want to reject
2007 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2008
2009
2010 {-
2011 Note [Avoiding spurious errors]
2012 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2013 When doing the unification for defaulting, we check for skolem
2014 type variables, and simply don't default them. For example:
2015 f = (*) -- Monomorphic
2016 g :: Num a => a -> a
2017 g x = f x x
2018 Here, we get a complaint when checking the type signature for g,
2019 that g isn't polymorphic enough; but then we get another one when
2020 dealing with the (Num a) context arising from f's definition;
2021 we try to unify a with Int (to default it), but find that it's
2022 already been unified with the rigid variable from g's type sig.
2023 -}