Implement Partial Type Signatures
[ghc.git] / compiler / typecheck / TcSMonad.lhs
1 \begin{code}
2 {-# LANGUAGE CPP, TypeFamilies #-}
3
4 -- Type definitions for the constraint solver
5 module TcSMonad (
6
7        -- Canonical constraints, definition is now in TcRnTypes
8
9     WorkList(..), isEmptyWorkList, emptyWorkList,
10     extendWorkListFunEq,
11     extendWorkListNonEq, extendWorkListCt,
12     extendWorkListCts, appendWorkList, selectWorkItem,
13     workListSize,
14
15     updWorkListTcS, updWorkListTcS_return,
16
17     updInertTcS, updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
18
19     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
20     emitInsoluble, emitWorkNC,
21
22     isWanted, isDerived,
23     isGivenCt, isWantedCt, isDerivedCt,
24
25     mkGivenLoc,
26
27     TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
28     traceFireTcS, bumpStepCountTcS, csTraceTcS,
29     tryTcS, nestTcS, nestImplicTcS, recoverTcS,
30     wrapErrTcS, wrapWarnTcS,
31     runTcPluginTcS,
32
33     -- Getting and setting the flattening cache
34     addSolvedDict, 
35
36     -- Marking stuff as used
37     addUsedRdrNamesTcS,
38
39     deferTcSForAllEq,
40
41     setEvBind,
42     XEvTerm(..),
43     Freshness(..), freshGoals, 
44
45     StopOrContinue(..), continueWith, stopWith, andWhenContinue,
46
47     xCtEvidence,        -- Transform a CtEvidence during a step
48     rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
49     rewriteEqEvidence,  -- Yet more specialised, for equality coercions
50     maybeSym,
51
52     newTcEvBinds, newWantedEvVar, newWantedEvVarNC, 
53     newEvVar, newGivenEvVar, 
54     emitNewDerived, emitNewDerivedEq,
55     instDFunConstraints,
56
57        -- Creation of evidence variables
58     setWantedTyBind, reportUnifications,
59
60     getInstEnvs, getFamInstEnvs,                -- Getting the environments
61     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
62     getTcEvBindsMap, 
63
64     lookupFlatCache, newFlattenSkolem,            -- Flatten skolems
65
66         -- Deque
67     Deque(..), insertDeque, emptyDeque,
68
69         -- Inerts
70     InertSet(..), InertCans(..),
71     getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
72     emptyInert, getTcSInerts, setTcSInerts, 
73     getUnsolvedInerts, checkAllSolved,
74     splitInertCans, removeInertCts,
75     prepareInertsForImplications,
76     addInertCan, insertInertItemTcS, insertFunEq,
77     EqualCtList,
78     lookupSolvedDict, extendFlatCache,
79
80     lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
81
82     findFunEq, findTyEqs,
83     findFunEqsByTyCon, findFunEqs, partitionFunEqs,
84     sizeFunEqMap,
85
86     instDFunType,                              -- Instantiation
87     newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
88     cloneMetaTyVar, demoteUnfilledFmv,
89
90     Untouchables, isTouchableMetaTyVarTcS,
91     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
92     zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
93
94     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
95
96     matchFam,
97     checkWellStagedDFun,
98     pprEq                                    -- Smaller utils, re-exported from TcM
99                                              -- TODO (DV): these are only really used in the
100                                              -- instance matcher in TcSimplify. I am wondering
101                                              -- if the whole instance matcher simply belongs
102                                              -- here
103 ) where
104
105 #include "HsVersions.h"
106
107 import HscTypes
108
109 import Inst
110 import InstEnv
111 import FamInst
112 import FamInstEnv
113
114 import qualified TcRnMonad as TcM
115 import qualified TcMType as TcM
116 import qualified TcEnv as TcM
117        ( checkWellStaged, topIdLvl, tcGetDefaultTys )
118 import Kind
119 import TcType
120 import DynFlags
121 import Type
122 import CoAxiom(sfMatchFam)
123
124 import TcEvidence
125 import Class
126 import TyCon
127
128 import Name
129 import RdrName (RdrName, GlobalRdrEnv)
130 import RnEnv (addUsedRdrNames)
131 import Var
132 import VarEnv
133 import VarSet
134 import Outputable
135 import Bag
136 import UniqSupply
137
138 import FastString
139 import Util
140 import Id
141 import TcRnTypes
142
143 import BasicTypes
144 import Unique
145 import UniqFM
146 import Maybes ( orElse, firstJusts )
147
148 import TrieMap
149 import Control.Monad( ap, when, unless )
150 import MonadUtils
151 import Data.IORef
152 import Data.List ( partition, foldl' )
153 import Pair
154
155 #ifdef DEBUG
156 import Digraph
157 #endif
158 \end{code}
159
160 %************************************************************************
161 %*                                                                      *
162 %*                            Worklists                                *
163 %*  Canonical and non-canonical constraints that the simplifier has to  *
164 %*  work on. Including their simplification depths.                     *
165 %*                                                                      *
166 %*                                                                      *
167 %************************************************************************
168
169 Note [WorkList priorities]
170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
171 A WorkList contains canonical and non-canonical items (of all flavors).
172 Notice that each Ct now has a simplification depth. We may
173 consider using this depth for prioritization as well in the future.
174
175 As a simple form of priority queue, our worklist separates out
176 equalities (wl_eqs) from the rest of the canonical constraints,
177 so that it's easier to deal with them first, but the separation
178 is not strictly necessary. Notice that non-canonical constraints
179 are also parts of the worklist.
180
181
182 \begin{code}
183 data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
184                             -- First to remove is at head of LH field
185
186 instance Outputable a => Outputable (Deque a) where
187   ppr q = ppr (dequeList q)
188
189 dequeList :: Deque a -> [a]
190 dequeList (DQ as bs) = as ++ reverse bs  -- First one to come out at the start
191
192 emptyDeque :: Deque a
193 emptyDeque = DQ [] []
194
195 isEmptyDeque :: Deque a -> Bool
196 isEmptyDeque (DQ as bs) = null as && null bs
197
198 dequeSize :: Deque a -> Int
199 dequeSize (DQ as bs) = length as + length bs
200
201 insertDeque :: a -> Deque a -> Deque a
202 insertDeque b (DQ as bs) = DQ as (b:bs)
203
204 appendDeque :: Deque a -> Deque a -> Deque a
205 appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
206
207 extractDeque :: Deque a -> Maybe (Deque a, a)
208 extractDeque (DQ [] [])     = Nothing
209 extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
210 extractDeque (DQ [] bs)     = case reverse bs of
211                                 (a:as) -> Just (DQ as [], a)
212                                 [] -> panic "extractDeque"
213
214 -- See Note [WorkList priorities]
215 data WorkList 
216   = WL { wl_eqs     :: [Ct]
217        , wl_funeqs  :: Deque Ct
218        , wl_rest    :: [Ct]
219        , wl_implics :: Bag Implication  -- See Note [Residual implications]
220     }
221
222 appendWorkList :: WorkList -> WorkList -> WorkList
223 appendWorkList 
224     (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
225     (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
226    = WL { wl_eqs     = eqs1     ++            eqs2
227         , wl_funeqs  = funeqs1  `appendDeque` funeqs2
228         , wl_rest    = rest1    ++            rest2
229         , wl_implics = implics1 `unionBags`   implics2 }
230
231
232 workListSize :: WorkList -> Int
233 workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
234   = length eqs + dequeSize funeqs + length rest
235
236 extendWorkListEq :: Ct -> WorkList -> WorkList
237 extendWorkListEq ct wl 
238   = wl { wl_eqs = ct : wl_eqs wl }
239
240 extendWorkListFunEq :: Ct -> WorkList -> WorkList
241 extendWorkListFunEq ct wl
242   = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
243
244 extendWorkListNonEq :: Ct -> WorkList -> WorkList
245 -- Extension by non equality
246 extendWorkListNonEq ct wl
247   = wl { wl_rest = ct : wl_rest wl }
248
249 extendWorkListImplic :: Implication -> WorkList -> WorkList
250 extendWorkListImplic implic wl
251   = wl { wl_implics = implic `consBag` wl_implics wl }
252
253 extendWorkListCt :: Ct -> WorkList -> WorkList
254 -- Agnostic
255 extendWorkListCt ct wl
256  = case classifyPredType (ctPred ct) of
257      EqPred ty1 _
258        | Just (tc,_) <- tcSplitTyConApp_maybe ty1
259        , isTypeFamilyTyCon tc
260        -> extendWorkListFunEq ct wl
261        | otherwise
262        -> extendWorkListEq ct wl
263
264      _ -> extendWorkListNonEq ct wl
265
266 extendWorkListCts :: [Ct] -> WorkList -> WorkList
267 -- Agnostic
268 extendWorkListCts cts wl = foldr extendWorkListCt wl cts
269
270 isEmptyWorkList :: WorkList -> Bool
271 isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
272                     , wl_rest = rest, wl_implics = implics })
273   = null eqs && null rest && isEmptyDeque funeqs && isEmptyBag implics
274
275 emptyWorkList :: WorkList
276 emptyWorkList = WL { wl_eqs  = [], wl_rest = []
277                    , wl_funeqs = emptyDeque, wl_implics = emptyBag }
278
279 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
280 selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
281   = case (eqs,feqs,rest) of
282       (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
283       (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
284                        -> (Just ct, wl { wl_funeqs = fun_eqs' })
285       (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
286       (_,_,_)          -> (Nothing,wl)
287
288 -- Pretty printing
289 instance Outputable WorkList where
290   ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
291           , wl_rest = rest, wl_implics = implics })
292    = text "WL" <+> (braces $
293      vcat [ ppUnless (null eqs) $ 
294             ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
295           , ppUnless (isEmptyDeque feqs) $
296             ptext (sLit "Funeqs =") <+> vcat (map ppr (dequeList feqs))
297           , ppUnless (null rest) $
298             ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
299           , ppUnless (isEmptyBag implics) $
300             ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
301           ])
302 \end{code}
303
304 %************************************************************************
305 %*                                                                      *
306 %*                            Inert Sets                                *
307 %*                                                                      *
308 %*                                                                      *
309 %************************************************************************
310
311 Note [Detailed InertCans Invariants]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
313 The InertCans represents a collection of constraints with the following properties:
314
315   * All canonical
316
317   * No two dictionaries with the same head
318   * No two CIrreds with the same type
319
320   * Family equations inert wrt top-level family axioms
321
322   * Dictionaries have no matching top-level instance
323
324   * Given family or dictionary constraints don't mention touchable
325     unification variables
326
327   * Non-CTyEqCan constraints are fully rewritten with respect
328     to the CTyEqCan equalities (modulo canRewrite of course;
329     eg a wanted cannot rewrite a given)
330
331   * CTyEqCan equalities: see Note [Applying the inert substitution]
332                          in TcFlatten
333
334 Note [Type family equations]
335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
336 Type-family equations, of form (ev : F tys ~ ty), live in three places
337
338   * The work-list, of course
339
340   * The inert_flat_cache.  This is used when flattening, to get maximal
341     sharing.  It contains lots of things that are still in the work-list.
342     E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
343         work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
344         list.  Now if we flatten w2 before we get to w3, we still want to
345         share that (G a).
346
347     Because it contains work-list things, DO NOT use the flat cache to solve
348     a top-level goal.  Eg in the above example we don't want to solve w3
349     using w3 itself!
350
351   * The inert_funeqs are un-solved but fully processed and in the InertCans.
352
353 \begin{code}
354 -- All Given (fully known) or Wanted or Derived
355 -- See Note [Detailed InertCans Invariants] for more
356 data InertCans
357   = IC { inert_eqs :: TyVarEnv EqualCtList
358               -- All CTyEqCans; index is the LHS tyvar
359
360        , inert_funeqs :: FunEqMap Ct
361               -- All CFunEqCans; index is the whole family head type.
362
363        , inert_dicts :: DictMap Ct
364               -- Dictionaries only, index is the class
365               -- NB: index is /not/ the whole type because FD reactions
366               -- need to match the class but not necessarily the whole type.
367
368        , inert_irreds :: Cts
369               -- Irreducible predicates
370
371        , inert_insols :: Cts
372               -- Frozen errors (as non-canonicals)
373        }
374
375 type EqualCtList = [Ct]
376 -- EqualCtList invariants:
377 --    * All are equalities
378 --    * All these equalities have the same LHS
379 --    * The list is never empty
380 --    * No element of the list can rewrite any other
381 --
382 -- From the fourth invariant it follows that the list is
383 --   - A single Given, or
384 --   - Multiple Wanteds, or
385 --   - Multiple Deriveds
386
387 -- The Inert Set
388 data InertSet
389   = IS { inert_cans :: InertCans
390               -- Canonical Given, Wanted, Derived (no Solved)
391               -- Sometimes called "the inert set"
392
393        , inert_flat_cache :: FunEqMap (TcCoercion, TcTyVar)
394               -- See Note [Type family equations]
395               -- If    F tys :-> (co, fsk), 
396               -- then  co :: F tys ~ fsk
397               -- Just a hash-cons cache for use when flattening only
398               -- These include entirely un-processed goals, so don't use
399               -- them to solve a top-level goal, else you may end up solving
400               -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
401               -- when allocating a new flatten-skolem.
402               -- Not necessarily inert wrt top-level equations (or inert_cans)
403
404        , inert_solved_dicts   :: DictMap CtEvidence
405               -- Of form ev :: C t1 .. tn
406               -- Always the result of using a top-level instance declaration
407               -- See Note [Solved constraints]
408               -- - Used to avoid creating a new EvVar when we have a new goal
409               --   that we have solved in the past
410               -- - Stored not necessarily as fully rewritten
411               --   (ToDo: rewrite lazily when we lookup)
412        }
413 \end{code}
414
415 \begin{code}
416 instance Outputable InertCans where
417   ppr ics = vcat [ ptext (sLit "Equalities:")
418                    <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
419                                           emptyCts (inert_eqs ics))
420                  , ptext (sLit "Type-function equalities:")
421                    <+> pprCts (funEqsToBag (inert_funeqs ics))
422                  , ptext (sLit "Dictionaries:")
423                    <+> pprCts (dictsToBag (inert_dicts ics))
424                  , ptext (sLit "Irreds:")
425                    <+> pprCts (inert_irreds ics)
426                  , text "Insolubles =" <+> -- Clearly print frozen errors
427                     braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
428                  ]
429
430 instance Outputable InertSet where
431   ppr is = vcat [ ppr $ inert_cans is
432                 , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
433
434 emptyInert :: InertSet
435 emptyInert
436   = IS { inert_cans = IC { inert_eqs     = emptyVarEnv
437                          , inert_dicts   = emptyDicts
438                          , inert_funeqs  = emptyFunEqs
439                          , inert_irreds  = emptyCts
440                          , inert_insols  = emptyCts
441                          }
442        , inert_flat_cache    = emptyFunEqs
443        , inert_solved_dicts  = emptyDictMap }
444
445 ---------------
446 addInertCan :: InertCans -> Ct -> InertCans
447 -- Precondition: item /is/ canonical
448 addInertCan ics item@(CTyEqCan {})
449   = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
450                               (inert_eqs ics)
451                               (cc_tyvar item) [item] }
452
453 addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
454   = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
455
456 addInertCan ics item@(CIrredEvCan {})
457   = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
458        -- The 'False' is because the irreducible constraint might later instantiate
459        -- to an equality.
460        -- But since we try to simplify first, if there's a constraint function FC with
461        --    type instance FC Int = Show
462        -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
463
464 addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
465   = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
466
467 addInertCan _ item
468   = pprPanic "upd_inert set: can't happen! Inserting " $
469     ppr item   -- Can't be CNonCanonical, CHoleCan,
470                -- because they only land in inert_insols
471
472 --------------
473 insertInertItemTcS :: Ct -> TcS ()
474 -- Add a new item in the inerts of the monad
475 insertInertItemTcS item
476   = do { traceTcS "insertInertItemTcS {" $
477          text "Trying to insert new inert item:" <+> ppr item
478
479        ; updInertCans (\ics -> addInertCan ics item)
480
481        ; traceTcS "insertInertItemTcS }" $ empty }
482
483 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
484 -- Add a new item in the solved set of the monad
485 addSolvedDict item cls tys
486   | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
487   = return ()
488   | otherwise
489   = do { traceTcS "updSolvedSetTcs:" $ ppr item
490        ; updInertTcS $ \ ics ->
491              ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
492
493 updInertTcS :: (InertSet -> InertSet) -> TcS ()
494 -- Modify the inert set with the supplied function
495 updInertTcS upd_fn
496   = do { is_var <- getTcSInertsRef
497        ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
498                      ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
499
500 getInertCans :: TcS InertCans
501 getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
502
503 setInertCans :: InertCans -> TcS ()
504 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
505
506 updInertCans :: (InertCans -> InertCans) -> TcS ()
507 -- Modify the inert set with the supplied function
508 updInertCans upd_fn
509   = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
510
511 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
512 -- Modify the inert set with the supplied function
513 updInertDicts upd_fn
514   = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
515
516 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
517 -- Modify the inert set with the supplied function
518 updInertFunEqs upd_fn
519   = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
520
521 updInertIrreds :: (Cts -> Cts) -> TcS ()
522 -- Modify the inert set with the supplied function
523 updInertIrreds upd_fn
524   = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
525
526
527 prepareInertsForImplications :: InertSet -> (InertSet)
528 -- See Note [Preparing inert set for implications]
529 prepareInertsForImplications is@(IS { inert_cans = cans })
530   = is { inert_cans       = getGivens cans
531        , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
532   where
533     getGivens (IC { inert_eqs    = eqs
534                   , inert_irreds = irreds
535                   , inert_funeqs = funeqs
536                   , inert_dicts  = dicts })
537       = IC { inert_eqs     = filterVarEnv  is_given_ecl eqs
538            , inert_funeqs  = filterFunEqs  isGivenCt funeqs
539            , inert_irreds  = Bag.filterBag isGivenCt irreds
540            , inert_dicts   = filterDicts   isGivenCt dicts
541            , inert_insols  = emptyCts }
542
543     is_given_ecl :: EqualCtList -> Bool
544     is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
545     is_given_ecl _                        = False
546 \end{code}
547
548 Note [Do not inherit the flat cache]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 We do not want to inherit the flat cache when processing nested
551 implications.  Consider
552    a ~ F b, forall c. b~Int => blah
553 If we have F b ~ fsk in the flat-cache, and we push that into the
554 nested implication, we might miss that F b can be rewritten to F Int,
555 and hence perhpas solve it.  Moreover, the fsk from outside is 
556 flattened out after solving the outer level, but and we don't 
557 do that flattening recursively.
558
559 Note [Preparing inert set for implications]
560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
561 Before solving the nested implications, we trim the inert set,
562 retaining only Givens.  These givens can be used when solving
563 the inner implications.
564
565 There might be cases where interactions between wanteds at different levels
566 could help to solve a constraint. For example
567
568         class C a b | a -> b
569         (C Int alpha), (forall d. C d blah => C Int a)
570
571 If we pushed the (C Int alpha) inwards, as a given, it can produce a
572 fundep (alpha~a) and this can float out again and be used to fix
573 alpha.  (In general we can't float class constraints out just in case
574 (C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
575
576 For Derived constraints we don't have evidence, so we do not turn
577 them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
578
579 \begin{code}
580 getInertEqs :: TcS (TyVarEnv EqualCtList)
581 getInertEqs = do { inert <- getTcSInerts
582                  ; return (inert_eqs (inert_cans inert)) }
583
584 getUnsolvedInerts :: TcS ( Bag Implication
585                          , Cts     -- Tyvar eqs: a ~ ty
586                          , Cts     -- Fun eqs:   F a ~ ty
587                          , Cts     -- Insoluble
588                          , Cts )   -- All others
589 getUnsolvedInerts
590  = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs
591            , inert_irreds = irreds, inert_dicts = idicts
592            , inert_insols = insols } <- getInertCans
593
594       ; let unsolved_tv_eqs  = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts)
595                                           emptyCts tv_eqs
596             unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
597             unsolved_irreds  = Bag.filterBag is_unsolved irreds
598             unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
599             others = unsolved_irreds `unionBags` unsolved_dicts
600
601       ; implics <- getWorkListImplics
602
603       ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
604               -- Keep even the given insolubles
605               -- so that we can report dead GADT pattern match branches
606   where
607     add_if_unsolved :: Ct -> Cts -> Cts
608     add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
609                            | otherwise      = cts
610
611     is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived
612
613 getNoGivenEqs :: Untouchables     -- Untouchables of this implication
614                -> [TcTyVar]       -- Skolems of this implication
615                -> TcS Bool        -- True <=> definitely no residual given equalities
616 -- See Note [When does an implication have given equalities?]
617 getNoGivenEqs untch skol_tvs
618   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
619              <- getInertCans
620        ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
621
622              has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence)  False iirreds
623                           || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
624
625        ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
626        ; return (not has_given_eqs) }
627   where
628     eqs_given_here :: VarSet -> EqualCtList -> Bool
629     eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
630                               -- Givens are always a sigleton
631       = not (skolem_bound_here local_fsks tv) && ev_given_here ev
632     eqs_given_here _ _ = False
633
634     ev_given_here :: CtEvidence -> Bool
635     -- True for a Given bound by the curent implication,
636     -- i.e. the current level
637     ev_given_here ev
638       =  isGiven ev
639       && untch == tcl_untch (ctl_env (ctEvLoc ev))
640
641     add_fsk :: Ct -> VarSet -> VarSet
642     add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
643                     , isGiven ev = extendVarSet fsks tv
644                     | otherwise  = fsks
645
646     skol_tv_set = mkVarSet skol_tvs
647     skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
648       = case tcTyVarDetails tv of
649           SkolemTv {} -> tv `elemVarSet` skol_tv_set
650           FlatSkol {} -> not (tv `elemVarSet` local_fsks)
651           _           -> False
652 \end{code}
653
654 Note [When does an implication have given equalities?]
655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 Consider an implication
657    beta => alpha ~ Int
658 where beta is a unification variable that has already been unified
659 to () in an outer scope.  Then we can float the (alpha ~ Int) out
660 just fine. So when deciding whether the givens contain an equality,
661 we should canonicalise first, rather than just looking at the original
662 givens (Trac #8644).
663
664 So we simply look at the inert, canonical Givens and see if there are
665 any equalities among them, the calculation of has_given_eqs.  There
666 are some wrinkles:
667
668  * We must know which ones are bound in *this* implication and which
669    are bound further out.  We can find that out from the Untouchable
670    level of the Given, which is itself recorded in the tcl_untch field
671    of the TcLclEnv stored in the Given (ev_given_here).
672
673    What about interactions between inner and outer givens?
674       - Outer given is rewritten by an inner given, then there must
675         have been an inner given equality, hence the “given-eq” flag
676         will be true anyway.
677
678       - Inner given rewritten by outer, retains its level (ie. The inner one)
679
680  * We must take account of *potential* equalities, like the one above:
681       beta => ...blah...
682    If we still don't know what beta is, we conservatively treat it as potentially
683    becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
684
685  * When flattening givens, we generate Given equalities like
686      <F [a]> : F [a] ~ f,
687    with Refl evidence, and we *don't* want those to count as an equality
688    in the givens!  After all, the entire flattening business is just an
689    internal matter, and the evidence does not mention any of the 'givens'
690    of this implication.  So we do not treat inert_funeqs as a 'given equality'.
691
692  * See Note [Let-bound skolems] for another wrinkle
693
694 Note [Let-bound skolems]
695 ~~~~~~~~~~~~~~~~~~~~~~~~
696 If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
697 and  * 'a' is a skolem bound in this very implication, b
698
699 then:
700 a) The Given is pretty much a let-binding, like
701       f :: (a ~ b->c) => a -> a
702    Here the equality constraint is like saying
703       let a = b->c in ...
704    It is not adding any new, local equality  information,
705    and hence can be ignored by has_given_eqs
706
707 b) 'a' will have been completely substituted out in the inert set,
708    so we can safely discard it.  Notably, it doesn't need to be
709    returned as part of 'fsks'
710
711 For an example, see Trac #9211.
712
713 \begin{code}
714 splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
715 -- ^ Extract the (given, derived, wanted) inert constraints
716 splitInertCans iCans = (given,derived,wanted)
717   where
718     allCts   = foldDicts  (:) (inert_dicts iCans)
719              $ foldFunEqs (:) (inert_funeqs iCans)
720              $ concat (varEnvElts (inert_eqs iCans))
721
722     (derived,other) = partition isDerivedCt allCts
723     (wanted,given)  = partition isWantedCt  other
724
725 removeInertCts :: [Ct] -> InertCans -> InertCans
726 -- ^ Remove inert constraints from the 'InertCans', for use when a
727 -- typechecker plugin wishes to discard a given.
728 removeInertCts cts icans = foldl' removeInertCt icans cts
729
730 removeInertCt :: InertCans -> Ct -> InertCans
731 removeInertCt is ct =
732   case ct of
733
734     CDictCan  { cc_class = cl, cc_tyargs = tys } ->
735       is { inert_dicts = delDict (inert_dicts is) cl tys }
736
737     CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
738       is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
739
740     CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
741       is { inert_eqs = delTyEq (inert_eqs is) x ty }
742
743     CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
744     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
745     CHoleCan {}      -> panic "removeInertCt: CHoleCan"
746
747
748 checkAllSolved :: TcS Bool
749 -- True if there are no unsolved wanteds
750 -- Ignore Derived for this purpose, unless in insolubles
751 checkAllSolved
752  = do { is <- getTcSInerts
753
754       ; let icans = inert_cans is
755             unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
756             unsolved_dicts  = foldDicts ((||)  . isWantedCt) (inert_dicts icans)  False
757             unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False
758             unsolved_eqs    = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans)
759
760       ; return (not (unsolved_eqs || unsolved_irreds
761                      || unsolved_dicts || unsolved_funeqs
762                      || not (isEmptyBag (inert_insols icans)))) }
763
764 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcTyVar))
765 lookupFlatCache fam_tc tys
766   = do { IS { inert_flat_cache = flat_cache
767             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
768        ; return (firstJusts [lookup_inerts inert_funeqs,
769                              lookup_flats flat_cache]) }
770   where
771     lookup_inerts inert_funeqs
772       | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
773            <- findFunEqs inert_funeqs fam_tc tys
774       = Just (ctEvCoercion ctev, fsk)
775       | otherwise = Nothing
776
777     lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
778
779
780 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
781 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
782 lookupInInerts loc pty
783   = do { inerts <- getTcSInerts
784        ; return $ case (classifyPredType pty) of
785            ClassPred cls tys
786               | Just ev <- lookupSolvedDict inerts loc cls tys
787               -> Just ev
788               | otherwise
789               -> lookupInertDict (inert_cans inerts) loc cls tys
790
791            _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
792       }
793
794 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
795 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
796   = case findDict dicts cls tys of
797       Just ct | let ev = ctEvidence ct
798               , ctEvCheckDepth cls loc ev
799               -> Just ev
800       _       -> Nothing
801
802 lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
803 -- Returns just if exactly this predicate type exists in the solved.
804 lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
805   = case findDict solved cls tys of
806       Just ev | ctEvCheckDepth cls loc ev -> Just ev
807       _                                   -> Nothing
808 \end{code}
809
810
811 %************************************************************************
812 %*                                                                      *
813                    TyEqMap
814 %*                                                                      *
815 %************************************************************************
816
817 \begin{code}
818 type TyEqMap a = TyVarEnv a
819
820 findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
821 findTyEqs m tv = lookupVarEnv m tv `orElse` []
822
823 delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
824 delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
825   where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
826         isThisOne _                          = False
827 \end{code}
828
829
830 %************************************************************************
831 %*                                                                      *
832                    TcAppMap, DictMap, FunEqMap
833 %*                                                                      *
834 %************************************************************************
835
836 \begin{code}
837 type TcAppMap a = UniqFM (ListMap TypeMap a)
838     -- Indexed by tycon then the arg types
839     -- Used for types and classes; hence UniqFM
840
841 emptyTcAppMap :: TcAppMap a
842 emptyTcAppMap = emptyUFM
843
844 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
845 findTcApp m u tys = do { tys_map <- lookupUFM m u
846                        ; lookupTM tys tys_map }
847
848 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
849 delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
850
851 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
852 insertTcApp m cls tys ct = alterUFM alter_tm m cls
853   where
854     alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
855
856 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
857 -- mapTcApp f = mapUFM (mapTM f)
858
859 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
860 filterTcAppMap f m
861   = mapUFM do_tm m
862   where
863     do_tm tm = foldTM insert_mb tm emptyTM
864     insert_mb ct tm
865        | f ct      = insertTM tys ct tm
866        | otherwise = tm
867        where
868          tys = case ct of
869                 CFunEqCan { cc_tyargs = tys } -> tys
870                 CDictCan  { cc_tyargs = tys } -> tys
871                 _ -> pprPanic "filterTcAppMap" (ppr ct)
872
873 tcAppMapToBag :: TcAppMap a -> Bag a
874 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
875
876 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
877 foldTcAppMap k m z = foldUFM (foldTM k) z m
878
879 -------------------------
880 type DictMap a = TcAppMap a
881
882 emptyDictMap :: DictMap a
883 emptyDictMap = emptyTcAppMap
884
885 -- sizeDictMap :: DictMap a -> Int
886 -- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
887
888 findDict :: DictMap a -> Class -> [Type] -> Maybe a
889 findDict m cls tys = findTcApp m (getUnique cls) tys
890
891 findDictsByClass :: DictMap a -> Class -> Bag a
892 findDictsByClass m cls
893   | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
894   | otherwise                  = emptyBag
895
896 delDict :: DictMap a -> Class -> [Type] -> DictMap a
897 delDict m cls tys = delTcApp m (getUnique cls) tys
898
899 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
900 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
901
902 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
903 addDictsByClass m cls items
904   = addToUFM m cls (foldrBag add emptyTM items)
905   where
906     add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
907     add ct _ = pprPanic "addDictsByClass" (ppr ct)
908
909 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
910 filterDicts f m = filterTcAppMap f m
911
912 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
913 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
914   where
915     k ct (yeses, noes) | f ct      = (ct `consBag` yeses, noes)
916                        | otherwise = (yeses,              add ct noes)
917     add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
918       = addDict m cls tys ct
919     add ct _ = pprPanic "partitionDicts" (ppr ct)
920
921 dictsToBag :: DictMap a -> Bag a
922 dictsToBag = tcAppMapToBag
923
924 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
925 foldDicts = foldTcAppMap
926
927 emptyDicts :: DictMap a
928 emptyDicts = emptyTcAppMap
929
930 ------------------------
931 type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
932
933 emptyFunEqs :: TcAppMap a
934 emptyFunEqs = emptyTcAppMap
935
936 sizeFunEqMap :: FunEqMap a -> Int
937 sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
938
939 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
940 findFunEq m tc tys = findTcApp m (getUnique tc) tys
941
942 findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
943 findFunEqs m tc tys = findTcApp m (getUnique tc) tys
944
945 funEqsToBag :: FunEqMap a -> Bag a
946 funEqsToBag m = foldTcAppMap consBag m emptyBag
947
948 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
949 -- Get inert function equation constraints that have the given tycon
950 -- in their head.  Not that the constraints remain in the inert set.
951 -- We use this to check for derived interactions with built-in type-function
952 -- constructors.
953 findFunEqsByTyCon m tc
954   | Just tm <- lookupUFM m tc = foldTM (:) tm []
955   | otherwise                 = []
956
957 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
958 foldFunEqs = foldTcAppMap
959
960 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
961 -- mapFunEqs = mapTcApp
962
963 filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
964 filterFunEqs = filterTcAppMap
965
966 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
967 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
968
969 insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
970 insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
971   = insertFunEq m tc tys ct
972 insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
973
974 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> (Bag Ct, FunEqMap Ct)
975 partitionFunEqs f m = foldTcAppMap k m (emptyBag, emptyFunEqs)
976   where
977     k ct (yeses, noes)
978       | f ct      = (yeses `snocBag` ct, noes)
979       | otherwise = (yeses, insertFunEqCt noes ct)
980
981 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
982 delFunEq m tc tys = delTcApp m (getUnique tc) tys
983 \end{code}
984
985
986 %************************************************************************
987 %*                                                                      *
988 %*              The TcS solver monad                                    *
989 %*                                                                      *
990 %************************************************************************
991
992 Note [The TcS monad]
993 ~~~~~~~~~~~~~~~~~~~~
994 The TcS monad is a weak form of the main Tc monad
995
996 All you can do is
997     * fail
998     * allocate new variables
999     * fill in evidence variables
1000
1001 Filling in a dictionary evidence variable means to create a binding
1002 for it, so TcS carries a mutable location where the binding can be
1003 added.  This is initialised from the innermost implication constraint.
1004
1005 \begin{code}
1006 data TcSEnv
1007   = TcSEnv {
1008       tcs_ev_binds    :: EvBindsVar,
1009
1010       tcs_unified :: IORef Bool,
1011           -- The "dirty-flag" Bool is set True when 
1012           -- we unify a unification variable
1013
1014       tcs_count    :: IORef Int, -- Global step count
1015
1016       tcs_inerts   :: IORef InertSet, -- Current inert set
1017       tcs_worklist :: IORef WorkList  -- Current worklist
1018     }
1019 \end{code}
1020
1021 \begin{code}
1022
1023 ---------------
1024 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
1025
1026 instance Functor TcS where
1027   fmap f m = TcS $ fmap f . unTcS m
1028
1029 instance Applicative TcS where
1030   pure  = return
1031   (<*>) = ap
1032
1033 instance Monad TcS where
1034   return x  = TcS (\_ -> return x)
1035   fail err  = TcS (\_ -> fail err)
1036   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
1037
1038 instance MonadUnique TcS where
1039    getUniqueSupplyM = wrapTcS getUniqueSupplyM
1040
1041 -- Basic functionality
1042 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1043 wrapTcS :: TcM a -> TcS a
1044 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
1045 -- and TcS is supposed to have limited functionality
1046 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
1047
1048 wrapErrTcS :: TcM a -> TcS a
1049 -- The thing wrapped should just fail
1050 -- There's no static check; it's up to the user
1051 -- Having a variant for each error message is too painful
1052 wrapErrTcS = wrapTcS
1053
1054 wrapWarnTcS :: TcM a -> TcS a
1055 -- The thing wrapped should just add a warning, or no-op
1056 -- There's no static check; it's up to the user
1057 wrapWarnTcS = wrapTcS
1058
1059 failTcS, panicTcS :: SDoc -> TcS a
1060 failTcS      = wrapTcS . TcM.failWith
1061 panicTcS doc = pprPanic "TcCanonical" doc
1062
1063 traceTcS :: String -> SDoc -> TcS ()
1064 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
1065
1066 runTcPluginTcS :: TcPluginM a -> TcS a
1067 runTcPluginTcS = wrapTcS . runTcPluginM
1068
1069 instance HasDynFlags TcS where
1070     getDynFlags = wrapTcS getDynFlags
1071
1072 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
1073 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
1074
1075 bumpStepCountTcS :: TcS ()
1076 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
1077                                     ; n <- TcM.readTcRef ref
1078                                     ; TcM.writeTcRef ref (n+1) }
1079
1080 csTraceTcS :: SDoc -> TcS ()
1081 csTraceTcS doc
1082   = wrapTcS $ csTraceTcM 1 (return doc)
1083
1084 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
1085 -- Dump a rule-firing trace
1086 traceFireTcS ev doc
1087   = TcS $ \env -> csTraceTcM 1 $
1088     do { n <- TcM.readTcRef (tcs_count env)
1089        ; untch <- TcM.getUntouchables
1090        ; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr untch 
1091                                           <> ppr (ctLocDepth (ctEvLoc ev))) 
1092                        <+> doc <> colon)
1093                      4 (ppr ev)) } 
1094
1095 csTraceTcM :: Int -> TcM SDoc -> TcM ()
1096 -- Constraint-solver tracing, -ddump-cs-trace
1097 csTraceTcM trace_level mk_doc
1098   = do { dflags <- getDynFlags
1099        ; when (  (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
1100               && trace_level <= traceLevel dflags ) $
1101          do { msg <- mk_doc
1102             ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
1103
1104 runTcS :: TcS a                -- What to run
1105        -> TcM (a, Bag EvBind)
1106 runTcS tcs
1107   = do { ev_binds_var <- TcM.newTcEvBinds
1108        ; res <- runTcSWithEvBinds ev_binds_var tcs
1109        ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1110        ; return (res, ev_binds) }
1111
1112 runTcSWithEvBinds :: EvBindsVar
1113                   -> TcS a
1114                   -> TcM a
1115 runTcSWithEvBinds ev_binds_var tcs
1116   = do { unified_var <- TcM.newTcRef False
1117        ; step_count <- TcM.newTcRef 0
1118        ; inert_var <- TcM.newTcRef is
1119        ; wl_var <- TcM.newTcRef emptyWorkList
1120
1121        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
1122                           , tcs_unified  = unified_var
1123                           , tcs_count    = step_count
1124                           , tcs_inerts   = inert_var
1125                           , tcs_worklist = wl_var }
1126
1127              -- Run the computation
1128        ; res <- unTcS tcs env
1129
1130        ; count <- TcM.readTcRef step_count
1131        ; when (count > 0) $ 
1132          csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
1133
1134 #ifdef DEBUG
1135        ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1136        ; checkForCyclicBinds ev_binds
1137 #endif
1138
1139        ; return res }
1140   where
1141     is = emptyInert
1142
1143 #ifdef DEBUG
1144 checkForCyclicBinds :: Bag EvBind -> TcM ()
1145 checkForCyclicBinds ev_binds
1146   | null cycles
1147   = return ()
1148   | null coercion_cycles
1149   = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
1150   | otherwise
1151   = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
1152   where
1153     cycles :: [[EvBind]]
1154     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]
1155
1156     coercion_cycles = [c | c <- cycles, any is_co_bind c]
1157     is_co_bind (EvBind b _) = isEqVar b
1158
1159     edges :: [(EvBind, EvVar, [EvVar])]
1160     edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
1161 #endif
1162
1163 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
1164 nestImplicTcS ref inner_untch (TcS thing_inside)
1165   = TcS $ \ TcSEnv { tcs_unified = unified_var
1166                    , tcs_inerts = old_inert_var
1167                    , tcs_count = count } ->
1168     do { inerts <- TcM.readTcRef old_inert_var
1169        ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
1170                                    -- See Note [Do not inherit the flat cache]
1171        ; new_inert_var <- TcM.newTcRef nest_inert
1172        ; new_wl_var    <- TcM.newTcRef emptyWorkList
1173        ; let nest_env = TcSEnv { tcs_ev_binds    = ref
1174                                , tcs_unified     = unified_var
1175                                , tcs_count       = count
1176                                , tcs_inerts      = new_inert_var
1177                                , tcs_worklist    = new_wl_var }
1178        ; res <- TcM.setUntouchables inner_untch $
1179                 thing_inside nest_env
1180
1181 #ifdef DEBUG
1182        -- Perform a check that the thing_inside did not cause cycles
1183        ; ev_binds <- TcM.getTcEvBinds ref
1184        ; checkForCyclicBinds ev_binds
1185 #endif
1186
1187        ; return res }
1188
1189 recoverTcS :: TcS a -> TcS a -> TcS a
1190 recoverTcS (TcS recovery_code) (TcS thing_inside)
1191   = TcS $ \ env ->
1192     TcM.recoverM (recovery_code env) (thing_inside env)
1193
1194 nestTcS ::  TcS a -> TcS a
1195 -- Use the current untouchables, augmenting the current
1196 -- evidence bindings, and solved dictionaries
1197 -- But have no effect on the InertCans, or on the inert_flat_cache
1198 --  (the latter because the thing inside a nestTcS does unflattening)
1199 nestTcS (TcS thing_inside)
1200   = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
1201     do { inerts <- TcM.readTcRef inerts_var
1202        ; new_inert_var <- TcM.newTcRef inerts
1203        ; new_wl_var    <- TcM.newTcRef emptyWorkList
1204        ; let nest_env = env { tcs_inerts   = new_inert_var
1205                             , tcs_worklist = new_wl_var }
1206
1207        ; res <- thing_inside nest_env
1208
1209        ; new_inerts <- TcM.readTcRef new_inert_var
1210        ; TcM.writeTcRef inerts_var  -- See Note [Propagate the solved dictionaries]
1211                         (inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
1212
1213        ; return res }
1214
1215 tryTcS :: TcS a -> TcS a
1216 -- Like runTcS, but from within the TcS monad
1217 -- Completely fresh inerts and worklist, be careful!
1218 -- Moreover, we will simply throw away all the evidence generated.
1219 tryTcS (TcS thing_inside)
1220   = TcS $ \env ->
1221     do { is_var <- TcM.newTcRef emptyInert
1222        ; unified_var <- TcM.newTcRef False
1223        ; ev_binds_var <- TcM.newTcEvBinds
1224        ; wl_var <- TcM.newTcRef emptyWorkList
1225        ; let nest_env = env { tcs_ev_binds = ev_binds_var
1226                             , tcs_unified  = unified_var
1227                             , tcs_inerts   = is_var
1228                             , tcs_worklist = wl_var }
1229        ; thing_inside nest_env }
1230 \end{code}
1231
1232 Note [Propagate the solved dictionaries]
1233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1234 It's really quite important that nestTcS does not discard the solved
1235 dictionaries from the thing_inside.
1236 Consider
1237    Eq [a]
1238    forall b. empty =>  Eq [a]
1239 We solve the flat (Eq [a]), under nestTcS, and then turn our attention to
1240 the implications.  It's definitely fine to use the solved dictionaries on
1241 the inner implications, and it can make a signficant performance difference
1242 if you do so.
1243
1244 \begin{code}
1245 -- Getters and setters of TcEnv fields
1246 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1247
1248 -- Getter of inerts and worklist
1249 getTcSInertsRef :: TcS (IORef InertSet)
1250 getTcSInertsRef = TcS (return . tcs_inerts)
1251
1252 getTcSWorkListRef :: TcS (IORef WorkList)
1253 getTcSWorkListRef = TcS (return . tcs_worklist)
1254
1255 getTcSInerts :: TcS InertSet
1256 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
1257
1258 setTcSInerts :: InertSet -> TcS ()
1259 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
1260
1261 getWorkListImplics :: TcS (Bag Implication)
1262 getWorkListImplics
1263   = do { wl_var <- getTcSWorkListRef
1264        ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1265        ; return (wl_implics wl_curr) }
1266
1267 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
1268 updWorkListTcS f
1269   = do { wl_var <- getTcSWorkListRef
1270        ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1271        ; let new_work = f wl_curr
1272        ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1273
1274 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1275 -- Process the work list, returning a depleted work list,
1276 -- plus a value extracted from it (typically a work item removed from it)
1277 updWorkListTcS_return f
1278   = do { wl_var <- getTcSWorkListRef
1279        ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1280        ; traceTcS "updWorkList" (ppr wl_curr)
1281        ; let (res,new_work) = f wl_curr
1282        ; wrapTcS (TcM.writeTcRef wl_var new_work)
1283        ; return res }
1284
1285 emitWorkNC :: [CtEvidence] -> TcS ()
1286 emitWorkNC evs
1287   | null evs
1288   = return ()
1289   | otherwise
1290   = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
1291        ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
1292
1293 emitInsoluble :: Ct -> TcS ()
1294 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
1295 emitInsoluble ct
1296   = do { traceTcS "Emit insoluble" (ppr ct)
1297        ; updInertTcS add_insol }
1298   where
1299     this_pred = ctPred ct
1300     add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
1301       | already_there = is
1302       | otherwise     = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
1303       where
1304         already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
1305              -- See Note [Do not add duplicate derived insolubles]
1306
1307 getTcEvBinds :: TcS EvBindsVar
1308 getTcEvBinds = TcS (return . tcs_ev_binds)
1309
1310 getUntouchables :: TcS Untouchables
1311 getUntouchables = wrapTcS TcM.getUntouchables
1312 \end{code}
1313
1314 \begin{code}
1315 getTcEvBindsMap :: TcS EvBindMap
1316 getTcEvBindsMap
1317   = do { EvBindsVar ev_ref _ <- getTcEvBinds
1318        ; wrapTcS $ TcM.readTcRef ev_ref }
1319
1320 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
1321 -- Add a type binding
1322 -- We never do this twice!
1323 setWantedTyBind tv ty
1324   | ASSERT2( isMetaTyVar tv, ppr tv )
1325     isFmvTyVar tv
1326   = ASSERT2( isMetaTyVar tv, ppr tv )
1327     wrapTcS (TcM.writeMetaTyVar tv ty)
1328            -- Write directly into the mutable tyvar
1329            -- Flatten meta-vars are born and die locally
1330
1331   | otherwise
1332   = TcS $ \ env ->
1333     do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
1334        ; TcM.writeMetaTyVar tv ty
1335        ; TcM.writeTcRef (tcs_unified env) True }
1336
1337 reportUnifications :: TcS a -> TcS (Bool, a)
1338 reportUnifications (TcS thing_inside)
1339   = TcS $ \ env ->
1340     do { inner_unified <- TcM.newTcRef False
1341        ; res <- thing_inside (env { tcs_unified = inner_unified })
1342        ; dirty <- TcM.readTcRef inner_unified
1343        ; return (dirty, res) }
1344 \end{code}
1345
1346 \begin{code}
1347 getDefaultInfo ::  TcS ([Type], (Bool, Bool))
1348 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1349
1350 -- Just get some environments needed for instance looking up and matching
1351 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1352
1353 getInstEnvs :: TcS (InstEnv, InstEnv)
1354 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
1355
1356 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
1357 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1358
1359 getTopEnv :: TcS HscEnv
1360 getTopEnv = wrapTcS $ TcM.getTopEnv
1361
1362 getGblEnv :: TcS TcGblEnv
1363 getGblEnv = wrapTcS $ TcM.getGblEnv
1364
1365 -- Setting names as used (used in the deriving of Coercible evidence)
1366 -- Too hackish to expose it to TcS? In that case somehow extract the used
1367 -- constructors from the result of solveInteract
1368 addUsedRdrNamesTcS :: [RdrName] -> TcS ()
1369 addUsedRdrNamesTcS names = wrapTcS  $ addUsedRdrNames names
1370
1371 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1372 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1373
1374 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
1375 checkWellStagedDFun pred dfun_id loc
1376   = wrapTcS $ TcM.setCtLoc loc $
1377     do { use_stage <- TcM.getStage
1378        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1379   where
1380     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1381     bind_lvl = TcM.topIdLvl dfun_id
1382
1383 pprEq :: TcType -> TcType -> SDoc
1384 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
1385
1386 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
1387 isTouchableMetaTyVarTcS tv
1388   = do { untch <- getUntouchables
1389        ; return $ isTouchableMetaTyVar untch tv }
1390
1391 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
1392 isFilledMetaTyVar_maybe tv
1393  = ASSERT2( isTcTyVar tv, ppr tv )
1394    case tcTyVarDetails tv of
1395      MetaTv { mtv_ref = ref }
1396         -> do { cts <- wrapTcS (TcM.readTcRef ref)
1397               ; case cts of
1398                   Indirect ty -> return (Just ty)
1399                   Flexi       -> return Nothing }
1400      _ -> return Nothing
1401
1402 isFilledMetaTyVar :: TcTyVar -> TcS Bool
1403 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
1404
1405 zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
1406 zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
1407
1408 zonkTcType :: TcType -> TcS TcType
1409 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
1410
1411 zonkTcTyVar :: TcTyVar -> TcS TcType
1412 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
1413
1414 zonkFlats :: Cts -> TcS Cts
1415 zonkFlats cts = wrapTcS (TcM.zonkFlats cts)
1416 \end{code}
1417
1418
1419 Note [Do not add duplicate derived insolubles]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1421 In general we *must* add an insoluble (Int ~ Bool) even if there is
1422 one such there already, because they may come from distinct call
1423 sites.  Not only do we want an error message for each, but with
1424 -fdefer-type-errors we must generate evidence for each.  But for
1425 *derived* insolubles, we only want to report each one once.  Why?
1426
1427 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
1428     equality many times, as the original constraint is sucessively rewritten.
1429
1430 (b) Ditto the successive iterations of the main solver itself, as it traverses
1431     the constraint tree. See example below.
1432
1433 Also for *given* insolubles we may get repeated errors, as we
1434 repeatedly traverse the constraint tree.  These are relatively rare
1435 anyway, so removing duplicates seems ok.  (Alternatively we could take
1436 the SrcLoc into account.)
1437
1438 Note that the test does not need to be particularly efficient because
1439 it is only used if the program has a type error anyway.
1440
1441 Example of (b): assume a top-level class and instance declaration:
1442
1443   class D a b | a -> b
1444   instance D [a] [a]
1445
1446 Assume we have started with an implication:
1447
1448   forall c. Eq c => { wc_flat = D [c] c [W] }
1449
1450 which we have simplified to:
1451
1452   forall c. Eq c => { wc_flat = D [c] c [W]
1453                     , wc_insols = (c ~ [c]) [D] }
1454
1455 For some reason, e.g. because we floated an equality somewhere else,
1456 we might try to re-solve this implication. If we do not do a
1457 dropDerivedWC, then we will end up trying to solve the following
1458 constraints the second time:
1459
1460   (D [c] c) [W]
1461   (c ~ [c]) [D]
1462
1463 which will result in two Deriveds to end up in the insoluble set:
1464
1465   wc_flat   = D [c] c [W]
1466   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
1467
1468
1469
1470 \begin{code}
1471 -- Flatten skolems
1472 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1473 newFlattenSkolem :: CtEvidence -> TcType         -- F xis
1474                  -> TcS (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
1475 newFlattenSkolem ctxt_ev fam_ty
1476   | isGiven ctxt_ev   -- Make a given
1477   =  do { fsk <- wrapTcS $
1478                  do { uniq <- TcM.newUnique
1479                     ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
1480                     ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
1481         ; let ev = CtGiven { ctev_pred = mkTcEqPred fam_ty (mkTyVarTy fsk)
1482                            , ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
1483                            , ctev_loc  = loc }
1484         ; return (ev, fsk) }
1485
1486   | otherwise        -- Make a wanted
1487   = do { fuv <- wrapTcS $
1488                  do { uniq <- TcM.newUnique
1489                     ; ref  <- TcM.newMutVar Flexi
1490                     ; let details = MetaTv { mtv_info  = FlatMetaTv
1491                                            , mtv_ref   = ref
1492                                            , mtv_untch = fskUntouchables }
1493                           name = TcM.mkTcTyVarName uniq (fsLit "s")
1494                     ; return (mkTcTyVar name (typeKind fam_ty) details) }
1495        ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
1496        ; return (ev, fuv) }
1497   where
1498     loc = ctEvLoc ctxt_ev
1499
1500 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcTyVar) -> TcS ()
1501 extendFlatCache tc xi_args (co, fsk)
1502   = do { dflags <- getDynFlags
1503        ; when (gopt Opt_FlatCache dflags) $
1504          updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
1505             is { inert_flat_cache = insertFunEq fc tc xi_args (co, fsk) } }
1506
1507 -- Instantiations
1508 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1509
1510 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
1511 instDFunType dfun_id mb_inst_tys
1512   = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
1513   where
1514     (dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
1515
1516     go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
1517     go [] [] subst = return ([], substTy subst dfun_phi)
1518     go (tv:tvs) (Just ty : mb_tys) subst
1519       = do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
1520            ; return (ty : tys, phi) }
1521     go (tv:tvs) (Nothing : mb_tys) subst
1522       = do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
1523                          -- Don't forget to instantiate the kind!
1524                          -- cf TcMType.tcInstTyVarX
1525            ; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
1526            ; return (ty : tys, phi) }
1527     go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
1528
1529 newFlexiTcSTy :: Kind -> TcS TcType
1530 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
1531
1532 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
1533 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
1534
1535 demoteUnfilledFmv :: TcTyVar -> TcS ()
1536 -- If a flatten-meta-var is still un-filled,
1537 -- turn it into an ordinary meta-var
1538 demoteUnfilledFmv fmv
1539   = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
1540                  ; unless is_filled $
1541                    do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
1542                       ; TcM.writeMetaTyVar fmv tv_ty } }
1543
1544 instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
1545 instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
1546   where
1547      inst_one subst tv
1548          = do { ty' <- instFlexiTcSHelper (tyVarName tv)
1549                                           (substTy subst (tyVarKind tv))
1550               ; return (extendTvSubst subst tv ty', ty') }
1551
1552 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1553 instFlexiTcSHelper tvname kind
1554   = do { uniq <- TcM.newUnique
1555        ; details <- TcM.newMetaDetails (TauTv False)
1556        ; let name = setNameUnique tvname uniq
1557        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
1558
1559 instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
1560 instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
1561
1562
1563 -- Creating and setting evidence variables and CtFlavors
1564 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1565
1566 data XEvTerm
1567   = XEvTerm { ev_preds  :: [PredType]           -- New predicate types
1568             , ev_comp   :: [EvTerm] -> EvTerm   -- How to compose evidence
1569             , ev_decomp :: EvTerm -> [EvTerm]   -- How to decompose evidence
1570             -- In both ev_comp and ev_decomp, the [EvTerm] is 1-1 with ev_preds
1571             -- and each EvTerm has type of the corresponding EvPred
1572             }
1573
1574 data Freshness = Fresh | Cached
1575
1576 freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
1577 freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
1578
1579 setEvBind :: EvVar -> EvTerm -> TcS ()
1580 setEvBind the_ev tm
1581   = do { tc_evbinds <- getTcEvBinds
1582        ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
1583
1584 newTcEvBinds :: TcS EvBindsVar
1585 newTcEvBinds = wrapTcS TcM.newTcEvBinds
1586
1587 newEvVar :: TcPredType -> TcS EvVar
1588 newEvVar pred = wrapTcS (TcM.newEvVar pred)
1589
1590 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
1591 -- Make a new variable of the given PredType,
1592 -- immediately bind it to the given term
1593 -- and return its CtEvidence
1594 newGivenEvVar loc (pred, rhs)
1595   = do { new_ev <- newEvVar pred
1596        ; setEvBind new_ev rhs
1597        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
1598
1599 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
1600 -- Don't look up in the solved/inerts; we know it's not there
1601 newWantedEvVarNC loc pty
1602   = do { new_ev <- newEvVar pty
1603        ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
1604
1605 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
1606 newWantedEvVar loc pty
1607   = do { mb_ct <- lookupInInerts loc pty
1608        ; case mb_ct of
1609             Just ctev | not (isDerived ctev)
1610                       -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
1611                             ; return (ctev, Cached) }
1612             _ -> do { ctev <- newWantedEvVarNC loc pty
1613                     ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
1614                     ; return (ctev, Fresh) } }
1615
1616 emitNewDerivedEq :: CtLoc -> Pair TcType -> TcS ()
1617 -- Create new Derived and put it in the work list
1618 emitNewDerivedEq loc (Pair ty1 ty2)
1619   | ty1 `tcEqType` ty2   -- Quite common!
1620   = return ()
1621   | otherwise
1622   = emitNewDerived loc (mkTcEqPred ty1 ty2)
1623
1624 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
1625 -- Create new Derived and put it in the work list
1626 emitNewDerived loc pred
1627   = do { mb_ev <- newDerived loc pred
1628        ; case mb_ev of
1629            Nothing -> return ()
1630            Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
1631                          ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
1632
1633 newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
1634 -- Returns Nothing    if cached,
1635 --         Just pred  if not cached
1636 newDerived loc pred
1637   = do { mb_ct <- lookupInInerts loc pred
1638        ; return (case mb_ct of
1639                     Just {} -> Nothing
1640                     Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
1641
1642 instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
1643 instDFunConstraints loc = mapM (newWantedEvVar loc)
1644 \end{code}
1645
1646
1647 Note [xCtEvidence]
1648 ~~~~~~~~~~~~~~~~~~
1649 A call might look like this:
1650
1651     xCtEvidence ev evidence-transformer
1652
1653   ev is Given   => use ev_decomp to create new Givens for ev_preds,
1654                    and return them
1655
1656   ev is Wanted  => create new wanteds for ev_preds,
1657                    use ev_comp to bind ev,
1658                    return fresh wanteds (ie ones not cached in inert_cans or solved)
1659
1660   ev is Derived => create new deriveds for ev_preds
1661                       (unless cached in inert_cans or solved)
1662
1663 Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
1664       Ones that are already cached are not returned
1665
1666 Example
1667     ev : Tree a b ~ Tree c d
1668     xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
1669                                        , ev_decomp = \c. [nth 1 c, nth 2 c] })
1670               (\fresh-goals.  stuff)
1671
1672 Note [Bind new Givens immediately]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 For Givens we make new EvVars and bind them immediately. We don't worry
1675 about caching, but we don't expect complicated calculations among Givens.
1676 It is important to bind each given:
1677       class (a~b) => C a b where ....
1678       f :: C a b => ....
1679 Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
1680 But that superclass selector can't (yet) appear in a coercion
1681 (see evTermCoercion), so the easy thing is to bind it to an Id.
1682
1683 See Note [Coercion evidence terms] in TcEvidence.
1684
1685 Note [Do not create Given kind equalities]
1686 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1687 We do not want to create a Given kind equality like
1688
1689    [G]  kv ~ k   -- kv is a skolem kind variable
1690                  -- Reason we don't yet support non-Refl kind equalities
1691
1692 This showed up in Trac #8566, where we had a data type
1693    data I (u :: U *) (r :: [*]) :: * where
1694         A :: I (AA t as) r                  -- Existential k
1695 so A has type
1696    A :: forall (u:U *) (r:[*])                  Universal
1697         (k:BOX) (t:k) (as:[U *]).        Existential
1698         (u ~ AA * k t as) => I u r
1699
1700 There is no direct kind equality, but in a pattern match where 'u' is
1701 instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
1702    k ~ kk, t ~ t1, as ~ as1
1703 This is bad.  We "fix" this by simply ignoring the Given kind equality
1704 But the Right Thing is to add kind equalities!
1705
1706 But note (Trac #8705) that we *do* create Given (non-canonical) equalities
1707 with un-equal kinds, e.g.
1708    [G]  t1::k1 ~ t2::k2   -- k1 and k2 are un-equal kinds
1709 Reason: k1 or k2 might be unification variables that have already been
1710 unified (at this point we have not canonicalised the types), so we want
1711 to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2 
1712 have been unified, we'll find that when we canonicalise it, and the 
1713 t1~t2 information may be crucial (Trac #8705 is an example).
1714
1715 If it turns out that k1 and k2 are really un-equal, then it'll end up
1716 as an Irreducible (see Note [Equalities with incompatible kinds] in
1717 TcCanonical), and will do no harm.
1718
1719 \begin{code}
1720 xCtEvidence :: CtEvidence            -- Original evidence
1721             -> XEvTerm               -- Instructions about how to manipulate evidence
1722             -> TcS ()
1723
1724 xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
1725             (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
1726   = do { new_evars <- mapM (newWantedEvVar loc) ptys
1727        ; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
1728        ; emitWorkNC (freshGoals new_evars) }
1729          -- Note the "NC": these are fresh goals, not necessarily canonical
1730
1731 xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
1732             (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
1733   = ASSERT( equalLength ptys (decomp_fn tm) )
1734     do { given_evs <- mapM (newGivenEvVar loc) $    -- See Note [Bind new Givens immediately]
1735                       filterOut bad_given_pred (ptys `zip` decomp_fn tm)
1736        ; emitWorkNC given_evs }
1737   where
1738     -- See Note [Do not create Given kind equalities]
1739     bad_given_pred (pred_ty, _)
1740       | EqPred t1 _ <- classifyPredType pred_ty
1741       = isKind t1
1742       | otherwise
1743       = False
1744
1745 xCtEvidence (CtDerived { ctev_loc = loc })
1746             (XEvTerm { ev_preds = ptys })
1747   = mapM_ (emitNewDerived loc) ptys
1748
1749 -----------------------------
1750 data StopOrContinue a
1751   = ContinueWith a    -- The constraint was not solved, although it may have
1752                       --   been rewritten
1753
1754   | Stop CtEvidence   -- The (rewritten) constraint was solved
1755          SDoc         -- Tells how it was solved
1756                       -- Any new sub-goals have been put on the work list
1757
1758 instance Functor StopOrContinue where
1759   fmap f (ContinueWith x) = ContinueWith (f x)
1760   fmap _ (Stop ev s)      = Stop ev s
1761
1762 instance Outputable a => Outputable (StopOrContinue a) where
1763   ppr (Stop ev s)      = ptext (sLit "Stop") <> parens s <+> ppr ev
1764   ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1765
1766 continueWith :: a -> TcS (StopOrContinue a)
1767 continueWith = return . ContinueWith
1768
1769 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1770 stopWith ev s = return (Stop ev (text s))
1771
1772 andWhenContinue :: TcS (StopOrContinue a)
1773                 -> (a -> TcS (StopOrContinue b))
1774                 -> TcS (StopOrContinue b)
1775 andWhenContinue tcs1 tcs2
1776   = do { r <- tcs1
1777        ; case r of
1778            Stop ev s       -> return (Stop ev s)
1779            ContinueWith ct -> tcs2 ct }
1780
1781 rewriteEvidence :: CtEvidence   -- old evidence
1782                 -> TcPredType   -- new predicate
1783                 -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
1784                 -> TcS (StopOrContinue CtEvidence)
1785 -- Returns Just new_ev iff either (i)  'co' is reflexivity
1786 --                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1787 -- In either case, there is nothing new to do with new_ev
1788 {-
1789      rewriteEvidence old_ev new_pred co
1790 Main purpose: create new evidence for new_pred;
1791               unless new_pred is cached already
1792 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1793 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1794 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1795 * Returns Nothing if new_ev is already cached
1796
1797         Old evidence    New predicate is               Return new evidence
1798         flavour                                        of same flavor
1799         -------------------------------------------------------------------
1800         Wanted          Already solved or in inert     Nothing
1801         or Derived      Not                            Just new_evidence
1802
1803         Given           Already in inert               Nothing
1804                         Not                            Just new_evidence
1805
1806 Note [Rewriting with Refl]
1807 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1808 If the coercion is just reflexivity then you may re-use the same
1809 variable.  But be careful!  Although the coercion is Refl, new_pred
1810 may reflect the result of unification alpha := ty, so new_pred might
1811 not _look_ the same as old_pred, and it's vital to proceed from now on
1812 using new_pred.
1813
1814 The flattener preserves type synonyms, so they should appear in new_pred
1815 as well as in old_pred; that is important for good error messages.
1816  -}
1817
1818
1819 rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
1820   = -- If derived, don't even look at the coercion.
1821     -- This is very important, DO NOT re-order the equations for
1822     -- rewriteEvidence to put the isTcReflCo test first!
1823     -- Why?  Because for *Derived* constraints, c, the coercion, which
1824     -- was produced by flattening, may contain suspended calls to
1825     -- (ctEvTerm c), which fails for Derived constraints.
1826     -- (Getting this wrong caused Trac #7384.)
1827     do { mb_ev <- newDerived loc new_pred
1828        ; case mb_ev of
1829            Just new_ev -> continueWith new_ev
1830            Nothing     -> stopWith old_ev "Cached derived" }
1831
1832 rewriteEvidence old_ev new_pred co
1833   | isTcReflCo co -- See Note [Rewriting with Refl]
1834   = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1835
1836 rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
1837   = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
1838        ; return (ContinueWith new_ev) }
1839   where
1840     new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo
1841
1842 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1843   = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1844        ; MASSERT( tcCoercionRole co == Nominal )
1845        ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
1846        ; case freshness of
1847             Fresh  -> continueWith new_ev
1848             Cached -> stopWith ev "Cached wanted" }
1849
1850
1851 rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
1852                                         --              or orhs ~ olhs (swapped)
1853                   -> SwapFlag
1854                   -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
1855                                         -- Should be zonked, because we use typeKind on nlhs/nrhs
1856                   -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
1857                   -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
1858                   -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
1859 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1860 -- we generate
1861 -- If not swapped
1862 --      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1863 -- If 'swapped'
1864 --      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1865 --
1866 -- For (Wanted w) we do the dual thing.
1867 -- New  w1 : nlhs ~ nrhs
1868 -- If not swapped
1869 --      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1870 -- If swapped
1871 --      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1872 --
1873 -- It's all a form of rewwriteEvidence, specialised for equalities
1874 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
1875   | CtDerived { ctev_loc = loc } <- old_ev
1876   = do { mb <- newDerived loc (mkTcEqPred nlhs nrhs)
1877        ; case mb of 
1878            Just new_ev -> continueWith new_ev
1879            Nothing     -> stopWith old_ev "Cached derived" }
1880
1881   | NotSwapped <- swapped
1882   , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
1883   , isTcReflCo rhs_co
1884   = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1885
1886   | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
1887   = do { let new_tm = EvCoercion (lhs_co 
1888                                   `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
1889                                   `mkTcTransCo` mkTcSymCo rhs_co)
1890        ; new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
1891        ; return (ContinueWith new_ev) }
1892
1893   | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
1894   = do { new_evar <- newWantedEvVarNC loc new_pred
1895                      -- Not much point in seeking exact-match equality evidence
1896        ; let co = maybeSym swapped $
1897                   mkTcSymCo lhs_co
1898                   `mkTcTransCo` ctEvCoercion new_evar
1899                   `mkTcTransCo` rhs_co
1900        ; setEvBind evar (EvCoercion co)
1901        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1902        ; return (ContinueWith new_evar) }
1903
1904   | otherwise
1905   = panic "rewriteEvidence"
1906   where
1907     new_pred = mkTcEqPred nlhs nrhs
1908
1909 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1910 maybeSym IsSwapped  co = mkTcSymCo co
1911 maybeSym NotSwapped co = co
1912
1913 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
1914 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
1915 matchFam tycon args
1916   | isOpenTypeFamilyTyCon tycon
1917   = do { fam_envs <- getFamInstEnvs
1918        ; let mb_match = tcLookupFamInst fam_envs tycon args
1919        ; traceTcS "lookupFamInst" $
1920                   vcat [ ppr tycon <+> ppr args
1921                        , pprTvBndrs (varSetElems (tyVarsOfTypes args))
1922                        , ppr mb_match ]
1923        ; case mb_match of
1924            Nothing -> return Nothing
1925            Just (FamInstMatch { fim_instance = famInst
1926                               , fim_tys      = inst_tys })
1927              -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
1928                     ty = pSnd $ tcCoercionKind co
1929                 in return $ Just (co, ty) }
1930
1931   | Just ax <- isClosedSynFamilyTyCon_maybe tycon
1932   , Just (ind, inst_tys) <- chooseBranch ax args
1933   = let co = mkTcAxInstCo Nominal ax ind inst_tys
1934         ty = pSnd (tcCoercionKind co)
1935     in return $ Just (co, ty)
1936
1937   | Just ops <- isBuiltInSynFamTyCon_maybe tycon =
1938     return $ do (r,ts,ty) <- sfMatchFam ops args
1939                 return (mkTcAxiomRuleCo r ts [], ty)
1940
1941   | otherwise
1942   = return Nothing
1943
1944 \end{code}
1945
1946 Note [Residual implications]
1947 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1948 The wl_implics in the WorkList are the residual implication
1949 constraints that are generated while solving or canonicalising the
1950 current worklist.  Specifically, when canonicalising
1951    (forall a. t1 ~ forall a. t2) 
1952 from which we get the implication
1953    (forall a. t1 ~ t2)
1954 See TcSMonad.deferTcSForAllEq
1955
1956
1957 \begin{code}
1958 -- Deferring forall equalities as implications
1959 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1960
1961 deferTcSForAllEq :: Role -- Nominal or Representational
1962                  -> CtLoc  -- Original wanted equality flavor
1963                  -> ([TyVar],TcType)   -- ForAll tvs1 body1
1964                  -> ([TyVar],TcType)   -- ForAll tvs2 body2
1965                  -> TcS EvTerm
1966 -- Some of this functionality is repeated from TcUnify,
1967 -- consider having a single place where we create fresh implications.
1968 deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
1969  = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
1970       ; let tys  = mkTyVarTys skol_tvs
1971             phi1 = Type.substTy subst1 body1
1972             phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
1973             skol_info = UnifyForAllSkol skol_tvs phi1
1974             eq_pred   = case role of
1975                           Nominal ->          mkTcEqPred      phi1 phi2
1976                           Representational -> mkCoerciblePred phi1 phi2
1977                           Phantom ->          panic "deferTcSForAllEq Phantom"
1978         ; (ctev, freshness) <- newWantedEvVar loc eq_pred
1979         ; coe_inside <- case freshness of
1980             Cached -> return (ctEvCoercion ctev)
1981             Fresh  -> do { ev_binds_var <- newTcEvBinds
1982                          ; env <- wrapTcS $ TcM.getLclEnv
1983                          ; let ev_binds = TcEvBinds ev_binds_var
1984                                new_ct = mkNonCanonical ctev
1985                                new_co = ctEvCoercion ctev
1986                                new_untch = pushUntouchables (tcl_untch env)
1987                          ; let wc = WC { wc_flat  = singleCt new_ct
1988                                        , wc_impl  = emptyBag
1989                                        , wc_insol = emptyCts }
1990                                imp = Implic { ic_untch  = new_untch
1991                                             , ic_skols  = skol_tvs
1992                                             , ic_no_eqs = True
1993                                             , ic_given  = []
1994                                             , ic_wanted = wc
1995                                             , ic_insol  = False
1996                                             , ic_binds  = ev_binds_var
1997                                             , ic_env    = env
1998                                             , ic_info   = skol_info }
1999                          ; updWorkListTcS (extendWorkListImplic imp)
2000                          ; return (TcLetCo ev_binds new_co) }
2001
2002         ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
2003 \end{code}
2004