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