When floating constraints outwards, promote the floated type variables
[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               -> (Untouchables, 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 (untch,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   = TcRnMonad.setUntouchables untch $
346     do { runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
347        ; gbl_tvs        <- tcGetGlobalTyVars
348        ; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
349        ; zonked_wanteds <- zonkWC wanteds
350
351        ; traceTc "simplifyInfer {"  $ vcat
352              [ ptext (sLit "names =") <+> ppr (map fst name_taus)
353              , ptext (sLit "taus =") <+> ppr (map snd name_taus)
354              , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
355              , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
356              , ptext (sLit "closed =") <+> ppr _top_lvl
357              , ptext (sLit "apply_mr =") <+> ppr apply_mr
358              , ptext (sLit "untch =") <+> ppr untch
359              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
360              ]
361
362               -- Historical note: Before step 2 we used to have a
363               -- HORRIBLE HACK described in Note [Avoid unecessary
364               -- constraint simplification] but, as described in Trac
365               -- #4361, we have taken in out now.  That's why we start
366               -- with step 2!
367
368               -- Step 2) First try full-blown solving 
369
370               -- NB: we must gather up all the bindings from doing
371               -- this solving; hence (runTcSWithEvBinds ev_binds_var).
372               -- And note that since there are nested implications,
373               -- calling solveWanteds will side-effect their evidence
374               -- bindings, so we can't just revert to the input
375               -- constraint.
376        ; ev_binds_var <- newTcEvBinds
377        ; wanted_transformed <- solveWantedsWithEvBinds ev_binds_var zonked_wanteds
378
379               -- Step 3) Fail fast if there is an insoluble constraint,
380               -- unless we are deferring errors to runtime
381        ; when (not runtimeCoercionErrors && insolubleWC wanted_transformed) $ 
382          do { _ev_binds <- reportUnsolved False wanted_transformed; failM }
383
384               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
385        ; let quant_candidates = approximateWC wanted_transformed               
386               -- NB: Already the fixpoint of any unifications that may have happened                                
387               -- NB: We do not do any defaulting when inferring a type, this can lead
388               -- to less polymorphic types, see Note [Default while Inferring]
389               -- NB: quant_candidates here are wanted or derived, we filter the wanteds later, anyway
390  
391               -- Step 5) Minimize the quantification candidates                             
392        ; (quant_candidates_transformed, _extra_binds)   
393              <- solveWanteds $ WC { wc_flat  = quant_candidates
394                                   , wc_impl  = emptyBag
395                                   , wc_insol = emptyBag }
396
397               -- Step 6) Final candidates for quantification                
398        ; let final_quant_candidates :: [PredType]
399              final_quant_candidates = map ctPred $ bagToList $
400                                       wc_flat quant_candidates_transformed
401              -- NB: Already the fixpoint of any unifications that may have happened
402                   
403        ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
404        ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
405        
406        ; traceTc "simplifyWithApprox" $
407          vcat [ ptext (sLit "final_quant_candidates =") <+> ppr final_quant_candidates
408               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
409               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs ]
410          
411        ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
412              poly_qtvs = growThetaTyVars final_quant_candidates init_tvs 
413                          `minusVarSet` gbl_tvs
414              pbound    = filter (quantifyPred poly_qtvs) final_quant_candidates
415              
416        ; traceTc "simplifyWithApprox" $
417          vcat [ ptext (sLit "pbound =") <+> ppr pbound
418               , ptext (sLit "init_qtvs =") <+> ppr init_tvs 
419               , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ]
420          
421              -- Monomorphism restriction
422        ; let mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
423              constrained_tvs = tyVarsOfTypes final_quant_candidates
424              mr_bites        = apply_mr && not (null pbound)
425
426              (qtvs, bound)
427                 | mr_bites  = (mr_qtvs,   [])
428                 | otherwise = (poly_qtvs, pbound)
429              
430
431        ; if isEmptyVarSet qtvs && null bound
432          then do { traceTc "} simplifyInfer/no quantification" empty                   
433                  ; emitConstraints wanted_transformed
434                     -- Includes insolubles (if -fdefer-type-errors)
435                     -- as well as flats and implications
436                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
437          else do
438
439        { traceTc "simplifyApprox" $ 
440          ptext (sLit "bound are =") <+> ppr bound 
441          
442             -- Step 4, zonk quantified variables 
443        ; let minimal_flat_preds = mkMinimalBySCs bound
444              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
445                                    | (name, ty) <- name_taus ]
446                         -- Don't add the quantified variables here, because
447                         -- they are also bound in ic_skols and we want them to be
448                         -- tidied uniformly
449
450        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
451
452             -- Step 7) Emit an implication
453        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
454        ; lcl_env <- getLclTypeEnv
455        ; gloc <- getCtLoc skol_info
456        ; let implic = Implic { ic_untch    = 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        ; floated_eqs <- promoteFloatedUnificationVars floated_eqs
806
807        -- ... and we are back in the original TcS inerts 
808        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
809        -- them in the beginning of this function.
810        ; traceTcS "solveNestedImplications end }" $
811                   vcat [ text "all floated_eqs ="  <+> ppr floated_eqs
812                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
813
814        ; return (floated_eqs, unsolved_implics) }
815
816 solveImplication :: InertSet
817                  -> Implication    -- Wanted
818                  -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
819                          Bag Implication) -- Unsolved rest (always empty or singleton)
820 -- Precondition: The TcS monad contains an empty worklist and given-only inerts 
821 -- which after trying to solve this implication we must restore to their original value
822 solveImplication inerts
823      imp@(Implic { ic_untch  = untch
824                  , ic_binds  = ev_binds
825                  , ic_skols  = skols 
826                  , ic_fsks   = old_fsks
827                  , ic_given  = givens
828                  , ic_wanted = wanteds
829                  , ic_loc    = loc })
830   = nestImplicTcS ev_binds untch inerts $
831     do { traceTcS "solveImplication {" (ppr imp) 
832
833          -- Solve the nested constraints
834        ; solveInteractGiven loc old_fsks givens 
835        ; residual_wanted <- solve_wanteds wanteds
836        ; new_fsks <- getFlattenSkols
837
838        ; let all_fsks = new_fsks ++ old_fsks
839              (floated_eqs, final_wanted)
840                  = floatEqualities (skols ++ all_fsks) givens residual_wanted
841
842              res_implic | isEmptyWC final_wanted 
843                         = emptyBag
844                         | otherwise
845                         = unitBag imp { ic_fsks   = all_fsks
846                                       , ic_wanted = dropDerivedWC final_wanted
847                                       , ic_insol  = insolubleWC final_wanted }
848
849        ; evbinds <- getTcEvBindsMap
850        ; traceTcS "solveImplication end }" $ vcat
851              [ text "floated_eqs =" <+> ppr floated_eqs
852              , text "new_fsks =" <+> ppr all_fsks
853              , text "res_implic =" <+> ppr res_implic
854              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
855
856        ; return (floated_eqs, res_implic) }
857 \end{code}
858
859 Note [Floating equalities]
860
861 \begin{code}
862 promoteFloatedUnificationVars :: Cts -> TcS Cts
863 promoteFloatedUnificationVars cts
864   = do { untch <- TcSMonad.getUntouchables
865        ; let tvs = filter (isFloatedTouchableMetaTyVar untch) $
866                    varSetElems (tyVarsOfCts cts)
867        ; tv_eqs <- mapM promote_tv tvs
868        ; traceTcS "promoteFloated" (vcat [ text "Ctxt untoucables =" <+> ppr untch
869                                          , text "Floated eqs =" <+> ppr cts
870                                          , text "Promoted tvs =" <+> ppr tvs
871                                          , text "Promoted eqs =" <+> ppr tv_eqs])
872        ; return (cts `unionBags` listToBag tv_eqs) }
873   where
874     wloc = ctev_wloc (cc_ev (head (bagToList cts)))   -- Yuk, but not needed soon
875     promote_tv tv 
876       = do { rhs_ty <- newFlexiTcSTy (tyVarKind tv)
877            ; let refl_evtm = EvCoercion (mkTcReflCo rhs_ty)
878                  refl_pred = mkTcEqPred (mkTyVarTy tv) rhs_ty
879                  given_ev  = Given { ctev_gloc = mkGivenLoc wloc UnkSkol
880                                    , ctev_pred = refl_pred
881                                    , ctev_evtm = refl_evtm }
882            ; setWantedTyBind tv rhs_ty
883            ; return (CTyEqCan { cc_ev = given_ev, cc_tyvar = tv
884                               , cc_rhs = rhs_ty, cc_depth = 0 }) }
885
886 floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints -> (Cts, WantedConstraints)
887 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
888 -- and come from the input wanted ev vars or deriveds 
889 floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
890   | hasEqualities can_given 
891   = (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
892   | otherwise 
893   = (float_eqs, wanteds { wc_flat = remaining_flats })
894   where 
895     (float_eqs, remaining_flats) = partitionBag is_floatable flats
896     skol_set = growSkols wanteds (mkVarSet skols)
897
898     is_floatable :: Ct -> Bool
899     is_floatable ct
900        = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
901        where
902          pred = ctPred ct
903
904 growSkols :: WantedConstraints -> VarSet -> VarSet
905 -- Find all the type variables that might possibly be unified
906 -- with a type that mentions a skolem.  This test is very conservative.
907 -- I don't *think* we need look inside the implications, because any 
908 -- relevant unification variables in there are untouchable.
909 growSkols (WC { wc_flat = flats }) skols
910   = growThetaTyVars theta skols
911   where
912     theta = foldrBag ((:) . ctPred) [] flats
913 \end{code}
914
915 Note [Float Equalities out of Implications]
916 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
917 For ordinary pattern matches (including existentials) we float 
918 equalities out of implications, for instance: 
919      data T where 
920        MkT :: Eq a => a -> T 
921      f x y = case x of MkT _ -> (y::Int)
922 We get the implication constraint (x::T) (y::alpha): 
923      forall a. [untouchable=alpha] Eq a => alpha ~ Int
924 We want to float out the equality into a scope where alpha is no
925 longer untouchable, to solve the implication!  
926
927 But we cannot float equalities out of implications whose givens may
928 yield or contain equalities:
929
930       data T a where 
931         T1 :: T Int
932         T2 :: T Bool
933         T3 :: T a 
934         
935       h :: T a -> a -> Int
936       
937       f x y = case x of 
938                 T1 -> y::Int
939                 T2 -> y::Bool
940                 T3 -> h x y
941
942 We generate constraint, for (x::T alpha) and (y :: beta): 
943    [untouchables = beta] (alpha ~ Int => beta ~ Int)   -- From 1st branch
944    [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
945    (alpha ~ beta)                                      -- From 3rd branch 
946
947 If we float the equality (beta ~ Int) outside of the first implication and 
948 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
949 But if we just leave them inside the implications we unify alpha := beta and
950 solve everything.
951
952 Principle: 
953     We do not want to float equalities out which may need the given *evidence*
954     to become soluble.
955
956 Consequence: classes with functional dependencies don't matter (since there is 
957 no evidence for a fundep equality), but equality superclasses do matter (since 
958 they carry evidence).
959
960 Notice that, due to Note [Extra TcSTv Untouchables], the free unification variables 
961 of an equality that is floated out of an implication become effectively untouchables
962 for the leftover implication. This is absolutely necessary. Consider the following 
963 example. We start with two implications and a class with a functional dependency. 
964
965     class C x y | x -> y
966     instance C [a] [a]
967           
968     (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
969     (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
970
971 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2. 
972 They may react to yield that (beta := [alpha]) which can then be pushed inwards 
973 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
974 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
975 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
976
977     class C x y | x -> y where 
978      op :: x -> y -> ()
979
980     instance C [a] [a]
981
982     type family F a :: *
983
984     h :: F Int -> ()
985     h = undefined
986
987     data TEx where 
988       TEx :: a -> TEx 
989
990
991     f (x::beta) = 
992         let g1 :: forall b. b -> ()
993             g1 _ = h [x]
994             g2 z = case z of TEx y -> (h [[undefined]], op x [y])
995         in (g1 '3', g2 undefined)
996
997 Note [Extra TcsTv untouchables]
998 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
999 Whenever we are solving a bunch of flat constraints, they may contain 
1000 the following sorts of 'touchable' unification variables:
1001    
1002    (i)   Born-touchables in that scope
1003  
1004    (ii)  Simplifier-generated unification variables, such as unification 
1005          flatten variables
1006
1007    (iii) Touchables that have been floated out from some nested 
1008          implications, see Note [Float Equalities out of Implications]. 
1009
1010 Now, once we are done with solving these flats and have to move inwards to 
1011 the nested implications (perhaps for a second time), we must consider all the
1012 extra variables (categories (ii) and (iii) above) as untouchables for the 
1013 implication. Otherwise we have the danger or double unifications, as well
1014 as the danger of not ``seeing'' some unification. Example (from Trac #4494):
1015
1016    (F Int ~ uf)  /\  [untch=beta](forall a. C a => F Int ~ beta) 
1017
1018 In this example, beta is touchable inside the implication. The 
1019 first solveInteract step leaves 'uf' ununified. Then we move inside 
1020 the implication where a new constraint
1021        uf  ~  beta  
1022 emerges. We may spontaneously solve it to get uf := beta, so the whole
1023 implication disappears but when we pop out again we are left with (F
1024 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
1025 uf will get unified *once more* to (F Int).
1026
1027 The solution is to record the unification variables of the flats, 
1028 and make them untouchables for the nested implication. In the 
1029 example above uf would become untouchable, so beta would be forced 
1030 to be unified as beta := uf.
1031
1032 \begin{code}
1033 unFlattenWC :: WantedConstraints -> TcS WantedConstraints
1034 unFlattenWC wc 
1035   = do { (subst, remaining_unsolved_flats) <- solveCTyFunEqs (wc_flat wc)
1036                 -- See Note [Solving Family Equations]
1037                 -- NB: remaining_flats has already had subst applied
1038        ; return $ 
1039          WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
1040             , wc_impl  = mapBag (substImplication subst) (wc_impl wc) 
1041             , wc_insol = mapBag (substCt subst) (wc_insol wc) }
1042        }
1043   where 
1044     solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
1045     -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1046     -- See Note [Solving Family Equations]
1047     -- Returns: a bunch of unsolved constraints from the original Cts and implications
1048     --          where the newly generated equalities (alpha := F xi) have been substituted through.
1049     solveCTyFunEqs cts
1050      = do { untch   <- TcSMonad.getUntouchables 
1051           ; let (unsolved_can_cts, (ni_subst, cv_binds))
1052                     = getSolvableCTyFunEqs untch cts
1053           ; traceTcS "defaultCTyFunEqs" (vcat [ text "Trying to default family equations:"
1054                                               , text "untch" <+> ppr untch 
1055                                               , text "subst" <+> ppr ni_subst 
1056                                               , text "binds" <+> ppr cv_binds
1057                                               , ppr unsolved_can_cts
1058                                               ])
1059           ; mapM_ solve_one cv_binds
1060
1061           ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1062       where
1063         solve_one (Wanted { ctev_evar = cv }, tv, ty) 
1064           = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
1065         solve_one (Derived {}, tv, ty)
1066           = setWantedTyBind tv ty
1067         solve_one arg
1068           = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
1069
1070 ------------
1071 type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
1072   -- The TvSubstEnv is not idempotent, but is loop-free
1073   -- See Note [Non-idempotent substitution] in Unify
1074 emptyFunEqBinds :: FunEqBinds
1075 emptyFunEqBinds = (emptyVarEnv, [])
1076
1077 extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
1078 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
1079   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
1080
1081 ------------
1082 getSolvableCTyFunEqs :: Untouchables
1083                      -> Cts                -- Precondition: all Wanteds or Derived!
1084                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
1085 getSolvableCTyFunEqs untch cts
1086   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
1087   where
1088     dflt_funeq :: (Cts, FunEqBinds) -> Ct
1089                -> (Cts, FunEqBinds)
1090     dflt_funeq (cts_in, feb@(tv_subst, _))
1091                (CFunEqCan { cc_ev = fl
1092                           , cc_fun = tc
1093                           , cc_tyargs = xis
1094                           , cc_rhs = xi })
1095       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
1096
1097       , isTouchableMetaTyVar untch tv
1098            -- And it's a *touchable* unification variable
1099
1100       , typeKind xi `tcIsSubKind` tyVarKind tv
1101          -- Must do a small kind check since TcCanonical invariants 
1102          -- on family equations only impose compatibility, not subkinding
1103
1104       , not (tv `elemVarEnv` tv_subst)
1105            -- Check not in extra_binds
1106            -- See Note [Solving Family Equations], Point 1
1107
1108       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1109            -- Occurs check: see Note [Solving Family Equations], Point 2
1110       = ASSERT ( not (isGiven fl) )
1111         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
1112
1113     dflt_funeq (cts_in, fun_eq_binds) ct
1114       = (cts_in `extendCts` ct, fun_eq_binds)
1115 \end{code}
1116
1117 Note [Solving Family Equations] 
1118 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1119 After we are done with simplification we may be left with constraints of the form:
1120      [Wanted] F xis ~ beta 
1121 If 'beta' is a touchable unification variable not already bound in the TyBinds 
1122 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1123
1124 When is it ok to do so? 
1125     1) 'beta' must not already be defaulted to something. Example: 
1126
1127            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
1128            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
1129                                        have to report this as unsolved.
1130
1131     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
1132        set [beta := F xis] only if beta is not among the free variables of xis.
1133
1134     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
1135        of type family equations. See Inert Set invariants in TcInteract. 
1136
1137
1138 *********************************************************************************
1139 *                                                                               * 
1140 *                          Defaulting and disamgiguation                        *
1141 *                                                                               *
1142 *********************************************************************************
1143 \begin{code}
1144 applyDefaultingRules :: Cts      -- Wanteds or Deriveds
1145                      -> TcS Cts  -- Derived equalities 
1146 -- Return some extra derived equalities, which express the
1147 -- type-class default choice. 
1148 applyDefaultingRules wanteds
1149   | isEmptyBag wanteds 
1150   = return emptyBag
1151   | otherwise
1152   = do { traceTcS "applyDefaultingRules { " $ 
1153                   text "wanteds =" <+> ppr wanteds
1154                   
1155        ; info@(default_tys, _) <- getDefaultInfo
1156        ; let groups = findDefaultableGroups info wanteds
1157        ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
1158                                                  , text "info=" <+> ppr info ]
1159        ; deflt_cts <- mapM (disambigGroup default_tys) groups
1160
1161        ; traceTcS "applyDefaultingRules }" $ 
1162                   vcat [ text "Type defaults =" <+> ppr deflt_cts]
1163
1164        ; return (unionManyBags deflt_cts) }
1165 \end{code}
1166
1167 Note [tryTcS in defaulting]
1168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1169
1170 defaultTyVar and disambigGroup create new evidence variables for
1171 default equations, and hence update the EvVar cache. However, after
1172 applyDefaultingRules we will try to solve these default equations
1173 using solveInteractCts, which will consult the cache and solve those
1174 EvVars from themselves! That's wrong.
1175
1176 To avoid this problem we guard defaulting under a @tryTcS@ which leaves
1177 the original cache unmodified.
1178
1179 There is a second reason for @tryTcS@ in defaulting: disambGroup does
1180 some constraint solving to determine if a default equation is
1181 ``useful'' in solving some wanted constraints, but we want to
1182 discharge all evidence and unifications that may have happened during
1183 this constraint solving.
1184
1185 Finally, @tryTcS@ importantly does not inherit the original cache from
1186 the higher level but makes up a new cache, the reason is that disambigGroup
1187 will call solveInteractCts so the new derived and the wanteds must not be 
1188 in the cache!
1189
1190
1191 \begin{code}
1192 ------------------
1193 touchablesOfWC :: WantedConstraints -> TcTyVarSet
1194 -- See Note [Extra Tcs Untouchables] to see why we carry a Untouchables 
1195 -- instead of just using the Untouchable range have in our hands.
1196 touchablesOfWC 
1197   = go noUntouchables
1198   where 
1199     go :: Untouchables -> WantedConstraints -> TcTyVarSet
1200     go untch (WC { wc_flat = flats, wc_impl = impls }) 
1201       = filterVarSet is_touchable flat_tvs `unionVarSet`
1202         foldrBag (unionVarSet . go_impl) emptyVarSet impls 
1203       where 
1204          is_touchable = isTouchableMetaTyVar untch
1205          flat_tvs = tyVarsOfCts flats
1206
1207     go_impl implic = go (ic_untch implic) (ic_wanted implic)
1208
1209 applyTyVarDefaulting :: WantedConstraints -> TcM Cts
1210 applyTyVarDefaulting wc = runTcS do_dflt >>= (return . fst)
1211   where 
1212     do_dflt = do { tv_cts <- mapM defaultTyVar $ 
1213                              varSetElems (touchablesOfWC wc)
1214                  ; return (unionManyBags tv_cts) }
1215
1216 defaultTyVar :: TcTyVar -> TcS Cts
1217 -- Precondition: a touchable meta-variable
1218 defaultTyVar the_tv
1219   | not (k `eqKind` default_k)
1220   -- Why tryTcS? See Note [tryTcS in defaulting]
1221   = tryTcS $
1222     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1223        ; ty_k <- instFlexiTcSHelperTcS (tyVarName the_tv) default_k
1224        ; let derived_pred = mkTcEqPred (mkTyVarTy the_tv) ty_k
1225              -- Why not directly derived_pred = mkTcEqPred k default_k? 
1226              -- See Note [DefaultTyVar]
1227              derived_cts = unitBag $ mkNonCanonical $
1228                            Derived { ctev_wloc = loc
1229                                    , ctev_pred = derived_pred } 
1230        
1231        ; implics_from_defaulting <- solveInteract derived_cts
1232        ; MASSERT (isEmptyBag implics_from_defaulting)
1233          
1234        ; all_solved <- checkAllSolved
1235        ; if all_solved then return derived_cts
1236          else return emptyBag }
1237   | otherwise = return emptyBag  -- The common case
1238   where
1239     k = tyVarKind the_tv
1240     default_k = defaultKind k
1241 \end{code}
1242
1243 Note [DefaultTyVar]
1244 ~~~~~~~~~~~~~~~~~~~
1245 defaultTyVar is used on any un-instantiated meta type variables to
1246 default the kind of OpenKind and ArgKind etc to *.  This is important 
1247 to ensure that instance declarations match.  For example consider
1248
1249      instance Show (a->b)
1250      foo x = show (\_ -> True)
1251
1252 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
1253 and that won't match the typeKind (*) in the instance decl.  See tests
1254 tc217 and tc175.
1255
1256 We look only at touchable type variables. No further constraints
1257 are going to affect these type variables, so it's time to do it by
1258 hand.  However we aren't ready to default them fully to () or
1259 whatever, because the type-class defaulting rules have yet to run.
1260
1261 An important point is that if the type variable tv has kind k and the
1262 default is default_k we do not simply generate [D] (k ~ default_k) because:
1263
1264    (1) k may be ArgKind and default_k may be * so we will fail
1265
1266    (2) We need to rewrite all occurrences of the tv to be a type
1267        variable with the right kind and we choose to do this by rewriting 
1268        the type variable /itself/ by a new variable which does have the 
1269        right kind.
1270
1271 \begin{code}
1272 findDefaultableGroups 
1273     :: ( [Type]
1274        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1275     -> Cts              -- Unsolved (wanted or derived)
1276     -> [[(Ct,Class,TcTyVar)]]
1277 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
1278   | null default_tys             = []
1279   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1280   where 
1281     unaries     :: [(Ct, Class, TcTyVar)]  -- (C tv) constraints
1282     non_unaries :: [Ct]             -- and *other* constraints
1283     
1284     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1285         -- Finds unary type-class constraints
1286     find_unary cc 
1287         | Just (cls,[ty]) <- getClassPredTys_maybe (ctPred cc)
1288         , Just tv <- tcGetTyVar_maybe ty
1289         = Left (cc, cls, tv)
1290     find_unary cc = Right cc  -- Non unary or non dictionary 
1291
1292     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
1293     bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries 
1294
1295     cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
1296
1297     is_defaultable_group ds@((_,_,tv):_)
1298         = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
1299               b2 = not (tv `elemVarSet` bad_tvs)
1300               b4 = defaultable_classes [cls | (_,cls,_) <- ds]
1301           in (b1 && b2 && b4)
1302     is_defaultable_group [] = panic "defaultable_group"
1303
1304     defaultable_classes clss 
1305         | extended_defaults = any isInteractiveClass clss
1306         | otherwise         = all is_std_class clss && (any is_num_class clss)
1307
1308     -- In interactive mode, or with -XExtendedDefaultRules,
1309     -- we default Show a to Show () to avoid graututious errors on "show []"
1310     isInteractiveClass cls 
1311         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1312
1313     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1314     -- is_num_class adds IsString to the standard numeric classes, 
1315     -- when -foverloaded-strings is enabled
1316
1317     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1318     -- Similarly is_std_class
1319
1320 ------------------------------
1321 disambigGroup :: [Type]                  -- The default types 
1322               -> [(Ct, Class, TcTyVar)]  -- All classes of the form (C a)
1323                                          --  sharing same type variable
1324               -> TcS Cts
1325
1326 disambigGroup []  _grp
1327   = return emptyBag
1328 disambigGroup (default_ty:default_tys) group
1329   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1330        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
1331                     do { let derived_pred = mkTcEqPred (mkTyVarTy the_tv) default_ty
1332                              derived_cts = unitBag $ mkNonCanonical $
1333                                            Derived { ctev_wloc = the_loc
1334                                                    , ctev_pred = derived_pred }
1335                             
1336                        ; traceTcS "disambigGroup (solving) {" $
1337                          text "trying to solve constraints along with default equations ..."
1338                        ; implics_from_defaulting <- 
1339                                     solveInteract (derived_cts `unionBags` wanteds)
1340                        ; MASSERT (isEmptyBag implics_from_defaulting)
1341                            -- I am not certain if any implications can be generated
1342                            -- but I am letting this fail aggressively if this ever happens.
1343                                      
1344                        ; all_solved <- checkAllSolved
1345                        ; traceTcS "disambigGroup (solving) }" $
1346                          text "disambigGroup solved =" <+> ppr all_solved
1347                        ; if all_solved then
1348                              return (Just derived_cts) 
1349                          else 
1350                              return Nothing 
1351                        }
1352        ; case success of
1353            Just cts -> -- Success: record the type variable binding, and return
1354                     do { wrapWarnTcS $ warnDefaulting wanteds default_ty
1355                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1356                        ; return cts }
1357            Nothing -> -- Failure: try with the next type
1358                     do { traceTcS "disambigGroup failed, will try other default types"
1359                                   (ppr default_ty)
1360                        ; disambigGroup default_tys group } }
1361   where
1362     ((the_ct,_,the_tv):_) = group
1363     the_fl                = cc_ev the_ct
1364     the_loc               = ctev_wloc the_fl
1365     wanteds               = listToBag (map fstOf3 group)
1366 \end{code}
1367
1368 Note [Avoiding spurious errors]
1369 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1370 When doing the unification for defaulting, we check for skolem
1371 type variables, and simply don't default them.  For example:
1372    f = (*)      -- Monomorphic
1373    g :: Num a => a -> a
1374    g x = f x x
1375 Here, we get a complaint when checking the type signature for g,
1376 that g isn't polymorphic enough; but then we get another one when
1377 dealing with the (Num a) context arising from f's definition;
1378 we try to unify a with Int (to default it), but find that it's
1379 already been unified with the rigid variable from g's type sig
1380
1381
1382
1383 *********************************************************************************
1384 *                                                                               * 
1385 *                   Utility functions
1386 *                                                                               *
1387 *********************************************************************************
1388
1389 \begin{code}
1390 newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
1391 newFlatWanteds orig theta
1392   = do { loc <- getCtLoc orig
1393        ; mapM (inst_to_wanted loc) theta }
1394   where 
1395     inst_to_wanted loc pty 
1396           = do { v <- TcMType.newWantedEvVar pty 
1397                ; return $ 
1398                  CNonCanonical { cc_ev = Wanted { ctev_evar = v
1399                                                 , ctev_wloc = loc
1400                                                 , ctev_pred = pty }
1401                                , cc_depth = 0 } }
1402 \end{code}