Add a class HasDynFlags(getDynFlags)
[ghc.git] / compiler / typecheck / TcSMonad.lhs
1 \begin{code}
2 {-# OPTIONS -fno-warn-tabs #-}
3 -- The above warning supression flag is a temporary kludge.
4 -- While working on this module you are encouraged to remove it and
5 -- detab the module (please do the detabbing in a separate patch). See
6 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
7 -- for details
8
9 -- Type definitions for the constraint solver
10 module TcSMonad ( 
11
12        -- Canonical constraints, definition is now in TcRnTypes
13
14     WorkList(..), isEmptyWorkList, emptyWorkList,
15     workListFromEq, workListFromNonEq, workListFromCt, 
16     extendWorkListEq, extendWorkListNonEq, extendWorkListCt, 
17     appendWorkListCt, appendWorkListEqs, unionWorkList, selectWorkItem,
18
19     getTcSWorkList, updWorkListTcS, updWorkListTcS_return, keepWanted,
20
21     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, 
22     emitFrozenError,
23
24     isWanted, isGivenOrSolved, isDerived,
25     isGivenOrSolvedCt, isGivenCt_maybe, 
26     isWantedCt, isDerivedCt, pprFlavorArising,
27
28     isFlexiTcsTv,
29
30     canRewrite, canSolve,
31     combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
32     mkWantedFlavor,
33     getWantedLoc,
34
35     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
36     traceFireTcS, bumpStepCountTcS, doWithInert,
37     tryTcS, nestImplicTcS, recoverTcS,
38     wrapErrTcS, wrapWarnTcS,
39
40     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
41
42        -- Creation of evidence variables
43     newEvVar, forceNewEvVar, delCachedEvVar, updateFlatCache, flushFlatCache,
44     newGivenEqVar,
45     newEqVar, newKindConstraint,
46     EvVarCreated (..), isNewEvVar, FlatEqOrigin ( .. ), origin_matches,
47
48        -- Setting evidence variables 
49     setEqBind,
50     setEvBind,
51
52     setWantedTyBind,
53
54     getInstEnvs, getFamInstEnvs,                -- Getting the environments
55     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
56     getTcEvBindsMap, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
57     getTcSEvVarCacheMap, getTcSEvVarFlatCache, setTcSEvVarCacheMap, pprEvVarCache,
58
59     newFlattenSkolemTy,                         -- Flatten skolems 
60
61         -- Inerts 
62     InertSet(..), 
63     getInertEqs, liftInertEqsTy, getCtCoercion,
64     emptyInert, getTcSInerts, updInertSet, extractUnsolved,
65     extractUnsolvedTcS, modifyInertTcS,
66     updInertSetTcS, partitionCCanMap, partitionEqMap,
67     getRelevantCts, extractRelevantInerts,
68     CCanMap (..), CtTypeMap, pprCtTypeMap, mkPredKeyForTypeMap, partitionCtTypeMap,
69
70
71     instDFunTypes,                              -- Instantiation
72     instDFunConstraints,          
73     newFlexiTcSTy, instFlexiTcS,
74
75     compatKind, compatKindTcS, isSubKindTcS, unifyKindTcS,
76
77     TcsUntouchables,
78     isTouchableMetaTyVar,
79     isTouchableMetaTyVar_InRange, 
80
81     getDefaultInfo, getDynFlags,
82
83     matchClass, matchFam, MatchInstResult (..), 
84     checkWellStagedDFun, 
85     warnTcS,
86     pprEq                                    -- Smaller utils, re-exported from TcM
87                                              -- TODO (DV): these are only really used in the 
88                                              -- instance matcher in TcSimplify. I am wondering
89                                              -- if the whole instance matcher simply belongs
90                                              -- here 
91 ) where 
92
93 #include "HsVersions.h"
94
95 import HscTypes
96 import BasicTypes 
97
98 import Inst
99 import InstEnv 
100 import FamInst 
101 import FamInstEnv
102
103 import qualified TcRnMonad as TcM
104 import qualified TcMType as TcM
105 import qualified TcEnv as TcM 
106        ( checkWellStaged, topIdLvl, tcGetDefaultTys )
107 import {-# SOURCE #-} qualified TcUnify as TcM ( unifyKindEq, mkKindErrorCtxt )
108 import Kind
109 import TcType
110 import DynFlags
111 import Type
112
113 import TcEvidence
114 import Class
115 import TyCon
116 import TypeRep 
117
118 import Name
119 import Var
120 import VarEnv
121 import Outputable
122 import Bag
123 import MonadUtils
124 import VarSet
125
126 import FastString
127 import Util
128 import Id 
129 import TcRnTypes
130
131 import Unique 
132 import UniqFM
133 import Maybes ( orElse )
134
135 import Control.Monad( when )
136 import StaticFlags( opt_PprStyle_Debug )
137 import Data.IORef
138
139 import TrieMap
140
141 \end{code}
142
143
144 \begin{code}
145 compatKind :: Kind -> Kind -> Bool
146 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
147
148 compatKindTcS :: Kind -> Kind -> TcS Bool
149 -- Because kind unification happens during constraint solving, we have
150 -- to make sure that two kinds are zonked before we compare them.
151 compatKindTcS k1 k2 = wrapTcS (TcM.compatKindTcM k1 k2)
152
153 isSubKindTcS :: Kind -> Kind -> TcS Bool
154 isSubKindTcS k1 k2 = wrapTcS (TcM.isSubKindTcM k1 k2)
155
156 unifyKindTcS :: Type -> Type     -- Context
157              -> Kind -> Kind     -- Corresponding kinds
158              -> TcS Bool
159 unifyKindTcS ty1 ty2 ki1 ki2
160   = wrapTcS $ TcM.addErrCtxtM ctxt $ do
161       (_errs, mb_r) <- TcM.tryTc (TcM.unifyKindEq ki1 ki2)
162       return (maybe False (const True) mb_r)
163   where 
164     ctxt = TcM.mkKindErrorCtxt ty1 ki1 ty2 ki2
165 \end{code}
166
167 %************************************************************************
168 %*                                                                      *
169 %*                            Worklists                                *
170 %*  Canonical and non-canonical constraints that the simplifier has to  *
171 %*  work on. Including their simplification depths.                     *
172 %*                                                                      *
173 %*                                                                      *
174 %************************************************************************
175
176 Note [WorkList]
177 ~~~~~~~~~~~~~~~
178
179 A WorkList contains canonical and non-canonical items (of all flavors). 
180 Notice that each Ct now has a simplification depth. We may 
181 consider using this depth for prioritization as well in the future. 
182
183 As a simple form of priority queue, our worklist separates out
184 equalities (wl_eqs) from the rest of the canonical constraints, 
185 so that it's easier to deal with them first, but the separation 
186 is not strictly necessary. Notice that non-canonical constraints 
187 are also parts of the worklist. 
188
189 Note [NonCanonical Semantics]
190 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
191 Note that canonical constraints involve a CNonCanonical constructor. In the worklist
192 we use this constructor for constraints that have not yet been canonicalized such as 
193    [Int] ~ [a] 
194 In other words, all constraints start life as NonCanonicals. 
195
196 On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
197 means that we have a ``frozen error''. 
198
199 NonCanonical constraints never interact directly with other constraints -- but they can
200 be rewritten by equalities (for instance if a non canonical exists in the inert, we'd 
201 better rewrite it as much as possible before reporting it as an error to the user)
202
203 \begin{code}
204
205 -- See Note [WorkList]
206 data WorkList = WorkList { wl_eqs  :: [Ct], wl_funeqs :: [Ct], wl_rest :: [Ct] }
207
208
209 unionWorkList :: WorkList -> WorkList -> WorkList
210 unionWorkList new_wl orig_wl = 
211    WorkList { wl_eqs    = wl_eqs new_wl ++ wl_eqs orig_wl
212             , wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl
213             , wl_rest   = wl_rest new_wl ++ wl_rest orig_wl }
214
215 extendWorkListEq :: Ct -> WorkList -> WorkList
216 -- Extension by equality
217 extendWorkListEq ct wl 
218   | Just {} <- isCFunEqCan_Maybe ct
219   = wl { wl_funeqs = ct : wl_funeqs wl }
220   | otherwise
221   = wl { wl_eqs = ct : wl_eqs wl }
222
223 extendWorkListNonEq :: Ct -> WorkList -> WorkList
224 -- Extension by non equality
225 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
226
227 extendWorkListCt :: Ct -> WorkList -> WorkList
228 -- Agnostic
229 extendWorkListCt ct wl
230  | isEqVar (cc_id ct) = extendWorkListEq ct wl
231  | otherwise = extendWorkListNonEq ct wl
232
233 appendWorkListCt :: [Ct] -> WorkList -> WorkList
234 -- Agnostic
235 appendWorkListCt cts wl = foldr extendWorkListCt wl cts
236
237 appendWorkListEqs :: [Ct] -> WorkList -> WorkList
238 -- Append a list of equalities
239 appendWorkListEqs cts wl = foldr extendWorkListEq wl cts
240
241 isEmptyWorkList :: WorkList -> Bool
242 isEmptyWorkList wl 
243   = null (wl_eqs wl) &&  null (wl_rest wl) && null (wl_funeqs wl)
244
245 emptyWorkList :: WorkList
246 emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = []}
247
248 workListFromEq :: Ct -> WorkList
249 workListFromEq ct = extendWorkListEq ct emptyWorkList
250
251 workListFromNonEq :: Ct -> WorkList
252 workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
253
254 workListFromCt :: Ct -> WorkList
255 -- Agnostic 
256 workListFromCt ct | isEqVar (cc_id ct) = workListFromEq ct 
257                   | otherwise          = workListFromNonEq ct
258
259
260 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
261 selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
262   = case (eqs,feqs,rest) of
263       (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
264       (_,(ct:cts),_)   -> (Just ct, wl { wl_funeqs = cts })
265       (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
266       (_,_,_)          -> (Nothing,wl)
267
268 -- Pretty printing 
269 instance Outputable WorkList where 
270   ppr wl = vcat [ text "WorkList (eqs)   = " <+> ppr (wl_eqs wl)
271                 , text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
272                 , text "WorkList (rest)  = " <+> ppr (wl_rest wl)
273                 ]
274
275 keepWanted :: Cts -> Cts
276 keepWanted = filterBag isWantedCt
277     -- DV: there used to be a note here that read: 
278     -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' 
279     -- DV: Is this still relevant? 
280
281 \end{code}
282
283 %************************************************************************
284 %*                                                                      *
285 %*                            Inert sets                                *
286 %*                                                                      *
287 %*                                                                      *
288 %************************************************************************
289
290
291 Note [InertSet invariants]
292 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
293 An InertSet is a bag of canonical constraints, with the following invariants:
294
295   1 No two constraints react with each other. 
296     
297     A tricky case is when there exists a given (solved) dictionary 
298     constraint and a wanted identical constraint in the inert set, but do 
299     not react because reaction would create loopy dictionary evidence for 
300     the wanted. See note [Recursive dictionaries]
301
302   2 Given equalities form an idempotent substitution [none of the
303     given LHS's occur in any of the given RHS's or reactant parts]
304
305   3 Wanted equalities also form an idempotent substitution
306
307   4 The entire set of equalities is acyclic.
308
309   5 Wanted dictionaries are inert with the top-level axiom set 
310
311   6 Equalities of the form tv1 ~ tv2 always have a touchable variable
312     on the left (if possible).
313
314   7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
315     will be marked as solved right before being pushed into the inert set. 
316     See note [Touchables and givens].
317
318   8 No Given constraint mentions a touchable unification variable, but 
319     Given/Solved may do so. 
320
321   9 Given constraints will also have their superclasses in the inert set, 
322     but Given/Solved will not. 
323  
324 Note that 6 and 7 are /not/ enforced by canonicalization but rather by 
325 insertion in the inert list, ie by TcInteract. 
326
327 During the process of solving, the inert set will contain some
328 previously given constraints, some wanted constraints, and some given
329 constraints which have arisen from solving wanted constraints. For
330 now we do not distinguish between given and solved constraints.
331
332 Note that we must switch wanted inert items to given when going under an
333 implication constraint (when in top-level inference mode).
334
335 \begin{code}
336
337 data CCanMap a = CCanMap { cts_given   :: UniqFM Cts
338                                           -- Invariant: all Given
339                          , cts_derived :: UniqFM Cts 
340                                           -- Invariant: all Derived
341                          , cts_wanted  :: UniqFM Cts } 
342                                           -- Invariant: all Wanted
343
344 cCanMapToBag :: CCanMap a -> Cts 
345 cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
346   where rest_wder = foldUFM unionBags rest_der  (cts_wanted cmap) 
347         rest_der  = foldUFM unionBags emptyCts  (cts_derived cmap)
348
349 emptyCCanMap :: CCanMap a 
350 emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM } 
351
352 updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a 
353 updCCanMap (a,ct) cmap 
354   = case cc_flavor ct of 
355       Wanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
356       Given {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
357       Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
358   where 
359     insert_into m = addToUFM_C unionBags m a (singleCt ct)
360
361 getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a) 
362 -- Gets the relevant constraints and returns the rest of the CCanMap
363 getRelevantCts a cmap 
364     = let relevant = lookup (cts_wanted cmap) `unionBags`
365                      lookup (cts_given cmap)  `unionBags`
366                      lookup (cts_derived cmap) 
367           residual_map = cmap { cts_wanted  = delFromUFM (cts_wanted cmap) a
368                               , cts_given   = delFromUFM (cts_given cmap) a
369                               , cts_derived = delFromUFM (cts_derived cmap) a }
370       in (relevant, residual_map) 
371   where
372     lookup map = lookupUFM map a `orElse` emptyCts
373
374
375 getCtTypeMapRelevants :: PredType -> TypeMap Ct -> (Cts, TypeMap Ct)
376 getCtTypeMapRelevants key_pty tmap
377   = partitionCtTypeMap (\ct -> mkPredKeyForTypeMap ct `eqType` key_pty) tmap
378
379
380 partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) 
381 -- All constraints that /match/ the predicate go in the bag, the rest remain in the map
382 partitionCCanMap pred cmap
383   = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap) 
384         (ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap)
385         (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap) 
386     in (ws `andCts` ds `andCts` gs, cmap { cts_wanted  = ws_map
387                                          , cts_given   = gs_map
388                                          , cts_derived = ds_map }) 
389   where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts)
390                                     where new_mp      = addToUFM mp k cts_keep
391                                           new_acc_cts = acc_cts `andCts` cts_out
392                                           (cts_out, cts_keep) = partitionBag pred this_cts
393
394 partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
395 partitionEqMap pred isubst 
396   = let eqs_out = foldVarEnv extend_if_pred [] isubst
397         eqs_in  = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
398     in (eqs_out, eqs_in)
399   where extend_if_pred (ct,_) cts = if pred ct then ct : cts else cts
400
401
402 extractUnsolvedCMap :: CCanMap a -> (Cts, CCanMap a)
403 -- Gets the wanted or derived constraints and returns a residual
404 -- CCanMap with only givens.
405 extractUnsolvedCMap cmap =
406   let wntd = foldUFM unionBags emptyCts (cts_wanted cmap)
407       derd = foldUFM unionBags emptyCts (cts_derived cmap)
408   in (wntd `unionBags` derd, 
409       cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM })
410
411 -- See Note [InertSet invariants]
412 data InertSet 
413   = IS { inert_eqs     :: TyVarEnv (Ct,TcCoercion) 
414          -- Must all be CTyEqCans! If an entry exists of the form: 
415          --   a |-> ct,co
416          -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
417          -- And  co : a ~ xi
418        , inert_eq_tvs  :: InScopeSet -- Invariant: superset of inert_eqs tvs
419
420        , inert_dicts        :: CCanMap Class -- Dictionaries only, index is the class
421        , inert_ips          :: CCanMap (IPName Name)      -- Implicit parameters 
422          -- NB: We do not want to use TypeMaps here because functional dependencies
423          -- will only match on the class but not the type. Similarly IPs match on the
424          -- name but not on the whole datatype
425
426        , inert_funeqs       :: CtTypeMap -- Map from family heads to CFunEqCan constraints
427
428        , inert_irreds       :: Cts  -- Irreducible predicates
429        , inert_frozen       :: Cts  -- All non-canonicals are kept here (as frozen errors)
430        }
431
432
433 type CtTypeMap = TypeMap Ct
434
435 pprCtTypeMap :: TypeMap Ct -> SDoc 
436 pprCtTypeMap ctmap = ppr (foldTM (:) ctmap [])
437
438 ctTypeMapCts :: TypeMap Ct -> Cts
439 ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
440
441 mkPredKeyForTypeMap :: Ct -> PredType
442 -- Create a key from a constraint to use in the inert CtTypeMap.
443 -- The only interesting case is for family applications, where the 
444 -- key is not the whole PredType of cc_id, but rather the family 
445 -- equality left hand side (head)
446 mkPredKeyForTypeMap (CFunEqCan { cc_fun = fn, cc_tyargs = xis }) 
447   = mkTyConApp fn xis
448 mkPredKeyForTypeMap ct 
449   = evVarPred (cc_id ct)
450
451 partitionCtTypeMap :: (Ct -> Bool)
452                    -> TypeMap Ct -> (Cts, TypeMap Ct)
453 -- Kick out the ones that match the predicate and keep the rest in the typemap
454 partitionCtTypeMap f ctmap
455   = foldTM upd_acc ctmap (emptyBag,ctmap)
456   where upd_acc ct (cts,acc_map)
457          | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
458          | otherwise = (cts,acc_map)
459          where ct_key = mkPredKeyForTypeMap ct
460
461
462 instance Outputable InertSet where
463   ppr is = vcat [ vcat (map ppr (varEnvElts (inert_eqs is)))
464                 , vcat (map ppr (Bag.bagToList $ inert_irreds is)) 
465                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
466                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is))) 
467                 , vcat (map ppr (Bag.bagToList $ ctTypeMapCts (inert_funeqs is)))
468                 , text "Frozen errors =" <+> -- Clearly print frozen errors
469                     braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
470                 , text "Warning: Not displaying cached (solved) constraints"
471                 ]
472                        
473 emptyInert :: InertSet
474 emptyInert = IS { inert_eqs     = emptyVarEnv
475                 , inert_eq_tvs  = emptyInScopeSet
476                 , inert_frozen  = emptyCts
477                 , inert_irreds  = emptyCts
478                 , inert_dicts   = emptyCCanMap
479                 , inert_ips     = emptyCCanMap
480                 , inert_funeqs  = emptyTM
481                 }
482
483
484 type AtomicInert = Ct 
485
486 updInertSet :: InertSet -> AtomicInert -> InertSet 
487 -- Add a new inert element to the inert set. 
488 updInertSet is item 
489   | isCTyEqCan item                     
490   = let upd_err a b = pprPanic "updInertSet" $
491                       vcat [ text "Multiple inert equalities:"
492                            , text "Old (already inert):" <+> ppr a
493                            , text "Trying to insert   :" <+> ppr b
494                            ]
495                            
496         -- If evidence is cached, pick it up from the flavor!
497         coercion = getCtCoercion item
498
499         eqs'     = extendVarEnv_C upd_err (inert_eqs is)
500                                           (cc_tyvar item)
501                                           (item, coercion)
502         inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item)
503     in is { inert_eqs = eqs', inert_eq_tvs = inscope' }
504
505   | Just x  <- isCIPCan_Maybe item      -- IP 
506   = is { inert_ips   = updCCanMap (x,item) (inert_ips is) }  
507   | isCIrredEvCan item                  -- Presently-irreducible evidence
508   = is { inert_irreds = inert_irreds is `Bag.snocBag` item }
509
510
511   | Just cls <- isCDictCan_Maybe item   -- Dictionary 
512   = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
513
514   | Just _tc <- isCFunEqCan_Maybe item  -- Function equality
515   = let pty = mkPredKeyForTypeMap item
516         upd_funeqs Nothing = Just item
517         upd_funeqs (Just _alredy_there) = panic "updInertSet: item already there!"
518     in is { inert_funeqs = alterTM pty upd_funeqs (inert_funeqs is) }
519      
520   | otherwise 
521   = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
522
523 updInertSetTcS :: AtomicInert -> TcS ()
524 -- Add a new item in the inerts of the monad
525 updInertSetTcS item
526   = do { traceTcS "updInertSetTcs {" $ 
527          text "Trying to insert new inert item:" <+> ppr item
528
529        ; modifyInertTcS (\is -> ((), updInertSet is item)) 
530                         
531        ; traceTcS "updInertSetTcs }" $ empty }
532
533
534 modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a 
535 -- Modify the inert set with the supplied function
536 modifyInertTcS upd 
537   = do { is_var <- getTcSInertsRef
538        ; curr_inert <- wrapTcS (TcM.readTcRef is_var)
539        ; let (a, new_inert) = upd curr_inert
540        ; wrapTcS (TcM.writeTcRef is_var new_inert)
541        ; return a }
542
543 extractUnsolvedTcS :: TcS (Cts,Cts) 
544 -- Extracts frozen errors and remaining unsolved and sets the 
545 -- inert set to be the remaining! 
546 extractUnsolvedTcS = 
547   modifyInertTcS extractUnsolved 
548
549 extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
550 -- Postcondition
551 -- -------------
552 -- When: 
553 --   ((frozen,cts),is_solved) <- extractUnsolved inert
554 -- Then: 
555 -- -----------------------------------------------------------------------------
556 --  cts       |  The unsolved (Derived or Wanted only) residual 
557 --            |  canonical constraints, that is, no CNonCanonicals.
558 -- -----------|-----------------------------------------------------------------
559 --  frozen    | The CNonCanonicals of the original inert (frozen errors), 
560 --            | of all flavors
561 -- -----------|-----------------------------------------------------------------
562 --  is_solved | Whatever remains from the inert after removing the previous two. 
563 -- -----------------------------------------------------------------------------
564 extractUnsolved is@(IS {inert_eqs = eqs, inert_irreds = irreds}) 
565   = let is_solved  = is { inert_eqs    = solved_eqs
566                         , inert_eq_tvs = inert_eq_tvs is
567                         , inert_dicts  = solved_dicts
568                         , inert_ips    = solved_ips
569                         , inert_irreds = solved_irreds
570                         , inert_frozen = emptyCts
571                         , inert_funeqs = solved_funeqs
572                         }
573     in ((inert_frozen is, unsolved), is_solved)
574
575   where solved_eqs = filterVarEnv_Directly (\_ (ct,_) -> isGivenOrSolvedCt ct) eqs
576         unsolved_eqs = foldVarEnv (\(ct,_co) cts -> cts `extendCts` ct) emptyCts $
577                        eqs `minusVarEnv` solved_eqs
578
579         (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds
580         (unsolved_ips, solved_ips)       = extractUnsolvedCMap (inert_ips is) 
581         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap (inert_dicts is) 
582
583         (unsolved_funeqs, solved_funeqs) = extractUnsolvedCtTypeMap (inert_funeqs is)
584
585         unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
586                    unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
587
588 extractUnsolvedCtTypeMap :: TypeMap Ct -> (Cts,TypeMap Ct)
589 extractUnsolvedCtTypeMap
590   = partitionCtTypeMap (not . isGivenOrSolved . cc_flavor)
591
592
593 extractRelevantInerts :: Ct -> TcS Cts
594 -- Returns the constraints from the inert set that are 'relevant' to react with 
595 -- this constraint. The monad is left with the 'thinner' inerts. 
596 -- NB: This function contains logic specific to the constraint solver, maybe move there?
597 extractRelevantInerts wi 
598   = modifyInertTcS (extract_inert_relevants wi)
599   where extract_inert_relevants (CDictCan {cc_class = cl}) is = 
600             let (cts,dict_map) = getRelevantCts cl (inert_dicts is) 
601             in (cts, is { inert_dicts = dict_map })
602         extract_inert_relevants (CFunEqCan {cc_fun = tc, cc_tyargs = xis}) is = 
603             let (cts,feqs_map)  = getCtTypeMapRelevants (mkTyConApp tc xis) (inert_funeqs is)
604             in (cts, is { inert_funeqs = feqs_map })
605         extract_inert_relevants (CIPCan { cc_ip_nm = nm } ) is = 
606             let (cts, ips_map) = getRelevantCts nm (inert_ips is) 
607             in (cts, is { inert_ips = ips_map })
608         extract_inert_relevants (CIrredEvCan { }) is = 
609             let cts = inert_irreds is 
610             in (cts, is { inert_irreds = emptyCts })
611         extract_inert_relevants _ is = (emptyCts,is)
612 \end{code}
613
614
615
616
617 %************************************************************************
618 %*                                                                      *
619                     CtFlavor
620          The "flavor" of a canonical constraint
621 %*                                                                      *
622 %************************************************************************
623
624 \begin{code}
625 getWantedLoc :: Ct -> WantedLoc
626 getWantedLoc ct 
627   = ASSERT (isWanted (cc_flavor ct))
628     case cc_flavor ct of 
629       Wanted wl -> wl 
630       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
631
632 isWantedCt :: Ct -> Bool
633 isWantedCt ct = isWanted (cc_flavor ct)
634 isDerivedCt :: Ct -> Bool
635 isDerivedCt ct = isDerived (cc_flavor ct)
636
637 isGivenCt_maybe :: Ct -> Maybe GivenKind
638 isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
639
640 isGivenOrSolvedCt :: Ct -> Bool
641 isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
642
643
644 canSolve :: CtFlavor -> CtFlavor -> Bool 
645 -- canSolve ctid1 ctid2 
646 -- The constraint ctid1 can be used to solve ctid2 
647 -- "to solve" means a reaction where the active parts of the two constraints match.
648 --  active(F xis ~ xi) = F xis 
649 --  active(tv ~ xi)    = tv 
650 --  active(D xis)      = D xis 
651 --  active(IP nm ty)   = nm 
652 --
653 -- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
654 -----------------------------------------
655 canSolve (Given {})   _            = True 
656 canSolve (Wanted {})  (Derived {}) = True
657 canSolve (Wanted {})  (Wanted {})  = True
658 canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
659 canSolve _ _ = False                       -- (There is no *evidence* for a derived.)
660
661 canRewrite :: CtFlavor -> CtFlavor -> Bool 
662 -- canRewrite ctid1 ctid2 
663 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
664 canRewrite = canSolve 
665
666 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
667 -- Precondition: At least one of them should be wanted 
668 combineCtLoc (Wanted loc) _    = loc
669 combineCtLoc _ (Wanted loc)    = loc
670 combineCtLoc (Derived loc ) _  = loc
671 combineCtLoc _ (Derived loc )  = loc
672 combineCtLoc _ _ = panic "combineCtLoc: both given"
673
674 mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor
675 -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
676 mkSolvedFlavor (Wanted  loc) sk  evterm  = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
677 mkSolvedFlavor (Derived loc) sk  evterm  = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
678 mkSolvedFlavor fl@(Given {}) _sk _evterm = pprPanic "Solving a given constraint!" $ ppr fl
679
680 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
681 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
682 mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
683 mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
684
685 mkWantedFlavor :: CtFlavor -> CtFlavor
686 mkWantedFlavor (Wanted  loc) = Wanted loc
687 mkWantedFlavor (Derived loc) = Wanted loc
688 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
689 \end{code}
690
691 %************************************************************************
692 %*                                                                      *
693 %*              The TcS solver monad                                    *
694 %*                                                                      *
695 %************************************************************************
696
697 Note [The TcS monad]
698 ~~~~~~~~~~~~~~~~~~~~
699 The TcS monad is a weak form of the main Tc monad
700
701 All you can do is
702     * fail
703     * allocate new variables
704     * fill in evidence variables
705
706 Filling in a dictionary evidence variable means to create a binding
707 for it, so TcS carries a mutable location where the binding can be
708 added.  This is initialised from the innermost implication constraint.
709
710 \begin{code}
711 data TcSEnv
712   = TcSEnv { 
713       tcs_ev_binds    :: EvBindsVar,
714       tcs_evvar_cache :: IORef EvVarCache,
715           -- Evidence bindings and a cache from predicate types to the created evidence 
716           -- variables. The scope of the cache will be the same as the scope of tcs_ev_binds
717
718       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
719           -- Global type bindings
720
721       tcs_context :: SimplContext,
722                      
723       tcs_untch :: TcsUntouchables,
724
725       tcs_ic_depth   :: Int,       -- Implication nesting depth
726       tcs_count      :: IORef Int, -- Global step count
727
728       tcs_inerts   :: IORef InertSet, -- Current inert set
729       tcs_worklist :: IORef WorkList  -- Current worklist
730
731
732     -- TcSEnv invariant: the tcs_evvar_cache is a superset of tcs_inerts, tcs_worklist, tcs_ev_binds which must 
733     --                   all be disjoint with each other.
734     }
735
736 data EvVarCache
737   = EvVarCache { evc_cache     :: TypeMap (EvVar,CtFlavor)    
738                      -- Map from PredTys to Evidence variables
739                      -- used to avoid creating new goals
740                , evc_flat_cache :: TypeMap (TcCoercion,(Xi,CtFlavor,FlatEqOrigin))
741                      -- Map from family-free heads (F xi) to family-free types.
742                      -- Useful during flattening to share flatten skolem generation
743                      -- The boolean flag:
744                      --   True  <-> This equation was generated originally during flattening
745                      --   False <-> This equation was generated by having solved a goal
746                }
747
748 data FlatEqOrigin = WhileFlattening  -- Was it generated during flattening?
749                   | WhenSolved       -- Was it generated when a family equation was solved?
750                   | Any
751
752 origin_matches :: FlatEqOrigin -> FlatEqOrigin -> Bool
753 origin_matches Any _                           = True
754 origin_matches WhenSolved WhenSolved           = True
755 origin_matches WhileFlattening WhileFlattening = True
756 origin_matches _ _ = False
757
758
759 type TcsUntouchables = (Untouchables,TcTyVarSet)
760 -- Like the TcM Untouchables, 
761 -- but records extra TcsTv variables generated during simplification
762 -- See Note [Extra TcsTv untouchables] in TcSimplify
763 \end{code}
764
765 \begin{code}
766 data SimplContext
767   = SimplInfer SDoc        -- Inferring type of a let-bound thing
768   | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
769   | SimplInteractive       -- Inferring type at GHCi prompt
770   | SimplCheck SDoc        -- Checking a type signature or RULE rhs
771
772 instance Outputable SimplContext where
773   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
774   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
775   ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
776   ppr SimplInteractive = ptext (sLit "SimplInteractive")
777
778 isInteractive :: SimplContext -> Bool
779 isInteractive SimplInteractive = True
780 isInteractive _                = False
781
782 simplEqsOnly :: SimplContext -> Bool
783 -- Simplify equalities only, not dictionaries
784 -- This is used for the LHS of rules; ee
785 -- Note [Simplifying RULE lhs constraints] in TcSimplify
786 simplEqsOnly (SimplRuleLhs {}) = True
787 simplEqsOnly _                 = False
788
789 performDefaulting :: SimplContext -> Bool
790 performDefaulting (SimplInfer {})   = False
791 performDefaulting (SimplRuleLhs {}) = False
792 performDefaulting SimplInteractive  = True
793 performDefaulting (SimplCheck {})   = True
794
795 ---------------
796 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
797
798 instance Functor TcS where
799   fmap f m = TcS $ fmap f . unTcS m
800
801 instance Monad TcS where 
802   return x  = TcS (\_ -> return x) 
803   fail err  = TcS (\_ -> fail err) 
804   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
805
806 -- Basic functionality 
807 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
808 wrapTcS :: TcM a -> TcS a 
809 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
810 -- and TcS is supposed to have limited functionality
811 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
812
813 wrapErrTcS :: TcM a -> TcS a 
814 -- The thing wrapped should just fail
815 -- There's no static check; it's up to the user
816 -- Having a variant for each error message is too painful
817 wrapErrTcS = wrapTcS
818
819 wrapWarnTcS :: TcM a -> TcS a 
820 -- The thing wrapped should just add a warning, or no-op
821 -- There's no static check; it's up to the user
822 wrapWarnTcS = wrapTcS
823
824 failTcS, panicTcS :: SDoc -> TcS a
825 failTcS      = wrapTcS . TcM.failWith
826 panicTcS doc = pprPanic "TcCanonical" doc
827
828 traceTcS :: String -> SDoc -> TcS ()
829 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
830
831 bumpStepCountTcS :: TcS ()
832 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
833                                     ; n <- TcM.readTcRef ref
834                                     ; TcM.writeTcRef ref (n+1) }
835
836 traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
837 -- Dump a rule-firing trace
838 traceFireTcS depth doc 
839   = TcS $ \env -> 
840     TcM.ifDOptM Opt_D_dump_cs_trace $ 
841     do { n <- TcM.readTcRef (tcs_count env)
842        ; let msg = int n 
843                 <> text (replicate (tcs_ic_depth env) '>')
844                 <> brackets (int depth) <+> doc
845        ; TcM.dumpTcRn msg }
846
847 runTcS :: SimplContext
848        -> Untouchables         -- Untouchables
849        -> InertSet             -- Initial inert set
850        -> WorkList             -- Initial work list
851        -> TcS a                -- What to run
852        -> TcM (a, Bag EvBind)
853 runTcS context untouch is wl tcs 
854   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
855        ; ev_cache_var <- TcM.newTcRef $ 
856                          EvVarCache { evc_cache = emptyTM, evc_flat_cache = emptyTM }
857        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
858        ; step_count <- TcM.newTcRef 0
859
860        ; inert_var <- TcM.newTcRef is 
861        ; wl_var <- TcM.newTcRef wl
862
863        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
864                           , tcs_evvar_cache = ev_cache_var
865                           , tcs_ty_binds = ty_binds_var
866                           , tcs_context  = context
867                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
868                           , tcs_count    = step_count
869                           , tcs_ic_depth = 0
870                           , tcs_inerts   = inert_var
871                           , tcs_worklist = wl_var }
872
873              -- Run the computation
874        ; res <- unTcS tcs env
875              -- Perform the type unifications required
876        ; ty_binds <- TcM.readTcRef ty_binds_var
877        ; mapM_ do_unification (varEnvElts ty_binds)
878
879        ; when debugIsOn $ do {
880              count <- TcM.readTcRef step_count
881            ; when (opt_PprStyle_Debug && count > 0) $
882              TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
883                                 <+> int count <+> ppr context)
884          }
885              -- And return
886        ; ev_binds      <- TcM.readTcRef evb_ref
887        ; return (res, evBindMapBinds ev_binds) }
888   where
889     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
890
891
892 doWithInert :: InertSet -> TcS a -> TcS a 
893 doWithInert inert (TcS action)
894   = TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert
895                      ; orig_cache_var <- TcM.readTcRef (tcs_evvar_cache env)
896                      ; new_cache_var <- TcM.newTcRef orig_cache_var
897                      ; action (env { tcs_inerts = new_inert_var 
898                                    , tcs_evvar_cache = new_cache_var }) }
899
900
901 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a 
902 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) 
903   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
904                    , tcs_evvar_cache = orig_evvar_cache_var
905                    , tcs_untch = (_outer_range, outer_tcs)
906                    , tcs_count = count
907                    , tcs_ic_depth = idepth
908                    , tcs_context = ctxt
909                    , tcs_inerts = inert_var
910                    , tcs_worklist = wl_var } -> 
911     do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
912                    -- The inner_range should be narrower than the outer one
913                    -- (thus increasing the set of untouchables) but 
914                    -- the inner Tcs-untouchables must be unioned with the
915                    -- outer ones!
916
917          -- Inherit the inerts from the outer scope
918        ; orig_inerts <- TcM.readTcRef inert_var
919        ; new_inert_var <- TcM.newTcRef orig_inerts
920                           
921          -- Inherit EvVar cache
922        ; orig_evvar_cache <- TcM.readTcRef orig_evvar_cache_var
923        ; evvar_cache <- TcM.newTcRef orig_evvar_cache
924  
925        ; let nest_env = TcSEnv { tcs_ev_binds    = ref
926                                , tcs_evvar_cache = evvar_cache
927                                , tcs_ty_binds    = ty_binds
928                                , tcs_untch       = inner_untch
929                                , tcs_count       = count
930                                , tcs_ic_depth    = idepth+1
931                                , tcs_context     = ctxtUnderImplic ctxt 
932                                , tcs_inerts      = new_inert_var
933                                , tcs_worklist    = wl_var 
934                                -- NB: worklist is going to be empty anyway, 
935                                -- so reuse the same ref cell
936                                }
937        ; thing_inside nest_env } 
938
939 recoverTcS :: TcS a -> TcS a -> TcS a
940 recoverTcS (TcS recovery_code) (TcS thing_inside)
941   = TcS $ \ env ->
942     TcM.recoverM (recovery_code env) (thing_inside env)
943
944 ctxtUnderImplic :: SimplContext -> SimplContext
945 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
946 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 
947                                                <+> doubleQuotes (ftext n))
948 ctxtUnderImplic ctxt              = ctxt
949
950 tryTcS :: TcS a -> TcS a
951 -- Like runTcS, but from within the TcS monad 
952 -- Completely afresh inerts and worklist, be careful! 
953 -- Moreover, we will simply throw away all the evidence generated. 
954 tryTcS tcs
955   = TcS (\env -> 
956              do { wl_var <- TcM.newTcRef emptyWorkList
957                 ; is_var <- TcM.newTcRef emptyInert
958
959                 ; ty_binds_var <- TcM.newTcRef emptyVarEnv
960                 ; ev_binds_var <- TcM.newTcEvBinds
961
962                 ; ev_binds_cache_var <- TcM.newTcRef (EvVarCache emptyTM emptyTM)
963                     -- Empty cache: Don't inherit cache from above, see 
964                     -- Note [tryTcS for defaulting] in TcSimplify
965
966                 ; let env1 = env { tcs_ev_binds = ev_binds_var
967                                  , tcs_evvar_cache = ev_binds_cache_var
968                                  , tcs_ty_binds = ty_binds_var
969                                  , tcs_inerts   = is_var
970                                  , tcs_worklist = wl_var } 
971                 ; unTcS tcs env1 })
972
973 -- Getters and setters of TcEnv fields
974 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
975
976 -- Getter of inerts and worklist
977 getTcSInertsRef :: TcS (IORef InertSet)
978 getTcSInertsRef = TcS (return . tcs_inerts)
979
980 getTcSWorkListRef :: TcS (IORef WorkList) 
981 getTcSWorkListRef = TcS (return . tcs_worklist) 
982
983 getTcSInerts :: TcS InertSet 
984 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) 
985
986 getTcSWorkList :: TcS WorkList
987 getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 
988
989 updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
990 updWorkListTcS f 
991   = updWorkListTcS_return (\w -> ((),f w))
992
993 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
994 updWorkListTcS_return f
995   = do { wl_var <- getTcSWorkListRef
996        ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
997        ; let (res,new_work) = f wl_curr
998        ; wrapTcS (TcM.writeTcRef wl_var new_work)
999        ; return res }
1000
1001 emitFrozenError :: CtFlavor -> EvVar -> SubGoalDepth -> TcS ()
1002 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
1003 emitFrozenError fl ev depth 
1004   = do { traceTcS "Emit frozen error" (ppr ev <+> dcolon <+> ppr (evVarPred ev))
1005        ; inert_ref <- getTcSInertsRef 
1006        ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
1007        ; let ct = CNonCanonical { cc_id = ev
1008                                 , cc_flavor = fl
1009                                 , cc_depth = depth } 
1010              inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
1011        ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
1012
1013 instance HasDynFlags TcS where
1014     getDynFlags = wrapTcS TcM.getDOpts
1015
1016 getTcSContext :: TcS SimplContext
1017 getTcSContext = TcS (return . tcs_context)
1018
1019 getTcEvBinds :: TcS EvBindsVar
1020 getTcEvBinds = TcS (return . tcs_ev_binds) 
1021
1022 getTcSEvVarCache :: TcS (IORef EvVarCache)
1023 getTcSEvVarCache = TcS (return . tcs_evvar_cache)
1024
1025 flushFlatCache :: TcS ()
1026 flushFlatCache
1027   = do { cache_var <- getTcSEvVarCache
1028        ; the_cache <- wrapTcS $ TcM.readTcRef cache_var
1029        ; wrapTcS $ TcM.writeTcRef cache_var (the_cache { evc_flat_cache = emptyTM }) }
1030
1031
1032 getTcSEvVarCacheMap :: TcS (TypeMap (EvVar,CtFlavor))
1033 getTcSEvVarCacheMap = do { cache_var <- getTcSEvVarCache 
1034                          ; the_cache <- wrapTcS $ TcM.readTcRef cache_var 
1035                          ; return (evc_cache the_cache) }
1036
1037 getTcSEvVarFlatCache :: TcS (TypeMap (TcCoercion,(Type,CtFlavor,FlatEqOrigin)))
1038 getTcSEvVarFlatCache = do { cache_var <- getTcSEvVarCache 
1039                           ; the_cache <- wrapTcS $ TcM.readTcRef cache_var 
1040                           ; return (evc_flat_cache the_cache) }
1041
1042 setTcSEvVarCacheMap :: TypeMap (EvVar,CtFlavor) -> TcS () 
1043 setTcSEvVarCacheMap cache = do { cache_var <- getTcSEvVarCache 
1044                                ; orig_cache <- wrapTcS $ TcM.readTcRef cache_var
1045                                ; let new_cache = orig_cache { evc_cache = cache } 
1046                                ; wrapTcS $ TcM.writeTcRef cache_var new_cache }
1047
1048 getUntouchables :: TcS TcsUntouchables
1049 getUntouchables = TcS (return . tcs_untch)
1050
1051 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1052 getTcSTyBinds = TcS (return . tcs_ty_binds)
1053
1054 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1055 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1056
1057
1058 getTcEvBindsMap :: TcS EvBindMap
1059 getTcEvBindsMap
1060   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
1061        ; wrapTcS $ TcM.readTcRef ev_ref }
1062
1063
1064 setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor
1065 setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl
1066
1067 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
1068 -- Add a type binding
1069 -- We never do this twice!
1070 setWantedTyBind tv ty 
1071   = do { ref <- getTcSTyBinds
1072        ; wrapTcS $ 
1073          do { ty_binds <- TcM.readTcRef ref
1074             ; when debugIsOn $
1075                   TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
1076                   vcat [ text "TERRIBLE ERROR: double set of meta type variable"
1077                        , ppr tv <+> text ":=" <+> ppr ty
1078                        , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
1079             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1080
1081
1082 setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
1083 -- If the flavor is Solved, we cache the new evidence term inside the returned flavor
1084 -- see Note [Optimizing Spontaneously Solved Coercions]
1085 setEvBind ev t fl
1086   = do { tc_evbinds <- getTcEvBinds
1087        ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
1088
1089 #ifdef DEBUG
1090        ; binds <- getTcEvBindsMap
1091        ; let cycle = any (reaches binds) (evVarsOfTerm t)
1092        ; when cycle (fail_if_co_loop binds)
1093 #endif
1094        ; return $ 
1095          case fl of 
1096            Given gl (GivenSolved _) 
1097                -> Given gl (GivenSolved (Just t))
1098            _   -> fl
1099        }
1100
1101 #ifdef DEBUG
1102   where fail_if_co_loop binds
1103           = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev
1104                                        , ppr (evBindMapBinds binds) ]) $
1105             when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
1106
1107         reaches :: EvBindMap -> Var -> Bool 
1108         -- Does this evvar reach ev? 
1109         reaches ebm ev0 = go ev0
1110           where go ev0
1111                   | ev0 == ev = True
1112                   | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
1113                   = any go (evVarsOfTerm evtrm)
1114                   | otherwise = False
1115 #endif
1116
1117 \end{code}
1118 Note [Optimizing Spontaneously Solved Coercions]
1119 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1120
1121 Spontaneously solved coercions such as alpha := tau used to be bound as everything else
1122 in the evidence binds. Subsequently they were used for rewriting other wanted or solved
1123 goals. For instance: 
1124
1125 WorkItem = [S] g1 : a ~ tau
1126 Inerts   = [S] g2 : b ~ [a]
1127            [S] g3 : c ~ [(a,a)]
1128
1129 Would result, eventually, after the workitem rewrites the inerts, in the
1130 following evidence bindings:
1131
1132         g1 = ReflCo tau
1133         g2 = ReflCo [a]
1134         g3 = ReflCo [(a,a)]
1135         g2' = g2 ; [g1] 
1136         g3' = g3 ; [(g1,g1)]
1137
1138 This ia annoying because it puts way too much stress to the zonker and
1139 desugarer, since we /know/ at the generation time (spontaneously
1140 solving) that the evidence for a particular evidence variable is the
1141 identity.
1142
1143 For this reason, our solution is to cache inside the GivenSolved
1144 flavor of a constraint the term which is actually solving this
1145 constraint. Whenever we perform a setEvBind, a new flavor is returned
1146 so that if it was a GivenSolved to start with, it remains a
1147 GivenSolved with a new evidence term inside. Then, when we use solved
1148 goals to rewrite other constraints we simply use whatever is in the
1149 GivenSolved flavor and not the constraint cc_id.
1150
1151 In our particular case we'd get the following evidence bindings, eventually: 
1152
1153        g1 = ReflCo tau
1154        g2 = ReflCo [a]
1155        g3 = ReflCo [(a,a)]
1156        g2'= ReflCo [a]
1157        g3'= ReflCo [(a,a)]
1158
1159 Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
1160
1161 \begin{code}
1162
1163
1164 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
1165 warnTcS loc warn_if doc 
1166   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
1167   | otherwise = return ()
1168
1169 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
1170 getDefaultInfo 
1171   = do { ctxt <- getTcSContext
1172        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
1173        ; return (ctxt, tys, flags) }
1174
1175 -- Just get some environments needed for instance looking up and matching
1176 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1177
1178 getInstEnvs :: TcS (InstEnv, InstEnv) 
1179 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
1180
1181 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
1182 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1183
1184 getTopEnv :: TcS HscEnv 
1185 getTopEnv = wrapTcS $ TcM.getTopEnv 
1186
1187 getGblEnv :: TcS TcGblEnv 
1188 getGblEnv = wrapTcS $ TcM.getGblEnv 
1189
1190 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1191 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1192
1193 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
1194 checkWellStagedDFun pred dfun_id loc 
1195   = wrapTcS $ TcM.setCtLoc loc $ 
1196     do { use_stage <- TcM.getStage
1197        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1198   where
1199     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1200     bind_lvl = TcM.topIdLvl dfun_id
1201
1202 pprEq :: TcType -> TcType -> SDoc
1203 pprEq ty1 ty2 = pprType $ mkEqPred (ty1,ty2)
1204
1205 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
1206 isTouchableMetaTyVar tv 
1207   = do { untch <- getUntouchables
1208        ; return $ isTouchableMetaTyVar_InRange untch tv } 
1209
1210 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
1211 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
1212   = case tcTyVarDetails tv of 
1213       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
1214                         -- See Note [Touchable meta type variables] 
1215       MetaTv {}      -> inTouchableRange untch tv 
1216       _              -> False 
1217
1218
1219 \end{code}
1220
1221
1222 Note [Touchable meta type variables]
1223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1224 Meta type variables allocated *by the constraint solver itself* are always
1225 touchable.  Example: 
1226    instance C a b => D [a] where...
1227 if we use this instance declaration we "make up" a fresh meta type
1228 variable for 'b', which we must later guess.  (Perhaps C has a
1229 functional dependency.)  But since we aren't in the constraint *generator*
1230 we can't allocate a Unique in the touchable range for this implication
1231 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
1232
1233
1234 \begin{code}
1235 -- Flatten skolems
1236 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1237
1238 newFlattenSkolemTy :: TcType -> TcS TcType
1239 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
1240
1241 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
1242 newFlattenSkolemTyVar ty
1243   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
1244                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
1245                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
1246        ; traceTcS "New Flatten Skolem Born" $ 
1247            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
1248        ; return tv }
1249
1250 -- Instantiations 
1251 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1252
1253 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
1254 instDFunTypes mb_inst_tys 
1255   = mapM inst_tv mb_inst_tys
1256   where
1257     inst_tv :: Either TyVar TcType -> TcS Type
1258     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
1259     inst_tv (Right ty) = return ty 
1260
1261 instDFunConstraints :: TcThetaType -> CtFlavor -> TcS [EvVarCreated] 
1262 instDFunConstraints preds fl
1263   = mapM (newEvVar fl) preds
1264
1265 instFlexiTcS :: TyVar -> TcS TcTyVar 
1266 -- Like TcM.instMetaTyVar but the variable that is created is always
1267 -- touchable; we are supposed to guess its instantiation. 
1268 -- See Note [Touchable meta type variables] 
1269 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
1270
1271 newFlexiTcSTy :: Kind -> TcS TcType  
1272 newFlexiTcSTy knd 
1273   = wrapTcS $
1274     do { uniq <- TcM.newUnique 
1275        ; ref  <- TcM.newMutVar  Flexi 
1276        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
1277        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
1278
1279 isFlexiTcsTv :: TyVar -> Bool
1280 isFlexiTcsTv tv
1281   | not (isTcTyVar tv)                  = False
1282   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
1283   | otherwise                           = False
1284
1285 newKindConstraint :: TcTyVar -> Kind -> CtFlavor -> TcS EvVarCreated
1286 -- Create new wanted CoVar that constrains the type to have the specified kind. 
1287 newKindConstraint tv knd fl
1288   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
1289        ; let ty_k = mkTyVarTy tv_k
1290        ; eqv <- newEqVar fl (mkTyVarTy tv) ty_k
1291        ; return eqv }
1292
1293 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
1294 instFlexiTcSHelper tvname tvkind
1295   = wrapTcS $ 
1296     do { uniq <- TcM.newUnique 
1297        ; ref  <- TcM.newMutVar  Flexi 
1298        ; let name = setNameUnique tvname uniq 
1299              kind = tvkind 
1300        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
1301
1302 -- Superclasses and recursive dictionaries 
1303 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1304
1305 data EvVarCreated 
1306   = EvVarCreated { evc_is_new    :: Bool    -- True iff the variable was just created
1307                  , evc_the_evvar :: EvVar } -- The actual evidence variable could be cached or new
1308
1309 isNewEvVar :: EvVarCreated -> Bool
1310 isNewEvVar = evc_is_new
1311
1312 newEvVar :: CtFlavor -> TcPredType -> TcS EvVarCreated
1313 -- Post: If Given then evc_is_new is True
1314 -- Hence it is safe to do a setEvBind right after a newEvVar with a Given flavor
1315 -- NB: newEvVar may temporarily break the TcSEnv invariant but it is expected in 
1316 --     the call sites for this invariant to be quickly restored.
1317 newEvVar fl pty
1318   | isGivenOrSolved fl    -- Create new variable and update the cache
1319   = do { 
1320 {- We lose a lot of time if we enable this check:
1321          eref <- getTcSEvVarCache
1322        ; ecache <- wrapTcS (TcM.readTcRef eref)
1323        ; case lookupTM pty (evc_cache ecache) of
1324            Just (_,cached_fl) 
1325                | cached_fl `canSolve` fl 
1326                -> pprTrace "Interesting: given newEvVar, missed caching opportunity!" empty $
1327                   return ()
1328            _ -> return ()
1329 -}
1330          new <- forceNewEvVar fl pty
1331        ; return (EvVarCreated True new) }
1332
1333   | otherwise             -- Otherwise lookup first
1334   = {-# SCC "newEvVarWanted" #-}
1335     do { eref <- getTcSEvVarCache
1336        ; ecache <- wrapTcS (TcM.readTcRef eref)
1337        ; case lookupTM pty (evc_cache ecache) of
1338            Just (cached_evvar, cached_flavor)
1339              | cached_flavor `canSolve` fl -- NB: 
1340                                            -- We want to use the cache /only/ if he can solve
1341                                            -- the workitem. If cached_flavor is Derived
1342                                            -- but we have a real Wanted, we want to create
1343                                            -- new evidence, otherwise we are in danger to
1344                                            -- have unsolved goals in the end. 
1345                                            -- (Remember: Derived's are just unification hints
1346                                            --            but they don't come with guarantees
1347                                            --            that they can be solved and we don't 
1348                                            --            quantify over them.
1349              -> do { traceTcS "newEvVar: already cached, doing nothing" 
1350                               (ppr (evc_cache ecache))
1351                    ; return (EvVarCreated False cached_evvar) }
1352            _   -- Not cached or cached with worse flavor
1353              -> do { new <- force_new_ev_var eref ecache fl pty
1354                    ; return (EvVarCreated True new) } }
1355
1356 forceNewEvVar :: CtFlavor -> TcPredType -> TcS EvVar
1357 -- Create a new EvVar, regardless of whether or not the
1358 -- cache already contains one like it, and update the cache
1359 forceNewEvVar fl pty 
1360   = do { eref   <- getTcSEvVarCache
1361        ; ecache <- wrapTcS (TcM.readTcRef eref)
1362        ; force_new_ev_var eref ecache fl pty }
1363
1364 force_new_ev_var :: IORef EvVarCache -> EvVarCache -> CtFlavor -> TcPredType -> TcS EvVar
1365 -- Create a new EvVar, and update the cache with it
1366 force_new_ev_var eref ecache fl pty
1367   = wrapTcS $
1368     do { TcM.traceTc "newEvVar" $ text "updating cache"
1369
1370        ; new_evvar <-TcM.newEvVar pty
1371             -- This is THE PLACE where we finally call TcM.newEvVar
1372
1373        ; let new_cache = updateCache ecache (new_evvar,fl,pty)
1374        ; TcM.writeTcRef eref new_cache 
1375        ; return new_evvar }
1376
1377 updateCache :: EvVarCache -> (EvVar,CtFlavor,Type) -> EvVarCache
1378 updateCache ecache (ev,fl,pty)
1379   | IPPred {} <- classifier
1380   = ecache
1381   | otherwise
1382   = ecache { evc_cache = ecache' }
1383   where classifier = classifyPredType pty
1384         ecache'    = alterTM pty (\_ -> Just (ev,fl)) $
1385                      evc_cache ecache
1386
1387 delCachedEvVar :: EvVar -> CtFlavor -> TcS ()
1388 delCachedEvVar ev _fl
1389   = {-# SCC "delCachedEvVarOther" #-}
1390     do { eref   <- getTcSEvVarCache
1391        ; ecache <- wrapTcS (TcM.readTcRef eref)
1392        ; wrapTcS $ TcM.writeTcRef eref (delFromCache ecache ev) }
1393
1394 delFromCache :: EvVarCache -> EvVar -> EvVarCache 
1395 delFromCache (EvVarCache { evc_cache      = ecache
1396                          , evc_flat_cache = flat_cache }) ev
1397   = EvVarCache { evc_cache = ecache', evc_flat_cache = flat_cache }
1398   where ecache' = alterTM pty x_del ecache
1399         x_del Nothing = Nothing
1400         x_del r@(Just (ev0,_))
1401            | ev0 == ev = Nothing
1402            | otherwise = r
1403         pty = evVarPred ev
1404
1405
1406
1407 updateFlatCache :: EvVar -> CtFlavor 
1408                 -> TyCon -> [Xi] -> TcType 
1409                 -> FlatEqOrigin
1410                 -> TcS () 
1411 updateFlatCache ev fl fn xis rhs_ty feq_origin
1412   = do { eref <- getTcSEvVarCache
1413        ; ecache <- wrapTcS (TcM.readTcRef eref)
1414        ; let flat_cache     = evc_flat_cache ecache
1415              new_flat_cache = alterTM fun_ty x_flat_cache flat_cache
1416              new_evc = ecache { evc_flat_cache = new_flat_cache }
1417        ; wrapTcS $ TcM.writeTcRef eref new_evc }
1418   where x_flat_cache _ = Just (mkTcCoVarCo ev,(rhs_ty,fl,feq_origin))
1419         fun_ty = mkTyConApp fn xis
1420
1421
1422 pprEvVarCache :: TypeMap (TcCoercion,a) -> SDoc
1423 pprEvVarCache tm = ppr (foldTM mk_pair tm [])
1424  where mk_pair (co,_) cos = (co, tcCoercionKind co) : cos
1425
1426
1427 newGivenEqVar :: CtFlavor -> TcType -> TcType -> TcCoercion -> TcS (CtFlavor,EvVar)
1428 -- Pre: fl is Given
1429 newGivenEqVar fl ty1 ty2 co 
1430   = do { ecv <- newEqVar fl ty1 ty2
1431        ; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar
1432        ; fl' <- setEvBind v (EvCoercion co) fl
1433        ; return (fl',v) }
1434
1435 newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated
1436 newEqVar fl ty1 ty2 
1437   = newEvVar fl (mkEqPred (ty1,ty2))
1438
1439
1440 \end{code} 
1441
1442
1443 \begin{code} 
1444 -- Matching and looking up classes and family instances
1445 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1446
1447 data MatchInstResult mi
1448   = MatchInstNo         -- No matching instance 
1449   | MatchInstSingle mi  -- Single matching instance
1450   | MatchInstMany       -- Multiple matching instances
1451
1452
1453 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
1454 -- Look up a class constraint in the instance environment
1455 matchClass clas tys
1456   = do  { let pred = mkClassPred clas tys 
1457         ; instEnvs <- getInstEnvs
1458         ; case lookupInstEnv instEnvs clas tys of {
1459             ([], unifs, _)               -- Nothing matches  
1460                 -> do { traceTcS "matchClass not matching"
1461                                  (vcat [ text "dict" <+> ppr pred, 
1462                                          text "unifs" <+> ppr unifs ]) 
1463                       ; return MatchInstNo  
1464                       } ;  
1465             ([(ispec, inst_tys)], [], _) -- A single match 
1466                 -> do   { let dfun_id = is_dfun ispec
1467                         ; traceTcS "matchClass success"
1468                                    (vcat [text "dict" <+> ppr pred, 
1469                                           text "witness" <+> ppr dfun_id
1470                                            <+> ppr (idType dfun_id) ])
1471                                   -- Record that this dfun is needed
1472                         ; return $ MatchInstSingle (dfun_id, inst_tys)
1473                         } ;
1474             (matches, unifs, _)          -- More than one matches 
1475                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
1476                                    (vcat [text "dict" <+> ppr pred,
1477                                           text "matches" <+> ppr matches,
1478                                           text "unifs" <+> ppr unifs])
1479                         ; return MatchInstMany 
1480                         }
1481         }
1482         }
1483
1484 matchFam :: TyCon -> [Type] -> TcS (Maybe (TyCon, [Type]))
1485 matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
1486 \end{code}
1487
1488
1489 -- Rewriting with respect to the inert equalities 
1490 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1491 \begin{code}
1492
1493 getInertEqs :: TcS (TyVarEnv (Ct,TcCoercion), InScopeSet)
1494 getInertEqs = do { inert <- getTcSInerts
1495                  ; return (inert_eqs inert, inert_eq_tvs inert) }
1496
1497 getCtCoercion :: Ct -> TcCoercion
1498 -- Precondition: A CTyEqCan.
1499 getCtCoercion ct 
1500   | Just (GivenSolved (Just (EvCoercion co))) <- maybe_given
1501   = co
1502   | otherwise
1503   = mkTcCoVarCo (setVarType (cc_id ct) (ctPred ct))
1504                 -- NB: The variable could be rewritten by a spontaneously
1505                 -- solved, so it is not safe to simply do a mkTcCoVarCo (cc_id ct)
1506                 -- Instead we use the most accurate type, given by ctPred c
1507   where maybe_given = isGiven_maybe (cc_flavor ct)
1508
1509 -- See Note [LiftInertEqs]
1510 liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet)
1511                  -> CtFlavor
1512                  -> PredType -> TcCoercion
1513 liftInertEqsTy (subst,inscope) fl pty
1514   = ty_cts_subst subst inscope fl pty
1515
1516
1517 ty_cts_subst :: TyVarEnv (Ct, TcCoercion)
1518              -> InScopeSet -> CtFlavor -> Type -> TcCoercion
1519 ty_cts_subst subst inscope fl ty 
1520   = go ty 
1521   where 
1522         go ty = go' ty
1523
1524         go' (TyVarTy tv)      = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv)
1525         go' (AppTy ty1 ty2)   = mkTcAppCo (go ty1) (go ty2) 
1526         go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)  
1527
1528         go' (ForAllTy v ty)   = mkTcForAllCo v' $! co
1529                              where 
1530                                (subst',inscope',v') = upd_tyvar_bndr subst inscope v
1531                                co = ty_cts_subst subst' inscope' fl ty 
1532
1533         go' (FunTy ty1 ty2)   = mkTcFunCo (go ty1) (go ty2)
1534
1535
1536         tyvar_cts_subst tv  
1537           | Just (ct,co) <- lookupVarEnv subst tv, cc_flavor ct `canRewrite` fl  
1538           = Just co -- Warn: use cached, not cc_id directly, because of alpha-renamings!
1539           | otherwise = Nothing 
1540
1541         upd_tyvar_bndr subst inscope v 
1542           = (new_subst, (inscope `extendInScopeSet` new_v), new_v)
1543           where new_subst 
1544                     | no_change = delVarEnv subst v
1545                         -- Otherwise we have to extend the environment with /something/. 
1546                         -- But we do not want to monadically create a new EvVar. So, we
1547                         -- create an 'unused_ct' but we cache reflexivity as the 
1548                         -- associated coercion. 
1549                     | otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v))
1550
1551                 no_change = new_v == v 
1552                 new_v     = uniqAway inscope v 
1553
1554                 unused_ct = CTyEqCan { cc_id     = unused_evvar
1555                                      , cc_flavor = fl -- canRewrite is reflexive.
1556                                      , cc_tyvar  = v 
1557                                      , cc_rhs    = mkTyVarTy new_v 
1558                                      , cc_depth  = unused_depth }
1559                 unused_depth = panic "ty_cts_subst: This depth should not be accessed!"
1560                 unused_evvar = panic "ty_cts_subst: This var is just an alpha-renaming!"
1561 \end{code}
1562
1563 Note [LiftInertEqsTy]
1564 ~~~~~~~~~~~~~~~~~~~~~~~ 
1565 The function liftInertEqPred behaves almost like liftCoSubst (in
1566 Coercion), but accepts a map TyVarEnv (Ct,Coercion) instead of a
1567 LiftCoSubst. This data structure is more convenient to use since we
1568 must apply the inert substitution /only/ if the inert equality 
1569 `canRewrite` the work item. There's admittedly some duplication of 
1570 functionality but it would be more tedious to cache and maintain 
1571 different flavors of LiftCoSubst structures in the inerts. 
1572