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