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