Merge branch 'master' of darcs.haskell.org:/home/darcs/ghc
[ghc.git] / compiler / typecheck / TcSimplify.lhs
1 \begin{code}
2 {-# OPTIONS -fno-warn-tabs #-}
3 -- The above warning supression flag is a temporary kludge.
4 -- While working on this module you are encouraged to remove it and
5 -- detab the module (please do the detabbing in a separate patch). See
6 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
7 -- for details
8
9 module TcSimplify( 
10        simplifyInfer, simplifyAmbiguityCheck,
11        simplifyDefault, simplifyDeriv, 
12        simplifyRule, simplifyTop, simplifyInteractive
13   ) where
14
15 #include "HsVersions.h"
16
17 import TcRnMonad
18 import TcErrors
19 import TcMType
20 import TcType 
21 import TcSMonad 
22 import TcInteract 
23 import Inst
24 import Unify    ( niFixTvSubst, niSubstTvSet )
25 import Type     ( classifyPredType, PredTree(..), isIPPred_maybe )
26 import Var
27 import Unique
28 import VarSet
29 import VarEnv 
30 import TcEvidence
31 import TypeRep
32 import Name
33 import Bag
34 import ListSetOps
35 import Util
36 import PrelInfo
37 import PrelNames
38 import Class            ( classKey )
39 import BasicTypes       ( RuleName )
40 import Control.Monad    ( when )
41 import Outputable
42 import FastString
43 import TrieMap () -- DV: for now
44 import DynFlags
45 import Data.Maybe ( mapMaybe )
46 \end{code}
47
48
49 *********************************************************************************
50 *                                                                               * 
51 *                           External interface                                  *
52 *                                                                               *
53 *********************************************************************************
54
55
56 \begin{code}
57
58
59 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
60 -- Simplify top-level constraints
61 -- Usually these will be implications,
62 -- but when there is nothing to quantify we don't wrap
63 -- in a degenerate implication, so we do that here instead
64 simplifyTop wanteds 
65   = do { ev_binds_var <- newTcEvBinds
66                          
67        ; zonked_wanteds <- zonkWC wanteds
68        ; wc_first_go <- runTcSWithEvBinds ev_binds_var $ solveWanteds zonked_wanteds
69        ; cts <- applyTyVarDefaulting wc_first_go 
70                 -- See Note [Top-level Defaulting Plan]
71                 
72        ; let wc_for_loop = wc_first_go { wc_flat = wc_flat wc_first_go `unionBags` cts }
73                            
74        ; traceTc "simpl_top_loop {" $ text "zonked_wc =" <+> ppr zonked_wanteds
75        ; simpl_top_loop ev_binds_var wc_for_loop }
76     
77   where simpl_top_loop ev_binds_var wc
78           | isEmptyWC wc 
79           = do { traceTc "simpl_top_loop }" empty
80                ; TcRnMonad.getTcEvBinds ev_binds_var }
81           | otherwise
82           = do { wc_residual <- runTcSWithEvBinds ev_binds_var $ solveWanteds wc
83                ; let wc_flat_approximate = approximateWC wc_residual
84                ; (dflt_eqs,_unused_bind) <- runTcS $
85                                             applyDefaultingRules wc_flat_approximate
86                                             -- See Note [Top-level Defaulting Plan]
87                ; if isEmptyBag dflt_eqs then 
88                    do { traceTc "simpl_top_loop }" empty
89                       ; report_and_finish ev_binds_var wc_residual }
90                  else
91                    simpl_top_loop ev_binds_var $ 
92                    wc_residual { wc_flat = wc_flat wc_residual `unionBags` dflt_eqs } }
93
94         report_and_finish ev_binds_var wc_residual 
95           = do { eb1 <- TcRnMonad.getTcEvBinds ev_binds_var
96                ; traceTc "reportUnsolved {" empty
97                    -- See Note [Deferring coercion errors to runtime]
98                ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
99                ; eb2 <- reportUnsolved runtimeCoercionErrors wc_residual
100                ; traceTc "reportUnsolved }" empty
101                ; return (eb1 `unionBags` eb2) }
102 \end{code}
103
104 Note [Top-level Defaulting Plan]
105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
106
107 We have considered two design choices for where/when to apply defaulting.   
108    (i) Do it in SimplCheck mode only /whenever/ you try to solve some 
109        flat constraints, maybe deep inside the context of implications.
110        This used to be the case in GHC 7.4.1.
111    (ii) Do it in a tight loop at simplifyTop, once all other constraint has 
112         finished. This is the current story.
113
114 Option (i) had many disadvantages: 
115    a) First it was deep inside the actual solver, 
116    b) Second it was dependent on the context (Infer a type signature, 
117       or Check a type signature, or Interactive) since we did not want 
118       to always start defaulting when inferring (though there is an exception to  
119       this see Note [Default while Inferring])
120    c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
121           f :: Int -> Bool
122           f x = const True (\y -> let w :: a -> a
123                                       w a = const a (y+1)
124                                   in w y)
125       We will get an implication constraint (for beta the type of y):
126                [untch=beta] forall a. 0 => Num beta
127       which we really cannot default /while solving/ the implication, since beta is
128       untouchable.
129
130 Instead our new defaulting story is to pull defaulting out of the solver loop and
131 go with option (i), implemented at SimplifyTop. Namely:
132      - First have a go at solving the residual constraint of the whole program
133      - Try to approximate it with a flat constraint
134      - Figure out derived defaulting equations for that flat constraint
135      - Go round the loop again if you did manage to get some equations
136
137 Now, that has to do with class defaulting. However there exists type variable /kind/
138 defaulting. Again this is done at the top-level and the plan is:
139      - At the top-level, once you had a go at solving the constraint, do 
140        figure out /all/ the touchable unification variables of the wanted contraints.
141      - Apply defaulting to their kinds
142
143 More details in Note [DefaultTyVar].
144
145 \begin{code}
146
147 ------------------
148 simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
149 simplifyAmbiguityCheck name wanteds
150   = traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >> 
151     simplifyCheck wanteds
152  
153 ------------------
154 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
155 simplifyInteractive wanteds 
156   = traceTc "simplifyInteractive" empty >>
157     simplifyTop wanteds 
158
159 ------------------
160 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
161                 -> TcM ()       -- Succeeds iff the constraint is soluble
162 simplifyDefault theta
163   = do { traceTc "simplifyInteractive" empty
164        ; wanted <- newFlatWanteds DefaultOrigin theta
165        ; _ignored_ev_binds <- simplifyCheck (mkFlatWC wanted)
166        ; return () }
167 \end{code}
168
169
170 ***********************************************************************************
171 *                                                                                 * 
172 *                            Deriving                                             *
173 *                                                                                 *
174 ***********************************************************************************
175
176 \begin{code}
177 simplifyDeriv :: CtOrigin
178               -> PredType
179               -> [TyVar]        
180               -> ThetaType              -- Wanted
181               -> TcM ThetaType  -- Needed
182 -- Given  instance (wanted) => C inst_ty 
183 -- Simplify 'wanted' as much as possibles
184 -- Fail if not possible
185 simplifyDeriv orig pred tvs theta 
186   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
187                 -- The constraint solving machinery 
188                 -- expects *TcTyVars* not TyVars.  
189                 -- We use *non-overlappable* (vanilla) skolems
190                 -- See Note [Overlap and deriving]
191
192        ; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
193              skol_set   = mkVarSet tvs_skols
194              doc = ptext (sLit "deriving") <+> parens (ppr pred)
195
196        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
197
198        ; traceTc "simplifyDeriv" $ 
199          vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
200        ; (residual_wanted, _ev_binds1)
201              <- runTcS $ solveWanteds (mkFlatWC wanted)
202
203        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
204                          -- See Note [Exotic derived instance contexts]
205              get_good :: Ct -> Either PredType Ct
206              get_good ct | validDerivPred skol_set p = Left p
207                          | otherwise                 = Right ct
208                          where p = ctPred ct
209
210        -- We never want to defer these errors because they are errors in the
211        -- compiler! Hence the `False` below
212        ; _ev_binds2 <- reportUnsolved False (residual_wanted { wc_flat = bad })
213
214        ; let min_theta = mkMinimalBySCs (bagToList good)
215        ; return (substTheta subst_skol min_theta) }
216 \end{code}
217
218 Note [Overlap and deriving]
219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
220 Consider some overlapping instances:
221   data Show a => Show [a] where ..
222   data Show [Char] where ...
223
224 Now a data type with deriving:
225   data T a = MkT [a] deriving( Show )
226
227 We want to get the derived instance
228   instance Show [a] => Show (T a) where...
229 and NOT
230   instance Show a => Show (T a) where...
231 so that the (Show (T Char)) instance does the Right Thing
232
233 It's very like the situation when we're inferring the type
234 of a function
235    f x = show [x]
236 and we want to infer
237    f :: Show [a] => a -> String
238
239 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
240              the context for the derived instance. 
241              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
242
243 Note [Exotic derived instance contexts]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 In a 'derived' instance declaration, we *infer* the context.  It's a
246 bit unclear what rules we should apply for this; the Haskell report is
247 silent.  Obviously, constraints like (Eq a) are fine, but what about
248         data T f a = MkT (f a) deriving( Eq )
249 where we'd get an Eq (f a) constraint.  That's probably fine too.
250
251 One could go further: consider
252         data T a b c = MkT (Foo a b c) deriving( Eq )
253         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
254
255 Notice that this instance (just) satisfies the Paterson termination 
256 conditions.  Then we *could* derive an instance decl like this:
257
258         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
259 even though there is no instance for (C Int a), because there just
260 *might* be an instance for, say, (C Int Bool) at a site where we
261 need the equality instance for T's.  
262
263 However, this seems pretty exotic, and it's quite tricky to allow
264 this, and yet give sensible error messages in the (much more common)
265 case where we really want that instance decl for C.
266
267 So for now we simply require that the derived instance context
268 should have only type-variable constraints.
269
270 Here is another example:
271         data Fix f = In (f (Fix f)) deriving( Eq )
272 Here, if we are prepared to allow -XUndecidableInstances we
273 could derive the instance
274         instance Eq (f (Fix f)) => Eq (Fix f)
275 but this is so delicate that I don't think it should happen inside
276 'deriving'. If you want this, write it yourself!
277
278 NB: if you want to lift this condition, make sure you still meet the
279 termination conditions!  If not, the deriving mechanism generates
280 larger and larger constraints.  Example:
281   data Succ a = S a
282   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
283
284 Note the lack of a Show instance for Succ.  First we'll generate
285   instance (Show (Succ a), Show a) => Show (Seq a)
286 and then
287   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
288 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
289
290 The bottom line
291 ~~~~~~~~~~~~~~~
292 Allow constraints which consist only of type variables, with no repeats.
293
294 *********************************************************************************
295 *                                                                                 * 
296 *                            Inference
297 *                                                                                 *
298 ***********************************************************************************
299
300 Note [Which variables to quantify]
301 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
302 Suppose the inferred type of a function is
303    T kappa (alpha:kappa) -> Int
304 where alpha is a type unification variable and 
305       kappa is a kind unification variable
306 Then we want to quantify over *both* alpha and kappa.  But notice that
307 kappa appears "at top level" of the type, as well as inside the kind
308 of alpha.  So it should be fine to just look for the "top level"
309 kind/type variables of the type, without looking transitively into the
310 kinds of those type variables.
311
312 \begin{code}
313 simplifyInfer :: Bool
314               -> Bool                  -- Apply monomorphism restriction
315               -> [(Name, TcTauType)]   -- Variables to be generalised,
316                                        -- and their tau-types
317               -> (Untouchables, WantedConstraints)
318               -> TcM ([TcTyVar],    -- Quantify over these type variables
319                       [EvVar],      -- ... and these constraints
320                       Bool,         -- The monomorphism restriction did something
321                                     --   so the results type is not as general as
322                                     --   it could be
323                       TcEvBinds)    -- ... binding these evidence variables
324 simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
325   | isEmptyWC wanteds
326   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
327        ; zonked_taus <- zonkTcTypes (map snd name_taus)
328        ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
329                                -- tvs_to_quantify can contain both kind and type vars
330                                -- See Note [Which variables to quantify]
331        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
332        ; return (qtvs, [], False, emptyTcEvBinds) }
333
334   | otherwise
335   = do { runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
336        ; gbl_tvs        <- tcGetGlobalTyVars
337        ; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
338        ; zonked_wanteds <- zonkWC wanteds
339
340        ; traceTc "simplifyInfer {"  $ vcat
341              [ ptext (sLit "names =") <+> ppr (map fst name_taus)
342              , ptext (sLit "taus =") <+> ppr (map snd name_taus)
343              , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
344              , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
345              , ptext (sLit "closed =") <+> ppr _top_lvl
346              , ptext (sLit "apply_mr =") <+> ppr apply_mr
347              , ptext (sLit "untch =") <+> ppr untch
348              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
349              ]
350
351               -- Historical note: Before step 2 we used to have a
352               -- HORRIBLE HACK described in Note [Avoid unecessary
353               -- constraint simplification] but, as described in Trac
354               -- #4361, we have taken in out now.  That's why we start
355               -- with step 2!
356
357               -- Step 2) First try full-blown solving 
358
359               -- NB: we must gather up all the bindings from doing
360               -- this solving; hence (runTcSWithEvBinds ev_binds_var).
361               -- And note that since there are nested implications,
362               -- calling solveWanteds will side-effect their evidence
363               -- bindings, so we can't just revert to the input
364               -- constraint.
365        ; ev_binds_var <- newTcEvBinds
366        ; wanted_transformed <- runTcSWithEvBinds ev_binds_var $ 
367                                solveWanteds zonked_wanteds
368
369               -- Step 3) Fail fast if there is an insoluble constraint,
370               -- unless we are deferring errors to runtime
371        ; when (not runtimeCoercionErrors && insolubleWC wanted_transformed) $ 
372          do { _ev_binds <- reportUnsolved False wanted_transformed; failM }
373
374               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
375        ; let quant_candidates = approximateWC wanted_transformed               
376               -- NB: Already the fixpoint of any unifications that may have happened                                
377               -- NB: We do not do any defaulting when inferring a type, this can lead
378               -- to less polymorphic types, see Note [Default while Inferring]
379                                 
380               -- Step 5) Minimize the quantification candidates                             
381        ; (quant_candidates_transformed, _extra_binds)   
382              <- runTcS $ solveWanteds $ WC { wc_flat  = quant_candidates
383                                            , wc_impl  = emptyBag
384                                            , wc_insol = emptyBag }
385
386               -- Step 6) Final candidates for quantification                
387        ; let final_quant_candidates :: Bag PredType
388              final_quant_candidates = mapBag ctPred $ 
389                                       keepWanted (wc_flat quant_candidates_transformed)
390              -- NB: Already the fixpoint of any unifications that may have happened
391                   
392        ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
393        ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
394        
395        ; traceTc "simplifyWithApprox" $
396          vcat [ ptext (sLit "final_quant_candidates =") <+> ppr final_quant_candidates
397               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
398               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs ]
399          
400        ; let init_tvs        = zonked_tau_tvs `minusVarSet` gbl_tvs
401              poly_qtvs       = growPreds gbl_tvs id final_quant_candidates init_tvs
402              
403              pbound          = filterBag (quantifyMe poly_qtvs id) final_quant_candidates
404              
405        ; traceTc "simplifyWithApprox" $
406          vcat [ ptext (sLit "pbound =") <+> ppr pbound ]
407          
408              -- Monomorphism restriction
409        ; let mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
410              constrained_tvs = tyVarsOfBag tyVarsOfType final_quant_candidates
411              mr_bites        = apply_mr && not (isEmptyBag pbound)
412
413              (qtvs, bound)
414                 | mr_bites  = (mr_qtvs,   emptyBag)
415                 | otherwise = (poly_qtvs, pbound)
416              
417
418        ; if isEmptyVarSet qtvs && isEmptyBag bound
419          then do { traceTc "} simplifyInfer/no quantification" empty                   
420                  ; emitConstraints wanted_transformed
421                     -- Includes insolubles (if -fdefer-type-errors)
422                     -- as well as flats and implications
423                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
424          else do
425
426        { traceTc "simplifyApprox" $ 
427          ptext (sLit "bound are =") <+> ppr bound 
428          
429             -- Step 4, zonk quantified variables 
430        ; let minimal_flat_preds = mkMinimalBySCs $ bagToList bound
431              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
432                                    | (name, ty) <- name_taus ]
433                         -- Don't add the quantified variables here, because
434                         -- they are also bound in ic_skols and we want them to be
435                         -- tidied uniformly
436
437        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
438
439             -- Step 7) Emit an implication
440        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
441        ; lcl_env <- getLclTypeEnv
442        ; gloc <- getCtLoc skol_info
443        ; let implic = Implic { ic_untch    = untch 
444                              , ic_env      = lcl_env
445                              , ic_skols    = qtvs_to_return
446                              , ic_given    = minimal_bound_ev_vars
447                              , ic_wanted   = wanted_transformed 
448                              , ic_insol    = False
449                              , ic_binds    = ev_binds_var
450                              , ic_loc      = gloc }
451        ; emitImplication implic
452          
453        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
454              vcat [ ptext (sLit "implic =") <+> ppr implic
455                        -- ic_skols, ic_given give rest of result
456                   , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
457                   , ptext (sLit "spb =") <+> ppr final_quant_candidates
458                   , ptext (sLit "bound =") <+> ppr bound ]
459
460        ; return ( qtvs_to_return, minimal_bound_ev_vars
461                 , mr_bites,  TcEvBinds ev_binds_var) } }
462     where 
463 \end{code}
464
465
466 Note [Note [Default while Inferring]
467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
468 Our current plan is that defaulting only happens at simplifyTop and
469 not simplifyInfer.  This may lead to some insoluble deferred constraints
470 Example:
471
472 instance D g => C g Int b 
473
474 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
475 type inferred       = gamma -> gamma 
476
477 Now, if we try to default (alpha := Int) we will be able to refine the implication to 
478   (forall b. 0 => C gamma Int b) 
479 which can then be simplified further to 
480   (forall b. 0 => D gamma)
481 Finally we /can/ approximate this implication with (D gamma) and infer the quantified
482 type:  forall g. D g => g -> g
483
484 Instead what will currently happen is that we will get a quantified type 
485 (forall g. g -> g) and an implication:
486        forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
487
488 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an 
489 unsolvable implication:
490        forall g. 0 => (forall b. 0 => D g)
491
492 The concrete example would be: 
493        h :: C g a s => g -> a -> ST s a
494        f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
495
496 But it is quite tedious to do defaulting and resolve the implication constraints and
497 we have not observed code breaking because of the lack of defaulting in inference so 
498 we don't do it for now.
499
500
501
502 Note [Minimize by Superclasses]
503 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
504
505 When we quantify over a constraint, in simplifyInfer we need to
506 quantify over a constraint that is minimal in some sense: For
507 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
508 we'd like to quantify over Ord alpha, because we can just get Eq alpha
509 from superclass selection from Ord alpha. This minimization is what
510 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
511 to check the original wanted.
512
513
514 \begin{code}
515
516
517 approximateWC :: WantedConstraints -> Cts
518 approximateWC wc = float_wc emptyVarSet wc
519   where 
520     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
521     float_wc skols (WC { wc_flat = flat, wc_impl = implic }) = floats1 `unionBags` floats2
522       where floats1 = do_bag (float_flat skols) flat
523             floats2 = do_bag (float_implic skols) implic
524                                  
525     float_implic :: TcTyVarSet -> Implication -> Cts
526     float_implic skols imp
527       = float_wc (skols `extendVarSetList` ic_skols imp) (ic_wanted imp)
528             
529     float_flat :: TcTyVarSet -> Ct -> Cts
530     float_flat skols ct
531       | tyVarsOfCt ct `disjointVarSet` skols 
532       , isWantedCt ct = singleCt ct
533       | otherwise = emptyCts
534         
535     do_bag :: (a -> Bag c) -> Bag a -> Bag c
536     do_bag f = foldrBag (unionBags.f) emptyBag
537
538
539 \end{code}
540
541 \begin{code}
542 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
543 growPreds gbl_tvs get_pred items tvs
544   = foldrBag extend tvs items
545   where
546     extend item tvs = tvs `unionVarSet`
547                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
548
549 --------------------
550 quantifyMe :: TyVarSet      -- Quantifying over these
551            -> (a -> PredType)
552            -> a -> Bool     -- True <=> quantify over this wanted
553 quantifyMe qtvs toPred ct
554   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
555   | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
556   where
557     pred = toPred ct
558 \end{code}
559
560 Note [Avoid unecessary constraint simplification]
561 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
562     -------- NB NB NB (Jun 12) ------------- 
563     This note not longer applies; see the notes with Trac #4361.
564     But I'm leaving it in here so we remember the issue.)
565     ----------------------------------------
566 When inferring the type of a let-binding, with simplifyInfer,
567 try to avoid unnecessarily simplifying class constraints.
568 Doing so aids sharing, but it also helps with delicate 
569 situations like
570
571    instance C t => C [t] where ..
572
573    f :: C [t] => ....
574    f x = let g y = ...(constraint C [t])... 
575          in ...
576 When inferring a type for 'g', we don't want to apply the
577 instance decl, because then we can't satisfy (C t).  So we
578 just notice that g isn't quantified over 't' and partition
579 the contraints before simplifying.
580
581 This only half-works, but then let-generalisation only half-works.
582
583
584 Note [Inheriting implicit parameters]
585 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
586 Consider this:
587
588         f x = (x::Int) + ?y
589
590 where f is *not* a top-level binding.
591 From the RHS of f we'll get the constraint (?y::Int).
592 There are two types we might infer for f:
593
594         f :: Int -> Int
595
596 (so we get ?y from the context of f's definition), or
597
598         f :: (?y::Int) => Int -> Int
599
600 At first you might think the first was better, becuase then
601 ?y behaves like a free variable of the definition, rather than
602 having to be passed at each call site.  But of course, the WHOLE
603 IDEA is that ?y should be passed at each call site (that's what
604 dynamic binding means) so we'd better infer the second.
605
606 BOTTOM LINE: when *inferring types* you *must* quantify 
607 over implicit parameters. See the predicate isFreeWhenInferring.
608
609
610 *********************************************************************************
611 *                                                                                 * 
612 *                             RULES                                               *
613 *                                                                                 *
614 ***********************************************************************************
615
616 See note [Simplifying RULE consraints] in TcRule
617
618 Note [RULE quanfification over equalities]
619 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
620 Decideing 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 \begin{code}
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 { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
641        ; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
642              
643                  -- We allow ourselves to unify environment 
644                  -- variables: runTcS runs with NoUntouchables
645        ; (resid_wanted, _) <- runTcS (solveWanteds zonked_all)
646
647        ; zonked_lhs <- zonkWC lhs_wanted
648
649        ; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
650              quantify_me  -- Note [RULE quantification over equalities]
651                | insolubleWC resid_wanted = quantify_insol
652                | otherwise                = quantify_normal
653
654              quantify_insol ct = not (isEqPred (ctPred ct))
655
656              quantify_normal ct
657                | EqPred t1 t2 <- classifyPredType (ctPred ct)
658                = not (t1 `eqType` t2)
659                | otherwise
660                = True
661              
662        ; traceTc "simplifyRule" $
663          vcat [ doc
664               , text "zonked_lhs" <+> ppr zonked_lhs 
665               , text "q_cts"      <+> ppr q_cts ]
666
667        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
668                 , zonked_lhs { wc_flat = non_q_cts }) }
669 \end{code}
670
671
672 *********************************************************************************
673 *                                                                                 * 
674 *                                 Main Simplifier                                 *
675 *                                                                                 *
676 ***********************************************************************************
677
678 \begin{code}
679 simplifyCheck :: WantedConstraints      -- Wanted
680               -> TcM (Bag EvBind)
681 -- Solve a single, top-level implication constraint
682 -- e.g. typically one created from a top-level type signature
683 --          f :: forall a. [a] -> [a]
684 --          f x = rhs
685 -- We do this even if the function has no polymorphism:
686 --          g :: Int -> Int
687
688 --          g y = rhs
689 -- (whereas for *nested* bindings we would not create
690 --  an implication constraint for g at all.)
691 --
692 -- Fails if can't solve something in the input wanteds
693 simplifyCheck wanteds
694   = do { wanteds <- zonkWC wanteds
695
696        ; traceTc "simplifyCheck {" (vcat
697              [ ptext (sLit "wanted =") <+> ppr wanteds ])
698
699        ; (unsolved, eb1) <- runTcS (solveWanteds wanteds)
700
701        ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved
702
703        ; traceTc "reportUnsolved {" empty
704        -- See Note [Deferring coercion errors to runtime]
705        ; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
706        ; eb2 <- reportUnsolved runtimeCoercionErrors unsolved 
707        ; traceTc "reportUnsolved }" empty
708
709        ; return (eb1 `unionBags` eb2) }
710 \end{code}
711
712 Note [Deferring coercion errors to runtime]
713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
714
715 While developing, sometimes it is desirable to allow compilation to succeed even
716 if there are type errors in the code. Consider the following case:
717
718   module Main where
719
720   a :: Int
721   a = 'a'
722
723   main = print "b"
724
725 Even though `a` is ill-typed, it is not used in the end, so if all that we're
726 interested in is `main` it is handy to be able to ignore the problems in `a`.
727
728 Since we treat type equalities as evidence, this is relatively simple. Whenever
729 we run into a type mismatch in TcUnify, we normally just emit an error. But it
730 is always safe to defer the mismatch to the main constraint solver. If we do
731 that, `a` will get transformed into
732
733   co :: Int ~ Char
734   co = ...
735
736   a :: Int
737   a = 'a' `cast` co
738
739 The constraint solver would realize that `co` is an insoluble constraint, and
740 emit an error with `reportUnsolved`. But we can also replace the right-hand side
741 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
742 to compile, and it will run fine unless we evaluate `a`. This is what
743 `deferErrorsToRuntime` does.
744
745 It does this by keeping track of which errors correspond to which coercion
746 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
747 and does not fail if -fwarn-type-errors is on, so that we can continue
748 compilation. The errors are turned into warnings in `reportUnsolved`.
749
750 \begin{code}
751 solveWanteds :: WantedConstraints -> TcS WantedConstraints
752 -- Returns: residual constraints, plus evidence bindings 
753 -- NB: When we are called from TcM there are no inerts to pass down to TcS
754 solveWanteds wanted
755   = do { (_,wc_out) <- solve_wanteds wanted
756        ; let wc_ret = wc_out { wc_flat = keepWanted (wc_flat wc_out) } 
757                       -- Discard Derived
758        ; return wc_ret }
759
760 solve_wanteds :: WantedConstraints
761               -> TcS (TvSubst, WantedConstraints) 
762               -- NB: wc_flats may be wanted *or* derived now
763               -- Returns the flattening substitution as well in case we need to apply it
764 solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) 
765   = do { traceTcS "solveWanteds {" (ppr wanted)
766
767                  -- Try the flat bit
768                  -- Discard from insols all the derived/given constraints
769                  -- because they will show up again when we try to solve
770                  -- everything else.  Solving them a second time is a bit
771                  -- of a waste, but the code is simple, and the program is
772                  -- wrong anyway!
773
774                  -- DV: why only keepWanted? We make sure that we never float out
775                  -- whatever constraints can yield equalities, including class 
776                  -- constraints with functional dependencies and hence all the derived
777                  -- that were potentially insoluble will be re-generated.
778                  -- (It would not hurt though to just keep the wanted and the derived)
779                  -- See Note [The HasEqualities Predicate] in Inst.lhs
780          
781        ; let all_flats = flats `unionBags` keepWanted insols
782                          
783        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
784
785        -- solve_wanteds iterates when it is able to float equalities 
786        -- out of one or more of the implications. 
787        ; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
788
789        ; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS 
790
791        ; bb <- getTcEvBindsMap
792        ; tb <- getTcSTyBindsMap
793
794        ; traceTcS "solveWanteds }" $
795                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
796                       , text "unsolved_implics =" <+> ppr unsolved_implics
797                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb)
798                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
799                       ]
800
801        ; (subst, remaining_unsolved_flats) <- solveCTyFunEqs unsolved_flats
802                 -- See Note [Solving Family Equations]
803                 -- NB: remaining_flats has already had subst applied
804
805        ; traceTcS "solveWanteds finished with" $
806                  vcat [ text "remaining_unsolved_flats =" <+> ppr remaining_unsolved_flats
807                       , text "subst =" <+> ppr subst
808                       ]
809
810        ; return $ 
811          (subst, WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
812                     , wc_impl  = mapBag (substImplication subst) unsolved_implics
813                     , wc_insol = mapBag (substCt subst) insoluble_flats })
814        }
815
816 simpl_loop :: Int
817            -> Bag Implication
818            -> TcS (Bag Implication)
819 simpl_loop n implics
820   | n > 10 
821   = traceTcS "solveWanteds: loop!" empty >> return implics
822   | otherwise 
823   = do { (implic_eqs, unsolved_implics) <- solveNestedImplications implics
824
825        ; inerts <- getTcSInerts
826        ; let ((_,unsolved_flats),_) = extractUnsolved inerts
827                                       
828        ; let improve_eqs = implic_eqs
829              -- NB: improve_eqs used to contain defaulting equations HERE but 
830              -- defaulting now happens only at simplifyTop and not deep inside 
831              -- simpl_loop! See Note [Top-level Defaulting Plan]
832              
833        ; traceTcS "solveWanteds: simpl_loop end" $
834              vcat [ text "improve_eqs      =" <+> ppr improve_eqs
835                   , text "unsolved_flats   =" <+> ppr unsolved_flats
836                   , text "unsolved_implics =" <+> ppr unsolved_implics ]
837
838        ; if isEmptyBag improve_eqs then return unsolved_implics 
839          else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
840                  ; simpl_loop (n+1) (unsolved_implics `unionBags` 
841                                                  impls_from_eqs)} }
842
843 solveNestedImplications :: Bag Implication
844                         -> TcS (Cts, Bag Implication)
845 -- Precondition: the TcS inerts may contain unsolved flats which have 
846 -- to be converted to givens before we go inside a nested implication.
847 solveNestedImplications implics
848   | isEmptyBag implics
849   = return (emptyBag, emptyBag)
850   | otherwise 
851   = do { inerts <- getTcSInerts
852        ; traceTcS "solveNestedImplications starting, inerts are:" $ ppr inerts
853          
854        ; let ((_insoluble_flats, unsolved_flats),thinner_inerts) = extractUnsolved inerts 
855        ; traceTcS "solveNestedImplications starting, more info:" $ 
856          vcat [ text "inerts          = " <+> ppr inerts
857               , text "insoluble_flats = " <+> ppr _insoluble_flats
858               , text "unsolved_flats  = " <+> ppr unsolved_flats
859               , text "thinner_inerts  = " <+> ppr thinner_inerts ]
860          
861        ; (implic_eqs, unsolved_implics)
862            <- doWithInert thinner_inerts $ 
863               do { let pushed_givens = givens_from_wanteds unsolved_flats
864                        tcs_untouchables 
865                          = foldr (unionVarSet . tyVarsOfCt) emptyVarSet pushed_givens
866                                           -- Typically pushed_givens is very small, consists
867                                           -- only of unsolved equalities, so no inefficiency 
868                                           -- danger.
869                                                                                     
870                                           
871                  -- See Note [Preparing inert set for implications]
872                  -- Push the unsolved wanteds inwards, but as givens
873                  ; traceTcS "solveWanteds: preparing inerts for implications {" $ 
874                    vcat [ppr tcs_untouchables, ppr pushed_givens]
875                  ; impls_from_givens <- solveInteractCts pushed_givens
876                                         
877                  ; MASSERT (isEmptyBag impls_from_givens)
878                        -- impls_from_givens must be empty, since we are reacting givens
879                        -- with givens, and they can never generate extra implications 
880                        -- from decomposition of ForAll types. (Whereas wanteds can, see
881                        -- TcCanonical, canEq ForAll-ForAll case)
882                    
883                  ; traceTcS "solveWanteds: } now doing nested implications {" empty
884                  ; flatMapBagPairM (solveImplication tcs_untouchables) implics }
885
886        -- ... and we are back in the original TcS inerts 
887        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
888        -- them in the beginning of this function.
889        ; traceTcS "solveWanteds: done nested implications }" $
890                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
891                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
892
893        ; return (implic_eqs, unsolved_implics) }
894
895   where givens_from_wanteds = foldrBag get_wanted []
896         get_wanted cc rest_givens
897             | pushable_wanted cc
898             = let fl   = ctEvidence cc
899                   gfl  = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
900                                , ctev_evtm = EvId (ctev_evar fl)
901                                , ctev_pred = ctev_pred fl }
902                   this_given = cc { cc_ev = gfl }
903               in this_given : rest_givens
904             | otherwise = rest_givens 
905
906         pushable_wanted :: Ct -> Bool 
907         pushable_wanted cc 
908          | isWantedCt cc 
909          = isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
910          | otherwise = False 
911
912 solveImplication :: TcTyVarSet     -- Untouchable TcS unification variables
913                  -> Implication    -- Wanted
914                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
915                          Bag Implication) -- Unsolved rest (always empty or singleton)
916 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
917 -- which after trying to solve this implication we must restore to their original value
918 solveImplication tcs_untouchables
919      imp@(Implic { ic_untch  = untch
920                  , ic_binds  = ev_binds
921                  , ic_skols  = skols 
922                  , ic_given  = givens
923                  , ic_wanted = wanteds
924                  , ic_loc    = loc })
925   = shadowIPs givens $    -- See Note [Shadowing of Implicit Parameters]
926     nestImplicTcS ev_binds (untch, tcs_untouchables) $
927     recoverTcS (return (emptyBag, emptyBag)) $
928        -- Recover from nested failures.  Even the top level is
929        -- just a bunch of implications, so failing at the first one is bad
930     do { traceTcS "solveImplication {" (ppr imp) 
931
932          -- Solve flat givens
933        ; impls_from_givens <- solveInteractGiven loc givens 
934        ; MASSERT (isEmptyBag impls_from_givens)
935          
936          -- Simplify the wanteds
937        ; (_flat_subst, 
938            WC { wc_flat = unsolved_flats
939               , wc_impl = unsolved_implics
940               , wc_insol = insols }) <- solve_wanteds wanteds
941           -- NB: Not solveWanteds because we need the derived equalities,            
942           -- which may not be solvable (due to touchability) in this implication
943           -- but may become solvable by spontantenous unification outside. 
944
945        ; let (res_flat_free, res_flat_bound)
946                  = floatEqualities skols givens unsolved_flats
947              final_flat = keepWanted res_flat_bound
948
949        ; let res_wanted = WC { wc_flat  = final_flat
950                              , wc_impl  = unsolved_implics
951                              , wc_insol = insols }
952
953              res_implic = unitImplication $
954                           imp { ic_wanted = res_wanted
955                               , ic_insol  = insolubleWC res_wanted }
956
957        ; evbinds <- getTcEvBindsMap
958
959        ; traceTcS "solveImplication end }" $ vcat
960              [ text "res_flat_free =" <+> ppr res_flat_free
961              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds)
962              , text "res_implic =" <+> ppr res_implic ]
963
964        ; return (res_flat_free, res_implic) }
965     -- and we are back to the original inerts
966
967
968 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
969 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
970 -- and come from the input wanted ev vars or deriveds 
971 floatEqualities skols can_given wantders
972   | hasEqualities can_given = (emptyBag, wantders)
973           -- Note [Float Equalities out of Implications]
974   | otherwise = partitionBag is_floatable wantders
975   where skol_set = mkVarSet skols
976         is_floatable :: Ct -> Bool
977         is_floatable ct
978           | ct_predty <- ctPred ct
979           , isEqPred ct_predty
980           = skol_set `disjointVarSet` tvs_under_fsks ct_predty
981         is_floatable _ct = False
982
983         tvs_under_fsks :: Type -> TyVarSet
984         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
985         tvs_under_fsks (TyVarTy tv)     
986           | not (isTcTyVar tv)               = unitVarSet tv
987           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
988           | otherwise                        = unitVarSet tv
989         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
990         tvs_under_fsks (LitTy {})       = emptyVarSet
991         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
992         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
993         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
994                                         -- can mention type variables!
995           | isTyVar tv                = inner_tvs `delVarSet` tv
996           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
997                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
998           where
999             inner_tvs = tvs_under_fsks ty
1000
1001 shadowIPs :: [EvVar] -> TcS a -> TcS a
1002 shadowIPs gs m
1003   | null shadowed = m
1004   | otherwise     = do is <- getTcSInerts
1005                        doWithInert (purgeShadowed is) m
1006   where
1007   shadowed  = mapMaybe isIP gs
1008
1009   isIP g    = do p <- evVarPred_maybe g
1010                  (x,_) <- isIPPred_maybe p
1011                  return x
1012
1013   isShadowedCt ct = isShadowedEv (ctEvidence ct)
1014   isShadowedEv ev = case isIPPred_maybe (ctEvPred ev) of
1015                       Just (x,_) -> x `elem` shadowed
1016                       _          -> False
1017
1018   purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
1019                         , inert_solved = purgeSolved (inert_solved is)
1020                         }
1021
1022   purgeDicts    = snd . partitionCCanMap isShadowedCt
1023   purgeCans ics = ics { inert_dicts = purgeDicts (inert_dicts ics) }
1024   purgeSolved   = filterSolved (not . isShadowedEv)
1025 \end{code}
1026
1027 Note [Preparing inert set for implications]
1028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1029 Before solving the nested implications, we convert any unsolved flat wanteds
1030 to givens, and add them to the inert set.  Reasons:
1031
1032   a) In checking mode, suppresses unnecessary errors.  We already have
1033      on unsolved-wanted error; adding it to the givens prevents any 
1034      consequential errors from showing up
1035
1036   b) More importantly, in inference mode, we are going to quantify over this
1037      constraint, and we *don't* want to quantify over any constraints that
1038      are deducible from it.
1039
1040   c) Flattened type-family equalities must be exposed to the nested
1041      constraints.  Consider
1042         F b ~ alpha, (forall c.  F b ~ alpha)
1043      Obviously this is soluble with [alpha := F b].  But the
1044      unification is only done by solveCTyFunEqs, right at the end of
1045      solveWanteds, and if we aren't careful we'll end up with an
1046      unsolved goal inside the implication.  We need to "push" the
1047      as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
1048      can be used to solve the inner (F b
1049      ~ alpha).  See Trac #4935.
1050
1051   d) There are other cases where interactions between wanteds that can help
1052      to solve a constraint. For example
1053
1054         class C a b | a -> b
1055
1056         (C Int alpha), (forall d. C d blah => C Int a)
1057
1058      If we push the (C Int alpha) inwards, as a given, it can produce
1059      a fundep (alpha~a) and this can float out again and be used to
1060      fix alpha.  (In general we can't float class constraints out just
1061      in case (C d blah) might help to solve (C Int a).)
1062
1063 The unsolved wanteds are *canonical* but they may not be *inert*,
1064 because when made into a given they might interact with other givens.
1065 Hence the call to solveInteract.  Example:
1066
1067  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
1068
1069 We were not able to solve (a ~w [beta]) but we can't just assume it as
1070 given because the resulting set is not inert. Hence we have to do a
1071 'solveInteract' step first. 
1072
1073 Finally, note that we convert them to [Given] and NOT [Given/Solved].
1074 The reason is that Given/Solved are weaker than Givens and may be discarded.
1075 As an example consider the inference case, where we may have, the following 
1076 original constraints: 
1077      [Wanted] F Int ~ Int
1078              (F Int ~ a => F Int ~ a)
1079 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
1080 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
1081 the (F Int ~ a) insoluble. Hence we should really convert the residual 
1082 wanteds to plain old Given. 
1083
1084 We need only push in unsolved equalities both in checking mode and inference mode: 
1085
1086   (1) In checking mode we should not push given dictionaries in because of
1087 example LongWayOverlapping.hs, where we might get strange overlap
1088 errors between far-away constraints in the program.  But even in
1089 checking mode, we must still push type family equations. Consider:
1090
1091    type instance F True a b = a 
1092    type instance F False a b = b
1093
1094    [w] F c a b ~ gamma 
1095    (c ~ True) => a ~ gamma 
1096    (c ~ False) => b ~ gamma
1097
1098 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
1099 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
1100 merely Given/Solved because it has to interact with the top-level instance 
1101 environment) and push it inside the implications. Now, when we come out again at
1102 the end, having solved the implications solveCTyFunEqs will solve this equality.
1103
1104   (2) In inference mode, we recheck the final constraint in checking mode and
1105 hence we will be able to solve inner implications from top-level quantified
1106 constraints nonetheless.
1107
1108
1109 Note [Extra TcsTv untouchables]
1110 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1111
1112 Whenever we are solving a bunch of flat constraints, they may contain 
1113 the following sorts of 'touchable' unification variables:
1114    
1115    (i)   Born-touchables in that scope
1116  
1117    (ii)  Simplifier-generated unification variables, such as unification 
1118          flatten variables
1119
1120    (iii) Touchables that have been floated out from some nested 
1121          implications, see Note [Float Equalities out of Implications]. 
1122
1123 Now, once we are done with solving these flats and have to move inwards to 
1124 the nested implications (perhaps for a second time), we must consider all the
1125 extra variables (categories (ii) and (iii) above) as untouchables for the 
1126 implication. Otherwise we have the danger or double unifications, as well
1127 as the danger of not ``seing'' some unification. Example (from Trac #4494):
1128
1129    (F Int ~ uf)  /\  [untch=beta](forall a. C a => F Int ~ beta) 
1130
1131 In this example, beta is touchable inside the implication. The 
1132 first solveInteract step leaves 'uf' ununified. Then we move inside 
1133 the implication where a new constraint
1134        uf  ~  beta  
1135 emerges. We may spontaneously solve it to get uf := beta, so the whole
1136 implication disappears but when we pop out again we are left with (F
1137 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
1138 uf will get unified *once more* to (F Int).
1139
1140 The solution is to record the unification variables of the flats, 
1141 and make them untouchables for the nested implication. In the 
1142 example above uf would become untouchable, so beta would be forced 
1143 to be unified as beta := uf.
1144
1145 Note [Float Equalities out of Implications]
1146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1147 For ordinary pattern matches (including existentials) we float 
1148 equalities out of implications, for instance: 
1149      data T where 
1150        MkT :: Eq a => a -> T 
1151      f x y = case x of MkT _ -> (y::Int)
1152 We get the implication constraint (x::T) (y::alpha): 
1153      forall a. [untouchable=alpha] Eq a => alpha ~ Int
1154 We want to float out the equality into a scope where alpha is no
1155 longer untouchable, to solve the implication!  
1156
1157 But we cannot float equalities out of implications whose givens may
1158 yield or contain equalities:
1159
1160       data T a where 
1161         T1 :: T Int
1162         T2 :: T Bool
1163         T3 :: T a 
1164         
1165       h :: T a -> a -> Int
1166       
1167       f x y = case x of 
1168                 T1 -> y::Int
1169                 T2 -> y::Bool
1170                 T3 -> h x y
1171
1172 We generate constraint, for (x::T alpha) and (y :: beta): 
1173    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
1174    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1175    (alpha ~ beta)                                      -- From 3rd branch 
1176
1177 If we float the equality (beta ~ Int) outside of the first implication and 
1178 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1179 But if we just leave them inside the implications we unify alpha := beta and
1180 solve everything.
1181
1182 Principle: 
1183     We do not want to float equalities out which may need the given *evidence*
1184     to become soluble.
1185
1186 Consequence: classes with functional dependencies don't matter (since there is 
1187 no evidence for a fundep equality), but equality superclasses do matter (since 
1188 they carry evidence).
1189
1190 Notice that, due to Note [Extra TcSTv Untouchables], the free unification variables 
1191 of an equality that is floated out of an implication become effectively untouchables
1192 for the leftover implication. This is absolutely necessary. Consider the following 
1193 example. We start with two implications and a class with a functional dependency. 
1194
1195 class C x y | x -> y
1196 instance C [a] [a]
1197       
1198 (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
1199 (I2)      [untch=beta]forall b. 0 => F Int ~ [[alpha]] /\ C beta [b]
1200
1201 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
1202 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
1203 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1204 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1205 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1206
1207 class C x y | x -> y where 
1208  op :: x -> y -> ()
1209
1210 instance C [a] [a]
1211
1212 type family F a :: *
1213
1214 h :: F Int -> ()
1215 h = undefined
1216
1217 data TEx where 
1218   TEx :: a -> TEx 
1219
1220
1221 f (x::beta) = 
1222     let g1 :: forall b. b -> ()
1223         g1 _ = h [x]
1224         g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1225     in (g1 '3', g2 undefined)
1226
1227 Note [Shadowing of Implicit Parameters]
1228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1229 Consider the following example:
1230
1231 f :: (?x :: Char) => Char
1232 f = let ?x = 'a' in ?x
1233
1234 The "let ?x = ..." generates an implication constraint of the form:
1235
1236 ?x :: Char => ?x :: Char
1237
1238
1239 Furthermore, the signature for `f` also generates an implication
1240 constraint, so we end up with the following nested implication:
1241
1242 ?x :: Char => (?x :: Char => ?x :: Char)
1243
1244 Note that the wanted (?x :: Char) constraint may be solved in
1245 two incompatible ways:  either by using the parameter from the
1246 signature, or by using the local definition.  Our intention is
1247 that the local definition should "shadow" the parameter of the
1248 signature, and we implement this as follows: when we nest implications,
1249 we remove any implicit parameters in the outer implication, that
1250 have the same name as givens of the inner implication.
1251
1252 Here is another variation of the example:
1253
1254 f :: (?x :: Int) => Char
1255 f = let ?x = 'x' in ?x
1256
1257 This program should also be accepted: the two constraints `?x :: Int`
1258 and `?x :: Char` never exist in the same context, so they don't get to
1259 interact to cause failure.
1260 \begin{code}
1261
1262 solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
1263 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1264 -- See Note [Solving Family Equations]
1265 -- Returns: a bunch of unsolved constraints from the original Cts and implications
1266 --          where the newly generated equalities (alpha := F xi) have been substituted through.
1267 solveCTyFunEqs cts
1268  = do { untch   <- getUntouchables 
1269       ; let (unsolved_can_cts, (ni_subst, cv_binds))
1270                 = getSolvableCTyFunEqs untch cts
1271       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1272                                           , ppr ni_subst, ppr cv_binds
1273                                           ])
1274       ; mapM_ solve_one cv_binds
1275
1276       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1277   where
1278     solve_one (Wanted { ctev_evar = cv }, tv, ty) 
1279       = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
1280     solve_one (Derived {}, tv, ty)
1281       = setWantedTyBind tv ty
1282     solve_one arg
1283       = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
1284 ------------
1285 type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
1286   -- The TvSubstEnv is not idempotent, but is loop-free
1287   -- See Note [Non-idempotent substitution] in Unify
1288 emptyFunEqBinds :: FunEqBinds
1289 emptyFunEqBinds = (emptyVarEnv, [])
1290
1291 extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
1292 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
1293   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
1294
1295 ------------
1296 getSolvableCTyFunEqs :: TcsUntouchables
1297                      -> Cts                -- Precondition: all Wanteds or Derived!
1298                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
1299 getSolvableCTyFunEqs untch cts
1300   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
1301   where
1302     dflt_funeq :: (Cts, FunEqBinds) -> Ct
1303                -> (Cts, FunEqBinds)
1304     dflt_funeq (cts_in, feb@(tv_subst, _))
1305                (CFunEqCan { cc_ev = fl
1306                           , cc_fun = tc
1307                           , cc_tyargs = xis
1308                           , cc_rhs = xi })
1309       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1310
1311       , isTouchableMetaTyVar_InRange untch tv
1312            -- And it's a *touchable* unification variable
1313
1314       , typeKind xi `tcIsSubKind` tyVarKind tv
1315          -- Must do a small kind check since TcCanonical invariants 
1316          -- on family equations only impose compatibility, not subkinding
1317
1318       , not (tv `elemVarEnv` tv_subst)
1319            -- Check not in extra_binds
1320            -- See Note [Solving Family Equations], Point 1
1321
1322       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1323            -- Occurs check: see Note [Solving Family Equations], Point 2
1324       = ASSERT ( not (isGiven fl) )
1325         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
1326
1327     dflt_funeq (cts_in, fun_eq_binds) ct
1328       = (cts_in `extendCts` ct, fun_eq_binds)
1329 \end{code}
1330
1331 Note [Solving Family Equations] 
1332 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1333 After we are done with simplification we may be left with constraints of the form:
1334      [Wanted] F xis ~ beta 
1335 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1336 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1337
1338 When is it ok to do so? 
1339     1) 'beta' must not already be defaulted to something. Example: 
1340
1341            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1342            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1343                                        have to report this as unsolved.
1344
1345     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1346        set [beta := F xis] only if beta is not among the free variables of xis.
1347
1348     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1349        of type family equations. See Inert Set invariants in TcInteract. 
1350
1351
1352 *********************************************************************************
1353 *                                                                               * 
1354 *                          Defaulting and disamgiguation                        *
1355 *                                                                               *
1356 *********************************************************************************
1357 \begin{code}
1358 applyDefaultingRules :: Cts      -- All wanteds
1359                      -> TcS Cts  -- All wanteds again!
1360 -- Return some *extra* givens, which express the 
1361 -- type-class-default choice
1362 applyDefaultingRules wanteds
1363   | isEmptyBag wanteds 
1364   = return emptyBag
1365   | otherwise
1366   = do { traceTcS "applyDefaultingRules { " $ 
1367                   text "wanteds =" <+> ppr wanteds
1368                   
1369        ; info@(default_tys, _) <- getDefaultInfo
1370        ; let groups = findDefaultableGroups info wanteds
1371        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1372                                                  , text "info=" <+> ppr info ]
1373        ; deflt_cts <- mapM (disambigGroup default_tys) groups
1374
1375        ; traceTcS "applyDefaultingRules }" $ 
1376                   vcat [ text "Type defaults =" <+> ppr deflt_cts]
1377
1378        ; return (unionManyBags deflt_cts) }
1379 \end{code}
1380
1381 Note [tryTcS in defaulting]
1382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1383
1384 defaultTyVar and disambigGroup create new evidence variables for
1385 default equations, and hence update the EvVar cache. However, after
1386 applyDefaultingRules we will try to solve these default equations
1387 using solveInteractCts, which will consult the cache and solve those
1388 EvVars from themselves! That's wrong.
1389
1390 To avoid this problem we guard defaulting under a @tryTcS@ which leaves
1391 the original cache unmodified.
1392
1393 There is a second reason for @tryTcS@ in defaulting: disambGroup does
1394 some constraint solving to determine if a default equation is
1395 ``useful'' in solving some wanted constraints, but we want to
1396 discharge all evidence and unifications that may have happened during
1397 this constraint solving.
1398
1399 Finally, @tryTcS@ importantly does not inherit the original cache from
1400 the higher level but makes up a new cache, the reason is that disambigGroup
1401 will call solveInteractCts so the new derived and the wanteds must not be 
1402 in the cache!
1403
1404
1405 \begin{code}
1406 ------------------
1407 touchablesOfWC :: WantedConstraints -> TcTyVarSet
1408 -- See Note [Extra Tcs Untouchables] to see why we carry a TcsUntouchables 
1409 -- instead of just using the Untouchable range have in our hands.
1410 touchablesOfWC = go (NoUntouchables, emptyVarSet)
1411   where go :: TcsUntouchables -> WantedConstraints -> TcTyVarSet
1412         go untch (WC { wc_flat = flats, wc_impl = impls }) 
1413           = filterVarSet is_touchable flat_tvs `unionVarSet`
1414               foldrBag (unionVarSet . (go_impl $ untch_for_impls untch)) emptyVarSet impls 
1415           where is_touchable = isTouchableMetaTyVar_InRange untch
1416                 flat_tvs = tyVarsOfCts flats
1417                 untch_for_impls (r,uset) = (r, uset `unionVarSet` flat_tvs)
1418         go_impl (_rng,set) implic = go (ic_untch implic,set) (ic_wanted implic)
1419
1420 applyTyVarDefaulting :: WantedConstraints -> TcM Cts
1421 applyTyVarDefaulting wc = runTcS do_dflt >>= (return . fst)
1422   where do_dflt = do { tv_cts <- mapM defaultTyVar $ 
1423                                  varSetElems (touchablesOfWC wc)
1424                      ; return (unionManyBags tv_cts) }
1425
1426 defaultTyVar :: TcTyVar -> TcS Cts
1427 -- Precondition: a touchable meta-variable
1428 defaultTyVar the_tv
1429   | not (k `eqKind` default_k)
1430   -- Why tryTcS? See Note [tryTcS in defaulting]
1431   = tryTcS $
1432     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1433        ; ty_k <- instFlexiTcSHelperTcS (tyVarName the_tv) default_k
1434        ; md <- newDerived loc (mkTcEqPred (mkTyVarTy the_tv) ty_k)
1435              -- Why not directly newDerived loc (mkTcEqPred k default_k)? 
1436              -- See Note [DefaultTyVar]
1437        ; let cts
1438               | Just der_ev <- md = [mkNonCanonical der_ev]
1439               | otherwise = []
1440        
1441        ; implics_from_defaulting <- solveInteractCts cts
1442        ; MASSERT (isEmptyBag implics_from_defaulting)
1443          
1444        ; (_,unsolved) <- extractUnsolvedTcS
1445        ; if isEmptyBag (keepWanted unsolved) then return (listToBag cts)
1446          else return emptyBag }
1447   | otherwise = return emptyBag  -- The common case
1448   where
1449     k = tyVarKind the_tv
1450     default_k = defaultKind k
1451 \end{code}
1452
1453 Note [DefaultTyVar]
1454 ~~~~~~~~~~~~~~~~~~~
1455 defaultTyVar is used on any un-instantiated meta type variables to
1456 default the kind of OpenKind and ArgKind etc to *.  This is important 
1457 to ensure that instance declarations match.  For example consider
1458
1459      instance Show (a->b)
1460      foo x = show (\_ -> True)
1461
1462 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1463 and that won't match the typeKind (*) in the instance decl.  See tests
1464 tc217 and tc175.
1465
1466 We look only at touchable type variables. No further constraints
1467 are going to affect these type variables, so it's time to do it by
1468 hand.  However we aren't ready to default them fully to () or
1469 whatever, because the type-class defaulting rules have yet to run.
1470
1471 An important point is that if the type variable tv has kind k and the
1472 default is default_k we do not simply generate [D] (k ~ default_k) because:
1473
1474    (1) k may be ArgKind and default_k may be * so we will fail
1475
1476    (2) We need to rewrite all occurrences of the tv to be a type
1477        variable with the right kind and we choose to do this by rewriting 
1478        the type variable /itself/ by a new variable which does have the 
1479        right kind.
1480
1481 \begin{code}
1482
1483
1484 ----------------
1485 findDefaultableGroups 
1486     :: ( [Type]
1487        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1488     -> Cts      -- Unsolved
1489     -> [[(Ct,TcTyVar)]]
1490 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1491   | null default_tys             = []
1492   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1493   where 
1494     unaries     :: [(Ct, TcTyVar)]  -- (C tv) constraints
1495     non_unaries :: [Ct]             -- and *other* constraints
1496     
1497     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1498         -- Finds unary type-class constraints
1499     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1500         | Just tv <- tcGetTyVar_maybe ty
1501         = Left (cc, tv)
1502     find_unary cc = Right cc  -- Non unary or non dictionary 
1503
1504     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1505     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1506
1507     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1508
1509     is_defaultable_group ds@((_,tv):_)
1510         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1511               b2 = not (tv `elemVarSet` bad_tvs)
1512               b4 = defaultable_classes [cc_class cc | (cc,_) <- ds]
1513           in (b1 && b2 && b4)
1514     is_defaultable_group [] = panic "defaultable_group"
1515
1516     defaultable_classes clss 
1517         | extended_defaults = any isInteractiveClass clss
1518         | otherwise         = all is_std_class clss && (any is_num_class clss)
1519
1520     -- In interactive mode, or with -XExtendedDefaultRules,
1521     -- we default Show a to Show () to avoid graututious errors on "show []"
1522     isInteractiveClass cls 
1523         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1524
1525     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1526     -- is_num_class adds IsString to the standard numeric classes, 
1527     -- when -foverloaded-strings is enabled
1528
1529     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1530     -- Similarly is_std_class
1531
1532 ------------------------------
1533 disambigGroup :: [Type]           -- The default types 
1534               -> [(Ct, TcTyVar)]  -- All classes of the form (C a)
1535                                   --  sharing same type variable
1536               -> TcS Cts
1537
1538 disambigGroup []  _grp
1539   = return emptyBag
1540 disambigGroup (default_ty:default_tys) group
1541   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1542        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1543                     do { derived_eq <- tryTcS $ 
1544                        -- I need a new tryTcS because we will call solveInteractCts below!
1545                             do { md <- newDerived (ctev_wloc the_fl) 
1546                                                   (mkTcEqPred (mkTyVarTy the_tv) default_ty)
1547                                                   -- ctev_wloc because constraint is not Given!
1548                                ; case md of 
1549                                     Nothing   -> return []
1550                                     Just ctev -> return [ mkNonCanonical ctev ] }
1551                             
1552                        ; traceTcS "disambigGroup (solving) {" $
1553                          text "trying to solve constraints along with default equations ..."
1554                        ; implics_from_defaulting <- 
1555                                     solveInteractCts (derived_eq ++ wanteds)
1556                        ; MASSERT (isEmptyBag implics_from_defaulting)
1557                            -- I am not certain if any implications can be generated
1558                            -- but I am letting this fail aggressively if this ever happens.
1559                                      
1560                        ; (_,unsolved) <- extractUnsolvedTcS 
1561                        ; traceTcS "disambigGroup (solving) }" $
1562                          text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved)
1563                        ; if isEmptyBag (keepWanted unsolved) then -- Don't care about Derived's
1564                              return (Just $ listToBag derived_eq) 
1565                          else 
1566                              return Nothing 
1567                        }
1568        ; case success of
1569            Just cts -> -- Success: record the type variable binding, and return
1570                     do { wrapWarnTcS $ warnDefaulting wanteds default_ty
1571                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1572                        ; return cts }
1573            Nothing -> -- Failure: try with the next type
1574                     do { traceTcS "disambigGroup failed, will try other default types"
1575                                   (ppr default_ty)
1576                        ; disambigGroup default_tys group } }
1577   where
1578     ((the_ct,the_tv):_) = group
1579     the_fl              = cc_ev the_ct
1580     wanteds             = map fst group
1581 \end{code}
1582
1583 Note [Avoiding spurious errors]
1584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1585 When doing the unification for defaulting, we check for skolem
1586 type variables, and simply don't default them.  For example:
1587    f = (*)      -- Monomorphic
1588    g :: Num a => a -> a
1589    g x = f x x
1590 Here, we get a complaint when checking the type signature for g,
1591 that g isn't polymorphic enough; but then we get another one when
1592 dealing with the (Num a) context arising from f's definition;
1593 we try to unify a with Int (to default it), but find that it's
1594 already been unified with the rigid variable from g's type sig
1595
1596
1597
1598 *********************************************************************************
1599 *                                                                               * 
1600 *                   Utility functions
1601 *                                                                               *
1602 *********************************************************************************
1603
1604 \begin{code}
1605 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1606 newFlatWanteds orig theta
1607   = do { loc <- getCtLoc orig
1608        ; mapM (inst_to_wanted loc) theta }
1609   where 
1610     inst_to_wanted loc pty 
1611           = do { v <- TcMType.newWantedEvVar pty 
1612                ; return $ 
1613                  CNonCanonical { cc_ev = Wanted { ctev_evar = v
1614                                                 , ctev_wloc = loc
1615                                                 , ctev_pred = pty }
1616                                , cc_depth = 0 } }
1617 \end{code}