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