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