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