Improve improvement in the constraint solver
[ghc.git] / compiler / typecheck / TcSimplify.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcSimplify(
4 simplifyInfer,
5 quantifyPred, growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, simplifyInteractive,
9 solveWantedsTcM,
10
11 -- For Rules we need these twoo
12 solveWanteds, runTcS
13 ) where
14
15 #include "HsVersions.h"
16
17 import TcRnTypes
18 import TcRnMonad
19 import TcErrors
20 import TcMType as TcM
21 import TcType
22 import TcSMonad as TcS
23 import TcInteract
24 import Kind ( isKind, defaultKind_maybe )
25 import Inst
26 import Unify ( tcMatchTy )
27 import Type ( classifyPredType, isIPClass, PredTree(..)
28 , getClassPredTys_maybe, EqRel(..) )
29 import TyCon ( isTypeFamilyTyCon )
30 import Class ( Class )
31 import Id ( idType )
32 import Var
33 import Unique
34 import VarSet
35 import TcEvidence
36 import Name
37 import Bag
38 import ListSetOps
39 import Util
40 import PrelInfo
41 import PrelNames
42 import Control.Monad ( unless )
43 import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
44 import Class ( classKey )
45 import Maybes ( isNothing )
46 import Outputable
47 import FastString
48 import TrieMap () -- DV: for now
49 import Data.List( partition )
50
51 {-
52 *********************************************************************************
53 * *
54 * External interface *
55 * *
56 *********************************************************************************
57 -}
58
59 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
60 -- Simplify top-level constraints
61 -- Usually these will be implications,
62 -- but when there is nothing to quantify we don't wrap
63 -- in a degenerate implication, so we do that here instead
64 simplifyTop wanteds
65 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
66 ; (final_wc, binds1) <- runTcS (simpl_top wanteds)
67 ; traceTc "End simplifyTop }" empty
68
69 ; traceTc "reportUnsolved {" empty
70 ; binds2 <- reportUnsolved final_wc
71 ; traceTc "reportUnsolved }" empty
72
73 ; return (binds1 `unionBags` binds2) }
74
75 simpl_top :: WantedConstraints -> TcS WantedConstraints
76 -- See Note [Top-level Defaulting Plan]
77 simpl_top wanteds
78 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
79 -- This is where the main work happens
80 ; try_tyvar_defaulting wc_first_go }
81 where
82 try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
83 try_tyvar_defaulting wc
84 | isEmptyWC wc
85 = return wc
86 | otherwise
87 = do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc)
88 ; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
89 -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
90 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
91 -- and we definitely don't want to try to assign to those!
92
93 ; meta_tvs' <- mapM defaultTyVar meta_tvs -- Has unification side effects
94 ; if meta_tvs' == meta_tvs -- No defaulting took place;
95 -- (defaulting returns fresh vars)
96 then try_class_defaulting wc
97 else do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
98 -- See Note [Must simplify after defaulting]
99 ; try_class_defaulting wc_residual } }
100
101 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
102 try_class_defaulting wc
103 | isEmptyWC wc
104 = return wc
105 | otherwise -- See Note [When to do type-class defaulting]
106 = do { something_happened <- applyDefaultingRules wc
107 -- See Note [Top-level Defaulting Plan]
108 ; if something_happened
109 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
110 ; try_class_defaulting wc_residual }
111 else return wc }
112
113 {-
114 Note [When to do type-class defaulting]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
117 was false, on the grounds that defaulting can't help solve insoluble
118 constraints. But if we *don't* do defaulting we may report a whole
119 lot of errors that would be solved by defaulting; these errors are
120 quite spurious because fixing the single insoluble error means that
121 defaulting happens again, which makes all the other errors go away.
122 This is jolly confusing: Trac #9033.
123
124 So it seems better to always do type-class defaulting.
125
126 However, always doing defaulting does mean that we'll do it in
127 situations like this (Trac #5934):
128 run :: (forall s. GenST s) -> Int
129 run = fromInteger 0
130 We don't unify the return type of fromInteger with the given function
131 type, because the latter involves foralls. So we're left with
132 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
133 Now we do defaulting, get alpha := Integer, and report that we can't
134 match Integer with (forall s. GenST s) -> Int. That's not totally
135 stupid, but perhaps a little strange.
136
137 Another potential alternative would be to suppress *all* non-insoluble
138 errors if there are *any* insoluble errors, anywhere, but that seems
139 too drastic.
140
141 Note [Must simplify after defaulting]
142 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
143 We may have a deeply buried constraint
144 (t:*) ~ (a:Open)
145 which we couldn't solve because of the kind incompatibility, and 'a' is free.
146 Then when we default 'a' we can solve the constraint. And we want to do
147 that before starting in on type classes. We MUST do it before reporting
148 errors, because it isn't an error! Trac #7967 was due to this.
149
150 Note [Top-level Defaulting Plan]
151 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
152 We have considered two design choices for where/when to apply defaulting.
153 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
154 simple constraints, maybe deep inside the context of implications.
155 This used to be the case in GHC 7.4.1.
156 (ii) Do it in a tight loop at simplifyTop, once all other constraint has
157 finished. This is the current story.
158
159 Option (i) had many disadvantages:
160 a) First it was deep inside the actual solver,
161 b) Second it was dependent on the context (Infer a type signature,
162 or Check a type signature, or Interactive) since we did not want
163 to always start defaulting when inferring (though there is an exception to
164 this see Note [Default while Inferring])
165 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
166 f :: Int -> Bool
167 f x = const True (\y -> let w :: a -> a
168 w a = const a (y+1)
169 in w y)
170 We will get an implication constraint (for beta the type of y):
171 [untch=beta] forall a. 0 => Num beta
172 which we really cannot default /while solving/ the implication, since beta is
173 untouchable.
174
175 Instead our new defaulting story is to pull defaulting out of the solver loop and
176 go with option (i), implemented at SimplifyTop. Namely:
177 - First have a go at solving the residual constraint of the whole program
178 - Try to approximate it with a simple constraint
179 - Figure out derived defaulting equations for that simple constraint
180 - Go round the loop again if you did manage to get some equations
181
182 Now, that has to do with class defaulting. However there exists type variable /kind/
183 defaulting. Again this is done at the top-level and the plan is:
184 - At the top-level, once you had a go at solving the constraint, do
185 figure out /all/ the touchable unification variables of the wanted constraints.
186 - Apply defaulting to their kinds
187
188 More details in Note [DefaultTyVar].
189 -}
190
191 ------------------
192 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
193 simplifyAmbiguityCheck ty wanteds
194 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
195 ; (final_wc, _binds) <- runTcS (simpl_top wanteds)
196 ; traceTc "End simplifyAmbiguityCheck }" empty
197
198 -- Normally report all errors; but with -XAllowAmbiguousTypes
199 -- report only insoluble ones, since they represent genuinely
200 -- inaccessible code
201 ; allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
202 ; traceTc "reportUnsolved(ambig) {" empty
203 ; unless (allow_ambiguous && not (insolubleWC final_wc))
204 (discardResult (reportUnsolved final_wc))
205 ; traceTc "reportUnsolved(ambig) }" empty
206
207 ; return () }
208
209 ------------------
210 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
211 simplifyInteractive wanteds
212 = traceTc "simplifyInteractive" empty >>
213 simplifyTop wanteds
214
215 ------------------
216 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
217 -> TcM () -- Succeeds iff the constraint is soluble
218 simplifyDefault theta
219 = do { traceTc "simplifyInteractive" empty
220 ; wanted <- newWanteds DefaultOrigin theta
221 ; unsolved <- solveWantedsTcM wanted
222
223 ; traceTc "reportUnsolved {" empty
224 -- See Note [Deferring coercion errors to runtime]
225 ; reportAllUnsolved unsolved
226 ; traceTc "reportUnsolved }" empty
227
228 ; return () }
229
230 {-
231 *********************************************************************************
232 * *
233 * Inference
234 * *
235 ***********************************************************************************
236
237 Note [Inferring the type of a let-bound variable]
238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
239 Consider
240 f x = rhs
241
242 To infer f's type we do the following:
243 * Gather the constraints for the RHS with ambient level *one more than*
244 the current one. This is done by the call
245 pushLevelAndCaptureConstraints (tcMonoBinds...)
246 in TcBinds.tcPolyInfer
247
248 * Call simplifyInfer to simplify the constraints and decide what to
249 quantify over. We pass in the level used for the RHS constraints,
250 here called rhs_tclvl.
251
252 This ensures that the implication constraint we generate, if any,
253 has a strictly-increased level compared to the ambient level outside
254 the let binding.
255 -}
256
257 simplifyInfer :: TcLevel -- Used when generating the constraints
258 -> Bool -- Apply monomorphism restriction
259 -> [(Name, TcTauType)] -- Variables to be generalised,
260 -- and their tau-types
261 -> WantedConstraints
262 -> TcM ([TcTyVar], -- Quantify over these type variables
263 [EvVar], -- ... and these constraints (fully zonked)
264 Bool, -- The monomorphism restriction did something
265 -- so the results type is not as general as
266 -- it could be
267 TcEvBinds) -- ... binding these evidence variables
268 simplifyInfer rhs_tclvl apply_mr name_taus wanteds
269 | isEmptyWC wanteds
270 = do { gbl_tvs <- tcGetGlobalTyVars
271 ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
272 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
273 ; return (qtkvs, [], False, emptyTcEvBinds) }
274
275 | otherwise
276 = do { traceTc "simplifyInfer {" $ vcat
277 [ ptext (sLit "binds =") <+> ppr name_taus
278 , ptext (sLit "rhs_tclvl =") <+> ppr rhs_tclvl
279 , ptext (sLit "apply_mr =") <+> ppr apply_mr
280 , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
281 ]
282
283 -- Historical note: Before step 2 we used to have a
284 -- HORRIBLE HACK described in Note [Avoid unecessary
285 -- constraint simplification] but, as described in Trac
286 -- #4361, we have taken in out now. That's why we start
287 -- with step 2!
288
289 -- Step 2) First try full-blown solving
290
291 -- NB: we must gather up all the bindings from doing
292 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
293 -- And note that since there are nested implications,
294 -- calling solveWanteds will side-effect their evidence
295 -- bindings, so we can't just revert to the input
296 -- constraint.
297
298 ; ev_binds_var <- TcM.newTcEvBinds
299 ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $
300 runTcSWithEvBinds ev_binds_var (solveWanteds wanteds)
301 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
302
303 -- Step 4) Candidates for quantification are an approximation of wanted_transformed
304 -- NB: Already the fixpoint of any unifications that may have happened
305 -- NB: We do not do any defaulting when inferring a type, this can lead
306 -- to less polymorphic types, see Note [Default while Inferring]
307
308 ; tc_lcl_env <- TcRnMonad.getLclEnv
309 ; null_ev_binds_var <- TcM.newTcEvBinds
310 ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
311 ; quant_pred_candidates -- Fully zonked
312 <- if insolubleWC wanted_transformed_incl_derivs
313 then return [] -- See Note [Quantification with errors]
314 -- NB: must include derived errors in this test,
315 -- hence "incl_derivs"
316
317 else do { let quant_cand = approximateWC wanted_transformed
318 meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
319 ; gbl_tvs <- tcGetGlobalTyVars
320 -- Miminise quant_cand. We are not interested in any evidence
321 -- produced, because we are going to simplify wanted_transformed
322 -- again later. All we want here is the predicates over which to
323 -- quantify.
324 --
325 -- If any meta-tyvar unifications take place (unlikely), we'll
326 -- pick that up later.
327
328 ; WC { wc_simple = simples }
329 <- setTcLevel rhs_tclvl $
330 runTcSWithEvBinds null_ev_binds_var $
331 do { mapM_ (promoteAndDefaultTyVar rhs_tclvl gbl_tvs) meta_tvs
332 -- See Note [Promote _and_ default when inferring]
333 ; solveSimpleWanteds quant_cand }
334
335 ; return [ ctEvPred ev | ct <- bagToList simples
336 , let ev = ctEvidence ct
337 , isWanted ev ] }
338
339 -- NB: quant_pred_candidates is already fully zonked
340
341 -- Decide what type variables and constraints to quantify
342 ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
343 ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
344 ; (qtvs, bound_theta, mr_bites)
345 <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
346
347 -- Emit an implication constraint for the
348 -- remaining constraints from the RHS
349 ; bound_ev_vars <- mapM TcM.newEvVar bound_theta
350 ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty)
351 | (name, ty) <- name_taus ]
352 -- Don't add the quantified variables here, because
353 -- they are also bound in ic_skols and we want them
354 -- to be tidied uniformly
355
356 implic = Implic { ic_tclvl = rhs_tclvl
357 , ic_skols = qtvs
358 , ic_no_eqs = False
359 , ic_given = bound_ev_vars
360 , ic_wanted = wanted_transformed
361 , ic_status = IC_Unsolved
362 , ic_binds = ev_binds_var
363 , ic_info = skol_info
364 , ic_env = tc_lcl_env }
365 ; emitImplication implic
366
367 -- Promote any type variables that are free in the inferred type
368 -- of the function:
369 -- f :: forall qtvs. bound_theta => zonked_tau
370 -- These variables now become free in the envt, and hence will show
371 -- up whenever 'f' is called. They may currently at rhs_tclvl, but
372 -- they had better be unifiable at the outer_tclvl!
373 -- Example: envt mentions alpha[1]
374 -- tau_ty = beta[2] -> beta[2]
375 -- consraints = alpha ~ [beta]
376 -- we don't quantify over beta (since it is fixed by envt)
377 -- so we must promote it! The inferred type is just
378 -- f :: beta -> beta
379 ; outer_tclvl <- TcRnMonad.getTcLevel
380 ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV zonked_tau_tvs
381 -- decideQuantification turned some meta tyvars into
382 -- quantified skolems, so we have to zonk again
383 ; let phi_tvs = tyVarsOfTypes bound_theta `unionVarSet` zonked_tau_tvs
384 promote_tvs = varSetElems (closeOverKinds phi_tvs `delVarSetList` qtvs)
385 ; runTcSWithEvBinds null_ev_binds_var $ -- runTcS just to get the types right :-(
386 mapM_ (promoteTyVar outer_tclvl) promote_tvs
387
388 -- All done!
389 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
390 vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
391 , ptext (sLit "zonked_taus") <+> ppr zonked_taus
392 , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
393 , ptext (sLit "promote_tvs=") <+> ppr promote_tvs
394 , ptext (sLit "bound_theta =") <+> vcat [ ppr v <+> dcolon <+> ppr (idType v)
395 | v <- bound_ev_vars]
396 , ptext (sLit "mr_bites =") <+> ppr mr_bites
397 , ptext (sLit "qtvs =") <+> ppr qtvs
398 , ptext (sLit "implic =") <+> ppr implic ]
399
400 ; return ( qtvs, bound_ev_vars, mr_bites, TcEvBinds ev_binds_var) }
401
402 {-
403 ************************************************************************
404 * *
405 Quantification
406 * *
407 ************************************************************************
408
409 Note [Deciding quantification]
410 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
411 If the monomorphism restriction does not apply, then we quantify as follows:
412 * Take the global tyvars, and "grow" them using the equality constraints
413 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
414 happen because alpha is untouchable here) then do not quantify over
415 beta, because alpha fixes beta, and beta is effectively free in
416 the environment too
417 These are the mono_tvs
418
419 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
420 using all the constraints. These are tau_tvs_plus
421
422 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
423 careful to close over kinds, and to skolemise the quantified tyvars.
424 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
425 Result is qtvs.
426
427 * Filter the constraints using quantifyPred and the qtvs. We have to
428 zonk the constraints first, so they "see" the freshly created skolems.
429
430 If the MR does apply, mono_tvs includes all the constrained tyvars,
431 and the quantified constraints are empty.
432 -}
433
434 decideQuantification
435 :: Bool -- Apply monomorphism restriction
436 -> [PredType] -> TcTyVarSet -- Constraints and type variables from RHS
437 -> TcM ( [TcTyVar] -- Quantify over these tyvars (skolems)
438 , [PredType] -- and this context (fully zonked)
439 , Bool ) -- Did the MR bite?
440 -- See Note [Deciding quantification]
441 decideQuantification apply_mr constraints zonked_tau_tvs
442 | apply_mr -- Apply the Monomorphism restriction
443 = do { gbl_tvs <- tcGetGlobalTyVars
444 ; let constrained_tvs = tyVarsOfTypes constraints
445 mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
446 mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
447 ; qtvs <- quantifyTyVars mono_tvs zonked_tau_tvs
448 ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])
449 ; return (qtvs, [], mr_bites) }
450
451 | otherwise
452 = do { gbl_tvs <- tcGetGlobalTyVars
453 ; let mono_tvs = growThetaTyVars (filter isEqPred constraints) gbl_tvs
454 tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
455 ; qtvs <- quantifyTyVars mono_tvs tau_tvs_plus
456 ; constraints <- zonkTcThetaType constraints
457 -- quantifyTyVars turned some meta tyvars into
458 -- quantified skolems, so we have to zonk again
459
460 ; let theta = filter (quantifyPred (mkVarSet qtvs)) constraints
461 min_theta = mkMinimalBySCs theta -- See Note [Minimize by Superclasses]
462 ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
463 , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
464 ; return (qtvs, min_theta, False) }
465
466 ------------------
467 quantifyPred :: TyVarSet -- Quantifying over these
468 -> PredType -> Bool -- True <=> quantify over this wanted
469 -- This function decides whether a particular constraint shoudl be
470 -- quantified over, given the type variables that are being quantified
471 quantifyPred qtvs pred
472 = case classifyPredType pred of
473 ClassPred cls tys
474 | isIPClass cls -> True -- See note [Inheriting implicit parameters]
475 | otherwise -> tyVarsOfTypes tys `intersectsVarSet` qtvs
476
477 EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
478 -- representational equality is like a class constraint
479 EqPred ReprEq ty1 ty2 -> tyVarsOfTypes [ty1, ty2] `intersectsVarSet` qtvs
480
481 IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs
482 TuplePred {} -> False
483 where
484 -- See Note [Quantifying over equality constraints]
485 quant_fun ty
486 = case tcSplitTyConApp_maybe ty of
487 Just (tc, tys) | isTypeFamilyTyCon tc
488 -> tyVarsOfTypes tys `intersectsVarSet` qtvs
489 _ -> False
490
491 ------------------
492 growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
493 -- See Note [Growing the tau-tvs using constraints]
494 growThetaTyVars theta tvs
495 | null theta = tvs
496 | otherwise = transCloVarSet mk_next seed_tvs
497 where
498 seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips
499 (ips, non_ips) = partition isIPPred theta
500 -- See note [Inheriting implicit parameters]
501
502 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
503 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
504 grow_one so_far pred tvs
505 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
506 | otherwise = tvs
507 where
508 pred_tvs = tyVarsOfType pred
509
510 {-
511 Note [Quantifying over equality constraints]
512 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
513 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
514 Doing so may simply postpone a type error from the function definition site to
515 its call site. (At worst, imagine (Int ~ Bool)).
516
517 However, consider this
518 forall a. (F [a] ~ Int) => blah
519 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
520 site we will know 'a', and perhaps we have instance F [Bool] = Int.
521 So we *do* quantify over a type-family equality where the arguments mention
522 the quantified variables.
523
524 Note [Growing the tau-tvs using constraints]
525 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
526 (growThetaTyVars insts tvs) is the result of extending the set
527 of tyvars tvs using all conceivable links from pred
528
529 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
530 Then growThetaTyVars preds tvs = {a,b,c}
531
532 Notice that
533 growThetaTyVars is conservative if v might be fixed by vs
534 => v `elem` grow(vs,C)
535
536 Note [Inheriting implicit parameters]
537 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
538 Consider this:
539
540 f x = (x::Int) + ?y
541
542 where f is *not* a top-level binding.
543 From the RHS of f we'll get the constraint (?y::Int).
544 There are two types we might infer for f:
545
546 f :: Int -> Int
547
548 (so we get ?y from the context of f's definition), or
549
550 f :: (?y::Int) => Int -> Int
551
552 At first you might think the first was better, because then
553 ?y behaves like a free variable of the definition, rather than
554 having to be passed at each call site. But of course, the WHOLE
555 IDEA is that ?y should be passed at each call site (that's what
556 dynamic binding means) so we'd better infer the second.
557
558 BOTTOM LINE: when *inferring types* you must quantify over implicit
559 parameters, *even if* they don't mention the bound type variables.
560 Reason: because implicit parameters, uniquely, have local instance
561 declarations. See the predicate quantifyPred.
562
563 Note [Quantification with errors]
564 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
565 If we find that the RHS of the definition has some absolutely-insoluble
566 constraints, we abandon all attempts to find a context to quantify
567 over, and instead make the function fully-polymorphic in whatever
568 type we have found. For two reasons
569 a) Minimise downstream errors
570 b) Avoid spurious errors from this function
571
572 But NB that we must include *derived* errors in the check. Example:
573 (a::*) ~ Int#
574 We get an insoluble derived error *~#, and we don't want to discard
575 it before doing the isInsolubleWC test! (Trac #8262)
576
577 Note [Default while Inferring]
578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
579 Our current plan is that defaulting only happens at simplifyTop and
580 not simplifyInfer. This may lead to some insoluble deferred constraints
581 Example:
582
583 instance D g => C g Int b
584
585 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
586 type inferred = gamma -> gamma
587
588 Now, if we try to default (alpha := Int) we will be able to refine the implication to
589 (forall b. 0 => C gamma Int b)
590 which can then be simplified further to
591 (forall b. 0 => D gamma)
592 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
593 type: forall g. D g => g -> g
594
595 Instead what will currently happen is that we will get a quantified type
596 (forall g. g -> g) and an implication:
597 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
598
599 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
600 unsolvable implication:
601 forall g. 0 => (forall b. 0 => D g)
602
603 The concrete example would be:
604 h :: C g a s => g -> a -> ST s a
605 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
606
607 But it is quite tedious to do defaulting and resolve the implication constraints and
608 we have not observed code breaking because of the lack of defaulting in inference so
609 we don't do it for now.
610
611
612
613 Note [Minimize by Superclasses]
614 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
615 When we quantify over a constraint, in simplifyInfer we need to
616 quantify over a constraint that is minimal in some sense: For
617 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
618 we'd like to quantify over Ord alpha, because we can just get Eq alpha
619 from superclass selection from Ord alpha. This minimization is what
620 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
621 to check the original wanted.
622
623
624 Note [Avoid unecessary constraint simplification]
625 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
626 -------- NB NB NB (Jun 12) -------------
627 This note not longer applies; see the notes with Trac #4361.
628 But I'm leaving it in here so we remember the issue.)
629 ----------------------------------------
630 When inferring the type of a let-binding, with simplifyInfer,
631 try to avoid unnecessarily simplifying class constraints.
632 Doing so aids sharing, but it also helps with delicate
633 situations like
634
635 instance C t => C [t] where ..
636
637 f :: C [t] => ....
638 f x = let g y = ...(constraint C [t])...
639 in ...
640 When inferring a type for 'g', we don't want to apply the
641 instance decl, because then we can't satisfy (C t). So we
642 just notice that g isn't quantified over 't' and partition
643 the constraints before simplifying.
644
645 This only half-works, but then let-generalisation only half-works.
646
647
648 *********************************************************************************
649 * *
650 * Main Simplifier *
651 * *
652 ***********************************************************************************
653
654 Note [Deferring coercion errors to runtime]
655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 While developing, sometimes it is desirable to allow compilation to succeed even
657 if there are type errors in the code. Consider the following case:
658
659 module Main where
660
661 a :: Int
662 a = 'a'
663
664 main = print "b"
665
666 Even though `a` is ill-typed, it is not used in the end, so if all that we're
667 interested in is `main` it is handy to be able to ignore the problems in `a`.
668
669 Since we treat type equalities as evidence, this is relatively simple. Whenever
670 we run into a type mismatch in TcUnify, we normally just emit an error. But it
671 is always safe to defer the mismatch to the main constraint solver. If we do
672 that, `a` will get transformed into
673
674 co :: Int ~ Char
675 co = ...
676
677 a :: Int
678 a = 'a' `cast` co
679
680 The constraint solver would realize that `co` is an insoluble constraint, and
681 emit an error with `reportUnsolved`. But we can also replace the right-hand side
682 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
683 to compile, and it will run fine unless we evaluate `a`. This is what
684 `deferErrorsToRuntime` does.
685
686 It does this by keeping track of which errors correspond to which coercion
687 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
688 and does not fail if -fdefer-type-errors is on, so that we can continue
689 compilation. The errors are turned into warnings in `reportUnsolved`.
690 -}
691
692 solveWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
693 -- Simplify the input constraints
694 -- Discard the evidence binds
695 -- Discards all Derived stuff in result
696 -- Result is /not/ guaranteed zonked
697 solveWantedsTcM wanted
698 = do { (wanted1, _binds) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
699 ; return wanted1 }
700
701 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
702 -- Since solveWanteds returns the residual WantedConstraints,
703 -- it should always be called within a runTcS or something similar,
704 -- Result is not zonked
705 solveWantedsAndDrop wanted
706 = do { wc <- solveWanteds wanted
707 ; return (dropDerivedWC wc) }
708
709 solveWanteds :: WantedConstraints -> TcS WantedConstraints
710 -- so that the inert set doesn't mindlessly propagate.
711 -- NB: wc_simples may be wanted /or/ derived now
712 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
713 = do { traceTcS "solveWanteds {" (ppr wc)
714
715 -- Try the simple bit, including insolubles. Solving insolubles a
716 -- second time round is a bit of a waste; but the code is simple
717 -- and the program is wrong anyway, and we don't run the danger
718 -- of adding Derived insolubles twice; see
719 -- TcSMonad Note [Do not add duplicate derived insolubles]
720 ; wc1 <- solveSimpleWanteds simples
721 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
722
723 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
724
725 ; final_wc <- simpl_loop 0 floated_eqs
726 (WC { wc_simple = simples1, wc_impl = implics2
727 , wc_insol = insols `unionBags` insols1 })
728
729 ; bb <- getTcEvBindsMap
730 ; traceTcS "solveWanteds }" $
731 vcat [ text "final wc =" <+> ppr final_wc
732 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
733
734 ; return final_wc }
735
736 simpl_loop :: Int -> Cts
737 -> WantedConstraints
738 -> TcS WantedConstraints
739 simpl_loop n floated_eqs
740 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
741 | n > 10
742 = do { traceTcS "solveWanteds: loop!" (ppr wc); return wc }
743
744 | no_floated_eqs
745 = return wc -- Done!
746
747 | otherwise
748 = do { traceTcS "simpl_loop, iteration" (int n)
749
750 -- solveSimples may make progress if either float_eqs hold
751 ; (unifs_happened1, wc1) <- if no_floated_eqs
752 then return (False, emptyWC)
753 else reportUnifications $
754 solveSimpleWanteds (floated_eqs `unionBags` simples)
755 -- Put floated_eqs first so they get solved first
756 -- NB: the floated_eqs may include /derived/ equalities
757 -- arising from fundeps inside an implication
758
759 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
760
761 -- solveImplications may make progress only if unifs2 holds
762 ; (floated_eqs2, implics2) <- if not unifs_happened1 && isEmptyBag implics1
763 then return (emptyBag, implics)
764 else solveNestedImplications (implics `unionBags` implics1)
765
766 ; simpl_loop (n+1) floated_eqs2
767 (WC { wc_simple = simples1, wc_impl = implics2
768 , wc_insol = insols `unionBags` insols1 }) }
769
770 where
771 no_floated_eqs = isEmptyBag floated_eqs
772
773 solveNestedImplications :: Bag Implication
774 -> TcS (Cts, Bag Implication)
775 -- Precondition: the TcS inerts may contain unsolved simples which have
776 -- to be converted to givens before we go inside a nested implication.
777 solveNestedImplications implics
778 | isEmptyBag implics
779 = return (emptyBag, emptyBag)
780 | otherwise
781 = do { traceTcS "solveNestedImplications starting {" empty
782 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
783 ; let floated_eqs = concatBag floated_eqs_s
784
785 -- ... and we are back in the original TcS inerts
786 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
787 -- them in the beginning of this function.
788 ; traceTcS "solveNestedImplications end }" $
789 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
790 , text "unsolved_implics =" <+> ppr unsolved_implics ]
791
792 ; return (floated_eqs, catBagMaybes unsolved_implics) }
793
794 solveImplication :: Implication -- Wanted
795 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
796 Maybe Implication) -- Simplified implication (empty or singleton)
797 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
798 -- which after trying to solve this implication we must restore to their original value
799 solveImplication imp@(Implic { ic_tclvl = tclvl
800 , ic_binds = ev_binds
801 , ic_skols = skols
802 , ic_given = givens
803 , ic_wanted = wanteds
804 , ic_info = info
805 , ic_status = status
806 , ic_env = env })
807 | IC_Solved {} <- status
808 = return (emptyCts, Just imp) -- Do nothing
809
810 | otherwise -- Even for IC_Insoluble it is worth doing more work
811 -- The insoluble stuff might be in one sub-implication
812 -- and other unsolved goals in another; and we want to
813 -- solve the latter as much as possible
814 = do { inerts <- getTcSInerts
815 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
816
817 -- Solve the nested constraints
818 ; (no_given_eqs, given_insols, residual_wanted)
819 <- nestImplicTcS ev_binds tclvl $
820 do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens
821 ; no_eqs <- getNoGivenEqs tclvl skols
822
823 ; residual_wanted <- solveWanteds wanteds
824 -- solveWanteds, *not* solveWantedsAndDrop, because
825 -- we want to retain derived equalities so we can float
826 -- them out in floatEqualities
827
828 ; return (no_eqs, given_insols, residual_wanted) }
829
830 ; (floated_eqs, residual_wanted)
831 <- floatEqualities skols no_given_eqs residual_wanted
832
833 ; let final_wanted = residual_wanted `addInsols` given_insols
834
835 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
836 , ic_wanted = final_wanted })
837
838 ; evbinds <- getTcEvBindsMap
839 ; traceTcS "solveImplication end }" $ vcat
840 [ text "no_given_eqs =" <+> ppr no_given_eqs
841 , text "floated_eqs =" <+> ppr floated_eqs
842 , text "res_implic =" <+> ppr res_implic
843 , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
844
845 ; return (floated_eqs, res_implic) }
846
847 ----------------------
848 setImplicationStatus :: Implication -> TcS (Maybe Implication)
849 -- Finalise the implication returned from solveImplication:
850 -- * Set the ic_status field
851 -- * Trim the ic_wanted field to remove Derived constraints
852 -- Return Nothing if we can discard the implication altogether
853 setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _
854 , ic_info = info
855 , ic_wanted = wc
856 , ic_given = givens })
857 | some_insoluble
858 = return $ Just $
859 implic { ic_status = IC_Insoluble
860 , ic_wanted = wc { wc_simple = pruned_simples
861 , wc_insol = pruned_insols } }
862
863 | some_unsolved
864 = return $ Just $
865 implic { ic_status = IC_Unsolved
866 , ic_wanted = wc { wc_simple = pruned_simples
867 , wc_insol = pruned_insols } }
868
869 | otherwise -- Everything is solved; look at the implications
870 -- See Note [Tracking redundant constraints]
871 = do { ev_binds <- TcS.readTcRef ev_binds_var
872 ; let all_needs = neededEvVars ev_binds implic_needs
873
874 dead_givens | warnRedundantGivens info
875 = filterOut (`elemVarSet` all_needs) givens
876 | otherwise = [] -- None to report
877
878 final_needs = all_needs `delVarSetList` givens
879
880 discard_entire_implication -- Can we discard the entire implication?
881 = null dead_givens -- No warning from this implication
882 && isEmptyBag pruned_implics -- No live children
883 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
884
885 final_status = IC_Solved { ics_need = final_needs
886 , ics_dead = dead_givens }
887 final_implic = implic { ic_status = final_status
888 , ic_wanted = wc { wc_simple = pruned_simples
889 , wc_insol = pruned_insols
890 , wc_impl = pruned_implics } }
891 -- We can only prune the child implications (pruned_implics)
892 -- in the IC_Solved status case, because only then we can
893 -- accumulate their needed evidence variales into the
894 -- IC_Solved final_status field of the parent implication.
895
896 ; return $ if discard_entire_implication
897 then Nothing
898 else Just final_implic }
899 where
900 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
901
902 some_insoluble = insolubleWC wc
903 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
904 || isNothing mb_implic_needs
905
906 pruned_simples = dropDerivedSimples simples
907 pruned_insols = dropDerivedInsols insols
908 pruned_implics = filterBag need_to_keep_implic implics
909
910 mb_implic_needs :: Maybe VarSet
911 -- Just vs => all implics are IC_Solved, with 'vs' needed
912 -- Nothing => at least one implic is not IC_Solved
913 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
914 Just implic_needs = mb_implic_needs
915
916 add_implic implic acc
917 | Just vs_acc <- acc
918 , IC_Solved { ics_need = vs } <- ic_status implic
919 = Just (vs `unionVarSet` vs_acc)
920 | otherwise = Nothing
921
922 need_to_keep_implic ic
923 | IC_Solved { ics_dead = [] } <- ic_status ic
924 -- Fully solved, and no redundant givens to report
925 , isEmptyBag (wc_impl (ic_wanted ic))
926 -- And no children that might have things to report
927 = False
928 | otherwise
929 = True
930
931 warnRedundantGivens :: SkolemInfo -> Bool
932 warnRedundantGivens (SigSkol ctxt _)
933 = case ctxt of
934 FunSigCtxt _ warn_redundant -> warn_redundant
935 ExprSigCtxt -> True
936 _ -> False
937 warnRedundantGivens InstSkol = True
938 warnRedundantGivens _ = False
939
940 neededEvVars :: EvBindMap -> VarSet -> VarSet
941 -- Find all the evidence variables that are "needed",
942 -- and then delete all those bound by the evidence bindings
943 -- A variable is "needed" if
944 -- a) it is free in the RHS of a Wanted EvBind (add_wanted)
945 -- b) it is free in the RHS of an EvBind whose LHS is needed (transClo)
946 -- c) it is in the ic_need_evs of a nested implication (initial_seeds)
947 -- (after removing the givens)
948 neededEvVars ev_binds initial_seeds
949 = needed `minusVarSet` bndrs
950 where
951 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
952 needed = transCloVarSet also_needs seeds
953 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
954
955 add_wanted :: EvBind -> VarSet -> VarSet
956 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
957 | is_given = needs -- Add the rhs vars of the Wanted bindings only
958 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
959
960 also_needs :: VarSet -> VarSet
961 also_needs needs
962 = foldVarSet add emptyVarSet needs
963 where
964 add v needs
965 | Just ev_bind <- lookupEvBind ev_binds v
966 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
967 , is_given
968 = evVarsOfTerm rhs `unionVarSet` needs
969 | otherwise
970 = needs
971
972 add_bndr :: EvBind -> VarSet -> VarSet
973 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
974
975
976 {-
977 Note [Tracking redundant constraints]
978 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
979 With Opt_WarnRedundantConstraints, GHC can report which
980 constraints of a type signature (or instance declaration) are
981 redundant, and can be omitted. Here is an overview of how it
982 works:
983
984 ----- What is a redudant constraint?
985
986 * The things that can be redundant are precisely the Given
987 constraints of an implication.
988
989 * A constraint can be redundant in two different ways:
990 a) It is implied by other givens. E.g.
991 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
992 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
993 b) It is not needed by the Wanted constraints covered by the
994 implication E.g.
995 f :: Eq a => a -> Bool
996 f x = True -- Equality not uesd
997
998 * To find (a), when we have two Given constraints,
999 we must be careful to drop the one that is a naked variable (if poss).
1000 So if we have
1001 f :: (Eq a, Ord a) => blah
1002 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1003 [G] d2 :: Eq a
1004 We want to discard d2 in favour of the superclass selection from
1005 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1006 See Note [Replacement vs keeping].
1007
1008 * To find (b) we need to know which evidence bindings are 'wanted';
1009 hence the eb_is_given field on an EvBind.
1010
1011 ----- How tracking works
1012
1013 * When the constraint solver finishes solving all the wanteds in
1014 an implication, it sets its status to IC_Solved
1015
1016 - The ics_dead field of IC_Solved records the subset of the ic_given
1017 of this implication that are redundant (not needed).
1018
1019 - The ics_need field of IC_Solved then records all the
1020 in-scope (given) evidence variables, bound by the context, that
1021 were needed to solve this implication, including all its nested
1022 implications. (We remove the ic_given of this implication from
1023 the set, of course.)
1024
1025 * We compute which evidence variables are needed by an implication
1026 in setImplicationStatus. A variable is needed if
1027 a) it is free in the RHS of a Wanted EvBind
1028 b) it is free in the RHS of an EvBind whose LHS is needed
1029 c) it is in the ics_need of a nested implication
1030
1031 * We need to be careful not to discard an implication
1032 prematurely, even one that is fully solved, because we might
1033 thereby forget which variables it needs, and hence wrongly
1034 report a constraint as redundant. But we can discard it once
1035 its free vars have been incorporated into its parent; or if it
1036 simply has no free vars. This careful discarding is also
1037 handled in setImplicationStatus
1038
1039 ----- Reporting redundant constraints
1040
1041 * TcErrors does the actual warning, in warnRedundantConstraints.
1042
1043 * We don't report redundant givens for *every* implication; only
1044 for those which reply True to TcSimplify.warnRedundantGivens:
1045
1046 - For example, in a class declaration, the default method *can*
1047 use the class constraint, but it certainly doesn't *have* to,
1048 and we don't want to report an error there.
1049
1050 - More subtly, in a function definition
1051 f :: (Ord a, Ord a, Ix a) => a -> a
1052 f x = rhs
1053 we do an ambiguity check on the type (which would find that one
1054 of the Ord a constraints was redundant), and then we check that
1055 the definition has that type (which might find that both are
1056 redundant). We don't want to report the same error twice, so
1057 we disable it for the ambiguity check. Hence the flag in
1058 TcType.FunSigCtxt.
1059
1060 This decision is taken in setImplicationStatus, rather than TcErrors
1061 so that we can discard implication constraints that we don't need.
1062 So ics_dead consists only of the *reportable* redundant givens.
1063
1064 ----- Shortcomings
1065
1066 Consider (see Trac #9939)
1067 f2 :: (Eq a, Ord a) => a -> a -> Bool
1068 -- Ord a redundant, but Eq a is reported
1069 f2 x y = (x == y)
1070
1071 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1072 really not easy to detect that!
1073
1074
1075 Note [Cutting off simpl_loop]
1076 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1077 It is very important not to iterate in simpl_loop unless there is a chance
1078 of progress. Trac #8474 is a classic example:
1079
1080 * There's a deeply-nested chain of implication constraints.
1081 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1082
1083 * From the innermost one we get a [D] alpha ~ Int,
1084 but alpha is untouchable until we get out to the outermost one
1085
1086 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1087 is untouchable, the solveInteract in simpl_loop makes no progress
1088
1089 * So there is no point in attempting to re-solve
1090 ?yn:betan => [W] ?x:Int
1091 because we'll just get the same [D] again
1092
1093 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1094 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1095 exponentially many) iterations!
1096
1097 Conclusion: we should iterate simpl_loop iff we will get more 'givens'
1098 in the inert set when solving the nested implications. That is the
1099 result of prepareInertsForImplications is larger. How can we tell
1100 this?
1101
1102 Consider floated_eqs (all wanted or derived):
1103
1104 (a) [W/D] CTyEqCan (a ~ ty). This can give rise to a new given only by causing
1105 a unification. So we count those unifications.
1106
1107 (b) [W] CFunEqCan (F tys ~ xi). Even though these are wanted, they
1108 are pushed in as givens by prepareInertsForImplications. See Note
1109 [Preparing inert set for implications] in TcSMonad. But because
1110 of that very fact, we won't generate another copy if we iterate
1111 simpl_loop. So we iterate if there any of these
1112 -}
1113
1114 promoteTyVar :: TcLevel -> TcTyVar -> TcS TcTyVar
1115 -- When we float a constraint out of an implication we must restore
1116 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1117 -- See Note [Promoting unification variables]
1118 promoteTyVar tclvl tv
1119 | isFloatedTouchableMetaTyVar tclvl tv
1120 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1121 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1122 ; unifyTyVar tv (mkTyVarTy rhs_tv)
1123 ; return rhs_tv }
1124 | otherwise
1125 = return tv
1126
1127 promoteAndDefaultTyVar :: TcLevel -> TcTyVarSet -> TcTyVar -> TcS TcTyVar
1128 -- See Note [Promote _and_ default when inferring]
1129 promoteAndDefaultTyVar tclvl gbl_tvs tv
1130 = do { tv1 <- if tv `elemVarSet` gbl_tvs
1131 then return tv
1132 else defaultTyVar tv
1133 ; promoteTyVar tclvl tv1 }
1134
1135 defaultTyVar :: TcTyVar -> TcS TcTyVar
1136 -- Precondition: MetaTyVars only
1137 -- See Note [DefaultTyVar]
1138 defaultTyVar the_tv
1139 | Just default_k <- defaultKind_maybe (tyVarKind the_tv)
1140 = do { tv' <- TcS.cloneMetaTyVar the_tv
1141 ; let new_tv = setTyVarKind tv' default_k
1142 ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
1143 ; unifyTyVar the_tv (mkTyVarTy new_tv)
1144 ; return new_tv }
1145 -- Why not directly derived_pred = mkTcEqPred k default_k?
1146 -- See Note [DefaultTyVar]
1147 -- We keep the same TcLevel on tv'
1148
1149 | otherwise = return the_tv -- The common case
1150
1151 approximateWC :: WantedConstraints -> Cts
1152 -- Postcondition: Wanted or Derived Cts
1153 -- See Note [ApproximateWC]
1154 approximateWC wc
1155 = float_wc emptyVarSet wc
1156 where
1157 float_wc :: TcTyVarSet -> WantedConstraints -> Cts
1158 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1159 = filterBag is_floatable simples `unionBags`
1160 do_bag (float_implic new_trapping_tvs) implics
1161 where
1162 is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs
1163 new_trapping_tvs = transCloVarSet grow trapping_tvs
1164
1165 grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
1166 grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
1167 grow_one so_far ct tvs
1168 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
1169 | otherwise = tvs
1170 where
1171 ct_tvs = tyVarsOfCt ct
1172
1173 float_implic :: TcTyVarSet -> Implication -> Cts
1174 float_implic trapping_tvs imp
1175 | ic_no_eqs imp -- No equalities, so float
1176 = float_wc new_trapping_tvs (ic_wanted imp)
1177 | otherwise -- Don't float out of equalities
1178 = emptyCts -- See Note [ApproximateWC]
1179 where
1180 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1181 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1182 do_bag f = foldrBag (unionBags.f) emptyBag
1183
1184 {-
1185 Note [ApproximateWC]
1186 ~~~~~~~~~~~~~~~~~~~~
1187 approximateWC takes a constraint, typically arising from the RHS of a
1188 let-binding whose type we are *inferring*, and extracts from it some
1189 *simple* constraints that we might plausibly abstract over. Of course
1190 the top-level simple constraints are plausible, but we also float constraints
1191 out from inside, if they are not captured by skolems.
1192
1193 The same function is used when doing type-class defaulting (see the call
1194 to applyDefaultingRules) to extract constraints that that might be defaulted.
1195
1196 There are two caveats:
1197
1198 1. We do *not* float anything out if the implication binds equality
1199 constraints, because that defeats the OutsideIn story. Consider
1200 data T a where
1201 TInt :: T Int
1202 MkT :: T a
1203
1204 f TInt = 3::Int
1205
1206 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1207 f :: T a -> res
1208 We don't want to float (res~Int) out because then we'll infer
1209 f :: T a -> Int
1210 which is only on of the possible types. (GHC 7.6 accidentally *did*
1211 float out of such implications, which meant it would happily infer
1212 non-principal types.)
1213
1214 2. We do not float out an inner constraint that shares a type variable
1215 (transitively) with one that is trapped by a skolem. Eg
1216 forall a. F a ~ beta, Integral beta
1217 We don't want to float out (Integral beta). Doing so would be bad
1218 when defaulting, because then we'll default beta:=Integer, and that
1219 makes the error message much worse; we'd get
1220 Can't solve F a ~ Integer
1221 rather than
1222 Can't solve Integral (F a)
1223
1224 Moreover, floating out these "contaminated" constraints doesn't help
1225 when generalising either. If we generalise over (Integral b), we still
1226 can't solve the retained implication (forall a. F a ~ b). Indeed,
1227 arguably that too would be a harder error to understand.
1228
1229 Note [DefaultTyVar]
1230 ~~~~~~~~~~~~~~~~~~~
1231 defaultTyVar is used on any un-instantiated meta type variables to
1232 default the kind of OpenKind and ArgKind etc to *. This is important
1233 to ensure that instance declarations match. For example consider
1234
1235 instance Show (a->b)
1236 foo x = show (\_ -> True)
1237
1238 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1239 and that won't match the typeKind (*) in the instance decl. See tests
1240 tc217 and tc175.
1241
1242 We look only at touchable type variables. No further constraints
1243 are going to affect these type variables, so it's time to do it by
1244 hand. However we aren't ready to default them fully to () or
1245 whatever, because the type-class defaulting rules have yet to run.
1246
1247 An important point is that if the type variable tv has kind k and the
1248 default is default_k we do not simply generate [D] (k ~ default_k) because:
1249
1250 (1) k may be ArgKind and default_k may be * so we will fail
1251
1252 (2) We need to rewrite all occurrences of the tv to be a type
1253 variable with the right kind and we choose to do this by rewriting
1254 the type variable /itself/ by a new variable which does have the
1255 right kind.
1256
1257 Note [Promote _and_ default when inferring]
1258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1259 When we are inferring a type, we simplify the constraint, and then use
1260 approximateWC to produce a list of candidate constraints. Then we MUST
1261
1262 a) Promote any meta-tyvars that have been floated out by
1263 approximateWC, to restore invariant (MetaTvInv) described in
1264 Note [TcLevel and untouchable type variables] in TcType.
1265
1266 b) Default the kind of any meta-tyyvars that are not mentioned in
1267 in the environment.
1268
1269 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1270 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1271 should! If we don't solve the constraint, we'll stupidly quantify over
1272 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1273 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1274 Trac #7641 is a simpler example.
1275
1276 Note [Promoting unification variables]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 When we float an equality out of an implication we must "promote" free
1279 unification variables of the equality, in order to maintain Invariant
1280 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1281 leftover implication.
1282
1283 This is absolutely necessary. Consider the following example. We start
1284 with two implications and a class with a functional dependency.
1285
1286 class C x y | x -> y
1287 instance C [a] [a]
1288
1289 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1290 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1291
1292 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1293 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1294 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1295 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1296 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1297
1298 class C x y | x -> y where
1299 op :: x -> y -> ()
1300
1301 instance C [a] [a]
1302
1303 type family F a :: *
1304
1305 h :: F Int -> ()
1306 h = undefined
1307
1308 data TEx where
1309 TEx :: a -> TEx
1310
1311 f (x::beta) =
1312 let g1 :: forall b. b -> ()
1313 g1 _ = h [x]
1314 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1315 in (g1 '3', g2 undefined)
1316
1317
1318 Note [Solving Family Equations]
1319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1320 After we are done with simplification we may be left with constraints of the form:
1321 [Wanted] F xis ~ beta
1322 If 'beta' is a touchable unification variable not already bound in the TyBinds
1323 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1324
1325 When is it ok to do so?
1326 1) 'beta' must not already be defaulted to something. Example:
1327
1328 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1329 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1330 have to report this as unsolved.
1331
1332 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1333 set [beta := F xis] only if beta is not among the free variables of xis.
1334
1335 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1336 of type family equations. See Inert Set invariants in TcInteract.
1337
1338 This solving is now happening during zonking, see Note [Unflattening while zonking]
1339 in TcMType.
1340
1341
1342 *********************************************************************************
1343 * *
1344 * Floating equalities *
1345 * *
1346 *********************************************************************************
1347
1348 Note [Float Equalities out of Implications]
1349 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1350 For ordinary pattern matches (including existentials) we float
1351 equalities out of implications, for instance:
1352 data T where
1353 MkT :: Eq a => a -> T
1354 f x y = case x of MkT _ -> (y::Int)
1355 We get the implication constraint (x::T) (y::alpha):
1356 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1357 We want to float out the equality into a scope where alpha is no
1358 longer untouchable, to solve the implication!
1359
1360 But we cannot float equalities out of implications whose givens may
1361 yield or contain equalities:
1362
1363 data T a where
1364 T1 :: T Int
1365 T2 :: T Bool
1366 T3 :: T a
1367
1368 h :: T a -> a -> Int
1369
1370 f x y = case x of
1371 T1 -> y::Int
1372 T2 -> y::Bool
1373 T3 -> h x y
1374
1375 We generate constraint, for (x::T alpha) and (y :: beta):
1376 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1377 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1378 (alpha ~ beta) -- From 3rd branch
1379
1380 If we float the equality (beta ~ Int) outside of the first implication and
1381 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1382 But if we just leave them inside the implications we unify alpha := beta and
1383 solve everything.
1384
1385 Principle:
1386 We do not want to float equalities out which may
1387 need the given *evidence* to become soluble.
1388
1389 Consequence: classes with functional dependencies don't matter (since there is
1390 no evidence for a fundep equality), but equality superclasses do matter (since
1391 they carry evidence).
1392 -}
1393
1394 floatEqualities :: [TcTyVar] -> Bool
1395 -> WantedConstraints
1396 -> TcS (Cts, WantedConstraints)
1397 -- Main idea: see Note [Float Equalities out of Implications]
1398 --
1399 -- Precondition: the wc_simple of the incoming WantedConstraints are
1400 -- fully zonked, so that we can see their free variables
1401 --
1402 -- Postcondition: The returned floated constraints (Cts) are only
1403 -- Wanted or Derived and come from the input wanted
1404 -- ev vars or deriveds
1405 --
1406 -- Also performs some unifications (via promoteTyVar), adding to
1407 -- monadically-carried ty_binds. These will be used when processing
1408 -- floated_eqs later
1409 --
1410 -- Subtleties: Note [Float equalities from under a skolem binding]
1411 -- Note [Skolem escape]
1412 floatEqualities skols no_given_eqs wanteds@(WC { wc_simple = simples })
1413 | not no_given_eqs -- There are some given equalities, so don't float
1414 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1415 | otherwise
1416 = do { outer_tclvl <- TcS.getTcLevel
1417 ; mapM_ (promoteTyVar outer_tclvl) (varSetElems (tyVarsOfCts float_eqs))
1418 -- See Note [Promoting unification variables]
1419 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1420 , text "Simples =" <+> ppr simples
1421 , text "Floated eqs =" <+> ppr float_eqs ])
1422 ; return (float_eqs, wanteds { wc_simple = remaining_simples }) }
1423 where
1424 skol_set = mkVarSet skols
1425 (float_eqs, remaining_simples) = partitionBag (usefulToFloat is_useful) simples
1426 is_useful pred = tyVarsOfType pred `disjointVarSet` skol_set
1427
1428 {- Note [Float equalities from under a skolem binding]
1429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1430 Which of the simple equalities can we float out? Obviously, only
1431 ones that don't mention the skolem-bound variables. But that is
1432 over-eager. Consider
1433 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1434 The second constraint doesn't mention 'a'. But if we float it
1435 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1436 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1437 we left with the constraint
1438 [2] forall a. a ~ gamma'[1]
1439 which is insoluble because gamma became untouchable.
1440
1441 Solution: float only constraints that stand a jolly good chance of
1442 being soluble simply by being floated, namely ones of form
1443 a ~ ty
1444 where 'a' is a currently-untouchable unification variable, but may
1445 become touchable by being floated (perhaps by more than one level).
1446
1447 We had a very complicated rule previously, but this is nice and
1448 simple. (To see the notes, look at this Note in a version of
1449 TcSimplify prior to Oct 2014).
1450
1451 Note [Skolem escape]
1452 ~~~~~~~~~~~~~~~~~~~~
1453 You might worry about skolem escape with all this floating.
1454 For example, consider
1455 [2] forall a. (a ~ F beta[2] delta,
1456 Maybe beta[2] ~ gamma[1])
1457
1458 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1459 solve with gamma := beta. But what if later delta:=Int, and
1460 F b Int = b.
1461 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1462 skolem has escaped!
1463
1464 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1465 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1466
1467
1468 *********************************************************************************
1469 * *
1470 * Defaulting and disamgiguation *
1471 * *
1472 *********************************************************************************
1473 -}
1474
1475 applyDefaultingRules :: WantedConstraints -> TcS Bool
1476 -- True <=> I did some defaulting, by unifying a meta-tyvar
1477 -- Imput WantedConstraints are not necessarily zonked
1478
1479 applyDefaultingRules wanteds
1480 | isEmptyWC wanteds
1481 = return False
1482 | otherwise
1483 = do { info@(default_tys, _) <- getDefaultInfo
1484 ; wanteds <- TcS.zonkWC wanteds
1485
1486 ; let groups = findDefaultableGroups info wanteds
1487
1488 ; traceTcS "applyDefaultingRules {" $
1489 vcat [ text "wanteds =" <+> ppr wanteds
1490 , text "groups =" <+> ppr groups
1491 , text "info =" <+> ppr info ]
1492
1493 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1494
1495 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1496
1497 ; return (or something_happeneds) }
1498
1499 findDefaultableGroups
1500 :: ( [Type]
1501 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1502 -> WantedConstraints -- Unsolved (wanted or derived)
1503 -> [(TyVar, [Ct])]
1504 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1505 | null default_tys
1506 = []
1507 | otherwise
1508 = [ (tv, map fstOf3 group)
1509 | group@((_,_,tv):_) <- unary_groups
1510 , defaultable_tyvar tv
1511 , defaultable_classes (map sndOf3 group) ]
1512 where
1513 simples = approximateWC wanteds
1514 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
1515 unary_groups = equivClasses cmp_tv unaries
1516
1517 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
1518 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
1519 non_unaries :: [Ct] -- and *other* constraints
1520
1521 -- Finds unary type-class constraints
1522 -- But take account of polykinded classes like Typeable,
1523 -- which may look like (Typeable * (a:*)) (Trac #8931)
1524 find_unary cc
1525 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
1526 , Just (kinds, ty) <- snocView tys -- Ignore kind arguments
1527 , all isKind kinds -- for this purpose
1528 , Just tv <- tcGetTyVar_maybe ty
1529 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
1530 -- we definitely don't want to try to assign to those!
1531 = Left (cc, cls, tv)
1532 find_unary cc = Right cc -- Non unary or non dictionary
1533
1534 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1535 bad_tvs = mapUnionVarSet tyVarsOfCt non_unaries
1536
1537 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1538
1539 defaultable_tyvar tv
1540 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1541 b2 = not (tv `elemVarSet` bad_tvs)
1542 in b1 && b2
1543
1544 defaultable_classes clss
1545 | extended_defaults = any isInteractiveClass clss
1546 | otherwise = all is_std_class clss && (any is_num_class clss)
1547
1548 -- In interactive mode, or with -XExtendedDefaultRules,
1549 -- we default Show a to Show () to avoid graututious errors on "show []"
1550 isInteractiveClass cls
1551 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1552
1553 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1554 -- is_num_class adds IsString to the standard numeric classes,
1555 -- when -foverloaded-strings is enabled
1556
1557 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1558 -- Similarly is_std_class
1559
1560 ------------------------------
1561 disambigGroup :: [Type] -- The default types
1562 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
1563 -- sharing same type variable
1564 -> TcS Bool -- True <=> something happened, reflected in ty_binds
1565
1566 disambigGroup [] _
1567 = return False
1568 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
1569 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
1570 ; fake_ev_binds_var <- TcS.newTcEvBinds
1571 ; tclvl <- TcS.getTcLevel
1572 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl)
1573 try_group
1574
1575 ; if success then
1576 -- Success: record the type variable binding, and return
1577 do { unifyTyVar the_tv default_ty
1578 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
1579 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
1580 ; return True }
1581 else
1582 -- Failure: try with the next type
1583 do { traceTcS "disambigGroup failed, will try other default types }"
1584 (ppr default_ty)
1585 ; disambigGroup default_tys group } }
1586 where
1587 try_group
1588 | Just subst <- mb_subst
1589 = do { wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
1590 wanteds
1591 ; residual_wanted <- solveSimpleWanteds $ listToBag $
1592 map mkNonCanonical wanted_evs
1593 ; return (isEmptyWC residual_wanted) }
1594 | otherwise
1595 = return False
1596
1597 tmpl_tvs = extendVarSet (tyVarsOfType (tyVarKind the_tv)) the_tv
1598 mb_subst = tcMatchTy tmpl_tvs (mkTyVarTy the_tv) default_ty
1599 -- Make sure the kinds match too; hence this call to tcMatchTy
1600 -- E.g. suppose the only constraint was (Typeable k (a::k))
1601
1602 loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
1603 , ctl_env = panic "disambigGroup:env"
1604 , ctl_depth = initialSubGoalDepth }
1605
1606 {-
1607 Note [Avoiding spurious errors]
1608 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1609 When doing the unification for defaulting, we check for skolem
1610 type variables, and simply don't default them. For example:
1611 f = (*) -- Monomorphic
1612 g :: Num a => a -> a
1613 g x = f x x
1614 Here, we get a complaint when checking the type signature for g,
1615 that g isn't polymorphic enough; but then we get another one when
1616 dealing with the (Num a) context arising from f's definition;
1617 we try to unify a with Int (to default it), but find that it's
1618 already been unified with the rigid variable from g's type sig
1619 -}