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