Cosmetics
[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     getTcSWorkListTvs, 
21     
22     getTcSImplics, updTcSImplics, emitTcSImplication, 
23
24     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, 
25     emitFrozenError,
26
27     isWanted, isDerived, 
28     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
29
30     isFlexiTcsTv,
31
32     canRewrite, canSolve,
33     mkGivenLoc, ctWantedLoc,
34
35     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
36     traceFireTcS, bumpStepCountTcS, doWithInert,
37     tryTcS, nestImplicTcS, recoverTcS,
38     wrapErrTcS, wrapWarnTcS,
39
40     SimplContext(..), isInteractive, performDefaulting,
41
42     -- Getting and setting the flattening cache
43     getFlatCache, updFlatCache, addToSolved, addSolvedFunEq,
44     
45     deferTcSForAllEq, 
46     
47     setEvBind,
48     XEvTerm(..),
49     MaybeNew (..), isFresh, freshGoals, getEvTerms,
50
51     xCtFlavor, -- Transform a CtEvidence during a step 
52     rewriteCtFlavor,          -- Specialized version of xCtFlavor for coercions
53     newWantedEvVar, instDFunConstraints, newKindConstraint,
54     newDerived,
55     xCtFlavor_cache, rewriteCtFlavor_cache,
56     
57        -- Creation of evidence variables
58     setWantedTyBind,
59
60     getInstEnvs, getFamInstEnvs,                -- Getting the environments
61     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
62     getTcEvBindsMap, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
63
64
65     newFlattenSkolemTy,                         -- Flatten skolems 
66
67         -- Inerts 
68     InertSet(..), InertCans(..), 
69     getInertEqs, getCtCoercion,
70     emptyInert, getTcSInerts, lookupInInerts, 
71     extractUnsolved,
72     extractUnsolvedTcS, modifyInertTcS,
73     updInertSetTcS, partitionCCanMap, partitionEqMap,
74     getRelevantCts, extractRelevantInerts,
75     CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
76     PredMap, FamHeadMap,
77     partCtFamHeadMap, lookupFamHead,
78
79
80     instDFunType,                              -- Instantiation
81     newFlexiTcSTy, instFlexiTcS,
82
83     compatKind, mkKindErrorCtxtTcS,
84
85     TcsUntouchables,
86     isTouchableMetaTyVar,
87     isTouchableMetaTyVar_InRange, 
88
89     getDefaultInfo, getDynFlags,
90
91     matchClass, matchFam, MatchInstResult (..), 
92     checkWellStagedDFun, 
93     warnTcS,
94     pprEq                                    -- Smaller utils, re-exported from TcM
95                                              -- TODO (DV): these are only really used in the 
96                                              -- instance matcher in TcSimplify. I am wondering
97                                              -- if the whole instance matcher simply belongs
98                                              -- here 
99 ) where 
100
101 #include "HsVersions.h"
102
103 import HscTypes
104 import BasicTypes 
105
106 import Inst
107 import InstEnv 
108 import FamInst 
109 import FamInstEnv
110
111 import qualified TcRnMonad as TcM
112 import qualified TcMType as TcM
113 import qualified TcEnv as TcM 
114        ( checkWellStaged, topIdLvl, tcGetDefaultTys )
115 import {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
116 import Kind
117 import TcType
118 import DynFlags
119 import Type
120
121 import TcEvidence
122 import Class
123 import TyCon
124
125 import Name
126 import Var
127 import VarEnv
128 import Outputable
129 import Bag
130 import MonadUtils
131 import VarSet
132
133 import FastString
134 import Util
135 import Id 
136 import TcRnTypes
137
138 import Unique 
139 import UniqFM
140 import Maybes ( orElse, catMaybes )
141
142
143 import Control.Monad( when )
144 import StaticFlags( opt_PprStyle_Debug )
145 import Data.IORef
146 import TrieMap
147
148 \end{code}
149
150
151 \begin{code}
152 compatKind :: Kind -> Kind -> Bool
153 compatKind k1 k2 = k1 `tcIsSubKind` k2 || k2 `tcIsSubKind` k1 
154
155 mkKindErrorCtxtTcS :: Type -> Kind 
156                    -> Type -> Kind 
157                    -> ErrCtxt
158 mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
159   = (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
160
161 \end{code}
162
163 %************************************************************************
164 %*                                                                      *
165 %*                            Worklists                                *
166 %*  Canonical and non-canonical constraints that the simplifier has to  *
167 %*  work on. Including their simplification depths.                     *
168 %*                                                                      *
169 %*                                                                      *
170 %************************************************************************
171
172 Note [WorkList]
173 ~~~~~~~~~~~~~~~
174
175 A WorkList contains canonical and non-canonical items (of all flavors). 
176 Notice that each Ct now has a simplification depth. We may 
177 consider using this depth for prioritization as well in the future. 
178
179 As a simple form of priority queue, our worklist separates out
180 equalities (wl_eqs) from the rest of the canonical constraints, 
181 so that it's easier to deal with them first, but the separation 
182 is not strictly necessary. Notice that non-canonical constraints 
183 are also parts of the worklist. 
184
185 Note [NonCanonical Semantics]
186 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
187 Note that canonical constraints involve a CNonCanonical constructor. In the worklist
188 we use this constructor for constraints that have not yet been canonicalized such as 
189    [Int] ~ [a] 
190 In other words, all constraints start life as NonCanonicals. 
191
192 On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
193 means that we have a ``frozen error''. 
194
195 NonCanonical constraints never interact directly with other constraints -- but they can
196 be rewritten by equalities (for instance if a non canonical exists in the inert, we'd 
197 better rewrite it as much as possible before reporting it as an error to the user)
198
199 \begin{code}
200
201 -- See Note [WorkList]
202 data WorkList = WorkList { wl_eqs    :: [Ct]
203                          , wl_funeqs :: [Ct]
204                          , wl_rest   :: [Ct] 
205                          }
206
207
208 unionWorkList :: WorkList -> WorkList -> WorkList
209 unionWorkList new_wl orig_wl = 
210    WorkList { wl_eqs    = wl_eqs new_wl ++ wl_eqs orig_wl
211             , wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl
212             , wl_rest   = wl_rest new_wl ++ wl_rest orig_wl }
213
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 
226   = wl { wl_rest = ct : wl_rest wl }
227
228 extendWorkListCt :: Ct -> WorkList -> WorkList
229 -- Agnostic
230 extendWorkListCt ct wl
231  | isEqPred (ctPred ct) = extendWorkListEq ct wl
232  | otherwise = extendWorkListNonEq ct wl
233
234 appendWorkListCt :: [Ct] -> WorkList -> WorkList
235 -- Agnostic
236 appendWorkListCt cts wl = foldr extendWorkListCt wl cts
237
238 appendWorkListEqs :: [Ct] -> WorkList -> WorkList
239 -- Append a list of equalities
240 appendWorkListEqs cts wl = foldr extendWorkListEq wl cts
241
242 isEmptyWorkList :: WorkList -> Bool
243 isEmptyWorkList wl 
244   = null (wl_eqs wl) &&  null (wl_rest wl) && null (wl_funeqs wl)
245
246 emptyWorkList :: WorkList
247 emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = [] }
248
249 workListFromEq :: Ct -> WorkList
250 workListFromEq ct = extendWorkListEq ct emptyWorkList
251
252 workListFromNonEq :: Ct -> WorkList
253 workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
254
255 workListFromCt :: Ct -> WorkList
256 -- Agnostic 
257 workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct 
258                   | otherwise            = workListFromNonEq ct
259
260
261 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
262 selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
263   = case (eqs,feqs,rest) of
264       (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
265       (_,(ct:cts),_)   -> (Just ct, wl { wl_funeqs = cts })
266       (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
267       (_,_,_)          -> (Nothing,wl)
268
269 -- Pretty printing 
270 instance Outputable WorkList where 
271   ppr wl = vcat [ text "WorkList (eqs)   = " <+> ppr (wl_eqs wl)
272                 , text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
273                 , text "WorkList (rest)  = " <+> ppr (wl_rest wl)
274                 ]
275
276 keepWanted :: Cts -> Cts
277 keepWanted = filterBag isWantedCt
278     -- DV: there used to be a note here that read: 
279     -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' 
280     -- DV: Is this still relevant? 
281
282 -- Canonical constraint maps
283 data CCanMap a = CCanMap { cts_given   :: UniqFM Cts
284                                           -- Invariant: all Given
285                          , cts_derived :: UniqFM Cts 
286                                           -- Invariant: all Derived
287                          , cts_wanted  :: UniqFM Cts } 
288                                           -- Invariant: all Wanted
289
290 cCanMapToBag :: CCanMap a -> Cts 
291 cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
292   where rest_wder = foldUFM unionBags rest_der  (cts_wanted cmap) 
293         rest_der  = foldUFM unionBags emptyCts  (cts_derived cmap)
294
295 emptyCCanMap :: CCanMap a 
296 emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM } 
297
298 updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a 
299 updCCanMap (a,ct) cmap 
300   = case cc_ev ct of 
301       Wanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
302       Given {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
303       Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
304   where 
305     insert_into m = addToUFM_C unionBags m a (singleCt ct)
306
307 getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a) 
308 -- Gets the relevant constraints and returns the rest of the CCanMap
309 getRelevantCts a cmap 
310     = let relevant = lookup (cts_wanted cmap) `unionBags`
311                      lookup (cts_given cmap)  `unionBags`
312                      lookup (cts_derived cmap) 
313           residual_map = cmap { cts_wanted  = delFromUFM (cts_wanted cmap) a
314                               , cts_given   = delFromUFM (cts_given cmap) a
315                               , cts_derived = delFromUFM (cts_derived cmap) a }
316       in (relevant, residual_map) 
317   where
318     lookup map = lookupUFM map a `orElse` emptyCts
319
320 lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence
321 lookupCCanMap a pick_me map
322   = findEvidence pick_me possible_cts
323   where
324      possible_cts = lookupUFM (cts_given map)   a `plus` (
325                     lookupUFM (cts_wanted map)  a `plus` (
326                     lookupUFM (cts_derived map) a `plus` emptyCts))
327
328      plus Nothing     cts2 = cts2
329      plus (Just cts1) cts2 = cts1 `unionBags` cts2
330
331 findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence
332 findEvidence pick_me cts
333   = foldrBag pick Nothing cts
334   where
335      pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
336      pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
337                    | otherwise                             = deflt
338
339 partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) 
340 -- All constraints that /match/ the predicate go in the bag, the rest remain in the map
341 partitionCCanMap pred cmap
342   = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap) 
343         (ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap)
344         (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap) 
345     in (ws `andCts` ds `andCts` gs, cmap { cts_wanted  = ws_map
346                                          , cts_given   = gs_map
347                                          , cts_derived = ds_map }) 
348   where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts)
349                                     where new_mp      = addToUFM mp k cts_keep
350                                           new_acc_cts = acc_cts `andCts` cts_out
351                                           (cts_out, cts_keep) = partitionBag pred this_cts
352
353 partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
354 partitionEqMap pred isubst 
355   = let eqs_out = foldVarEnv extend_if_pred [] isubst
356         eqs_in  = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
357     in (eqs_out, eqs_in)
358   where extend_if_pred (ct,_) cts = if pred ct then ct : cts else cts
359
360
361 extractUnsolvedCMap :: CCanMap a -> (Cts, CCanMap a)
362 -- Gets the wanted or derived constraints and returns a residual
363 -- CCanMap with only givens.
364 extractUnsolvedCMap cmap =
365   let wntd = foldUFM unionBags emptyCts (cts_wanted cmap)
366       derd = foldUFM unionBags emptyCts (cts_derived cmap)
367   in (wntd `unionBags` derd, 
368       cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM })
369
370
371 -- Maps from PredTypes to Constraints
372 type CtTypeMap    = TypeMap    Ct
373 type CtPredMap    = PredMap    Ct
374 type CtFamHeadMap = FamHeadMap Ct
375
376 newtype PredMap    a = PredMap    { unPredMap    :: TypeMap a } -- Indexed by TcPredType
377 newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head
378
379 instance Outputable a => Outputable (PredMap a) where
380    ppr (PredMap m) = ppr (foldTM (:) m [])
381
382 instance Outputable a => Outputable (FamHeadMap a) where
383    ppr (FamHeadMap m) = ppr (foldTM (:) m [])
384
385 ctTypeMapCts :: TypeMap Ct -> Cts
386 ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
387
388 lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
389 lookupFamHead (FamHeadMap m) key = lookupTM key m
390
391 partCtFamHeadMap :: (Ct -> Bool) 
392                  -> CtFamHeadMap 
393                  -> (Cts, CtFamHeadMap)
394 partCtFamHeadMap f ctmap
395   = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
396     in (cts, FamHeadMap tymap_final)
397   where
398     tymap_inside = unFamHeadMap ctmap 
399     upd_acc ct (cts,acc_map)
400          | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
401          | otherwise = (cts,acc_map)
402          where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
403                       = ty1 
404                       | otherwise 
405                       = panic "partCtFamHeadMap, encountered non equality!"
406 \end{code}
407
408 %************************************************************************
409 %*                                                                      *
410 %*                            Inert Sets                                *
411 %*                                                                      *
412 %*                                                                      *
413 %************************************************************************
414
415 \begin{code}
416 -- All Given (fully known) or Wanted or Derived
417 -- See Note [Detailed InertCans Invariants] for more
418 data InertCans 
419   = IC { inert_eqs :: TyVarEnv Ct
420               -- Must all be CTyEqCans! If an entry exists of the form: 
421               --   a |-> ct,co
422               -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
423               -- And  co : a ~ xi
424        , inert_eq_tvs :: InScopeSet
425               -- Superset of the type variables of inert_eqs
426        , inert_dicts :: CCanMap Class
427               -- Dictionaries only, index is the class
428               -- NB: index is /not/ the whole type because FD reactions 
429               -- need to match the class but not necessarily the whole type.
430        , inert_ips :: CCanMap (IPName Name)
431               -- Implicit parameters, index is the name
432               -- NB: index is /not/ the whole type because IP reactions need 
433               -- to match the ip name but not necessarily the whole type.
434        , inert_funeqs :: CtFamHeadMap
435               -- Family equations, index is the whole family head type.
436        , inert_irreds :: Cts       
437               -- Irreducible predicates
438        }
439     
440                      
441 \end{code}
442
443 Note [Detailed InertCans Invariants]
444 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
445 The InertCans represents a collection of constraints with the following properties:
446   1 All canonical
447   2 All Given or Wanted or Derived. No (partially) Solved
448   3 No two dictionaries with the same head
449   4 No two family equations with the same head 
450       NB: This is enforced by construction since we use a CtFamHeadMap for inert_funeqs
451   5 Family equations inert wrt top-level family axioms
452   6 Dictionaries have no matching top-level instance 
453   
454   7 Non-equality constraints are fully rewritten with respect to the equalities (CTyEqCan)
455
456   8 Equalities _do_not_ form an idempotent substitution but they are guarranteed to not have
457     any occurs errors. Additional notes: 
458
459        - The lack of idempotence of the inert substitution implies that we must make sure 
460          that when we rewrite a constraint we apply the substitution /recursively/ to the 
461          types involved. Currently the one AND ONLY way in the whole constraint solver 
462          that we rewrite types and constraints wrt to the inert substitution is 
463          TcCanonical/flattenTyVar.
464
465        - In the past we did try to have the inert substituion as idempotent as possible but
466          this would only be true for constraints of the same flavor, so in total the inert 
467          substitution could not be idempotent, due to flavor-related issued. 
468          Note [Non-idempotent inert substitution] explains what is going on. 
469
470        - Whenever a constraint ends up in the worklist we do recursively apply exhaustively
471          the inert substitution to it to check for occurs errors but if an equality is already
472          in the inert set and we can guarantee that adding a new equality will not cause the
473          first equality to have an occurs check then we do not rewrite the inert equality. 
474          This happens in TcInteract, rewriteInertEqsFromInertEq. 
475          
476          See Note [Delicate equality kick-out] to see which inert equalities can safely stay
477          in the inert set and which must be kicked out to be rewritten and re-checked for 
478          occurs errors. 
479
480   9 Given family or dictionary constraints don't mention touchable unification variables
481
482 Note [Solved constraints]
483 ~~~~~~~~~~~~~~~~~~~~~~~~~
484 When we take a step to simplify a constraint 'c', we call the original constraint "solved".
485 For example:   Wanted:    ev  :: [s] ~ [t]
486                New goal:  ev1 :: s ~ t
487                Then 'ev' is now "solved".
488
489 The reason for all this is simply to avoid re-solving goals we have solved already.
490
491 * A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
492   use it to rewrite a Given; in that sense the solved goal is still a Wanted
493
494 * A solved Given is just given
495
496 * A solved Derived is possible; purpose is to avoid creating tons of identical
497   Derived goals.
498
499
500 \begin{code}
501 -- The Inert Set
502 data InertSet
503   = IS { inert_cans :: InertCans
504               -- Canonical Given, Wanted, Derived (no Solved)
505               -- Sometimes called "the inert set"
506
507        , inert_frozen :: Cts       
508               -- Frozen errors (as non-canonicals)
509                                
510        , inert_flat_cache :: CtFamHeadMap 
511               -- All ``flattening equations'' are kept here. 
512               -- Always canonical CTyFunEqs (Given or Wanted only!)
513               -- Key is by family head. We use this field during flattening only
514               -- Not necessarily inert wrt top-level equations (or inert_cans)
515
516        , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi
517        , inert_solved        :: PredMap    CtEvidence  -- All others
518               -- These two fields constitute a cache of solved (only!) constraints
519               -- See Note [Solved constraints]
520               -- - Constraints of form (F xis ~ xi) live in inert_solved_funeqs, 
521               --   all the others are in inert_solved
522               -- - Used to avoid creating a new EvVar when we have a new goal that we
523               --   have solvedin the past
524               -- - Stored not necessarily as fully rewritten 
525               --   (ToDo: rewrite lazily when we lookup)
526        }
527
528
529 instance Outputable InertCans where 
530   ppr ics = vcat [ vcat (map ppr (varEnvElts (inert_eqs ics)))
531                  , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
532                  , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics))) 
533                  , vcat (map ppr (Bag.bagToList $ 
534                                   ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
535                  , vcat (map ppr (Bag.bagToList $ inert_irreds ics))
536                  ]
537             
538 instance Outputable InertSet where 
539   ppr is = vcat [ ppr $ inert_cans is
540                 , text "Frozen errors =" <+> -- Clearly print frozen errors
541                     braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
542                 , text "Solved and cached" <+>
543                     int (foldTypeMap (\_ x -> x+1) 0 
544                              (unPredMap $ inert_solved is)) <+> 
545                     text "more constraints" ]
546
547 emptyInert :: InertSet
548 emptyInert
549   = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
550                          , inert_eq_tvs = emptyInScopeSet
551                          , inert_dicts  = emptyCCanMap
552                          , inert_ips    = emptyCCanMap
553                          , inert_funeqs = FamHeadMap emptyTM 
554                          , inert_irreds = emptyCts }
555        , inert_frozen        = emptyCts
556        , inert_flat_cache    = FamHeadMap emptyTM
557        , inert_solved        = PredMap emptyTM 
558        , inert_solved_funeqs = FamHeadMap emptyTM }
559
560 updSolvedSet :: InertSet -> CtEvidence -> InertSet 
561 updSolvedSet is item 
562   = let pty = ctEvPred item
563         upd_solved Nothing = Just item
564         upd_solved (Just _existing_solved) = Just item 
565                -- .. or Just existing_solved? Is this even possible to happen?
566     in is { inert_solved = 
567                PredMap $ 
568                alterTM pty upd_solved (unPredMap $ inert_solved is) }
569
570
571 updInertSet :: InertSet -> Ct -> InertSet 
572 -- Add a new inert element to the inert set. 
573 updInertSet is item 
574   | isCNonCanonical item 
575     -- NB: this may happen if we decide to kick some frozen error 
576     -- out to rewrite him. Frozen errors are just NonCanonicals
577   = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
578     
579   | otherwise  
580     -- A canonical Given, Wanted, or Derived
581   = is { inert_cans = upd_inert_cans (inert_cans is) item }
582   
583   where upd_inert_cans :: InertCans -> Ct -> InertCans
584         -- Precondition: item /is/ canonical
585         upd_inert_cans ics item
586           | isCTyEqCan item                     
587           = let upd_err a b = pprPanic "updInertSet" $
588                               vcat [ text "Multiple inert equalities:"
589                                    , text "Old (already inert):" <+> ppr a
590                                    , text "Trying to insert   :" <+> ppr b ]
591         
592                 eqs'     = extendVarEnv_C upd_err (inert_eqs ics) 
593                                                   (cc_tyvar item) item        
594                 inscope' = extendInScopeSetSet (inert_eq_tvs ics)
595                                                (tyVarsOfCt item)
596                 
597             in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }
598
599           | Just x  <- isCIPCan_Maybe item      -- IP 
600           = ics { inert_ips   = updCCanMap (x,item) (inert_ips ics) }  
601             
602           | isCIrredEvCan item                  -- Presently-irreducible evidence
603           = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
604
605           | Just cls <- isCDictCan_Maybe item   -- Dictionary 
606           = ics { inert_dicts = updCCanMap (cls,item) (inert_dicts ics) }
607
608           | Just _tc <- isCFunEqCan_Maybe item  -- Function equality
609           = let fam_head = mkTyConApp (cc_fun item) (cc_tyargs item)
610                 upd_funeqs Nothing = Just item
611                 upd_funeqs (Just _already_there) 
612                   = panic "updInertSet: item already there!"
613             in ics { inert_funeqs = FamHeadMap 
614                                       (alterTM fam_head upd_funeqs $ 
615                                          (unFamHeadMap $ inert_funeqs ics)) }
616           | otherwise
617           = pprPanic "upd_inert set: can't happen! Inserting " $ 
618             ppr item 
619
620 updInertSetTcS :: Ct -> TcS ()
621 -- Add a new item in the inerts of the monad
622 updInertSetTcS item
623   = do { traceTcS "updInertSetTcs {" $ 
624          text "Trying to insert new inert item:" <+> ppr item
625
626        ; modifyInertTcS (\is -> ((), updInertSet is item)) 
627                         
628        ; traceTcS "updInertSetTcs }" $ empty }
629
630
631 addToSolved :: CtEvidence -> TcS ()
632 -- Add a new item in the solved set of the monad
633 addToSolved item
634   | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
635   = return () 
636   | otherwise
637   = do { traceTcS "updSolvedSetTcs {" $ 
638          text "Trying to insert new solved item:" <+> ppr item
639
640        ; modifyInertTcS (\is -> ((), updSolvedSet is item)) 
641                         
642        ; traceTcS "updSolvedSetTcs }" $ empty }
643
644 addSolvedFunEq :: CtEvidence -> TcS ()
645 addSolvedFunEq fun_eq
646   = modifyInertTcS $ \inert -> ((), upd_inert inert)
647   where 
648     upd_inert inert 
649       = let slvd = unFamHeadMap (inert_solved_funeqs inert)
650         in inert { inert_solved_funeqs =
651                       FamHeadMap (alterTM key upd_funeqs slvd) }       
652     upd_funeqs Nothing    = Just fun_eq
653     upd_funeqs (Just _ct) = Just fun_eq 
654          -- Or _ct? depends on which caches more steps of computation
655     key = ctEvPred fun_eq
656
657 modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a 
658 -- Modify the inert set with the supplied function
659 modifyInertTcS upd 
660   = do { is_var <- getTcSInertsRef
661        ; curr_inert <- wrapTcS (TcM.readTcRef is_var)
662        ; let (a, new_inert) = upd curr_inert
663        ; wrapTcS (TcM.writeTcRef is_var new_inert)
664        ; return a }
665
666
667 extractUnsolvedTcS :: TcS (Cts,Cts) 
668 -- Extracts frozen errors and remaining unsolved and sets the 
669 -- inert set to be the remaining! 
670 extractUnsolvedTcS = modifyInertTcS extractUnsolved 
671
672 extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
673 -- Postcondition
674 -- -------------
675 -- When: 
676 --   ((frozen,cts),is_solved) <- extractUnsolved inert
677 -- Then: 
678 -- -----------------------------------------------------------------------------
679 --  cts       |  The unsolved (Derived or Wanted only) residual 
680 --            |  canonical constraints, that is, no CNonCanonicals.
681 -- -----------|-----------------------------------------------------------------
682 --  frozen    | The CNonCanonicals of the original inert (frozen errors), 
683 --            | of all flavors
684 -- -----------|-----------------------------------------------------------------
685 --  is_solved | Whatever remains from the inert after removing the previous two. 
686 -- -----------------------------------------------------------------------------
687 extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
688                                       , inert_eq_tvs = eq_tvs
689                                       , inert_irreds = irreds
690                                       , inert_ips    = ips
691                                       , inert_funeqs = funeqs
692                                       , inert_dicts  = dicts
693                                       }
694                     , inert_frozen = frozen
695                     , inert_solved = solved
696                     , inert_flat_cache = flat_cache 
697                     , inert_solved_funeqs = funeq_cache
698                     })
699   
700   = let is_solved  = IS { inert_cans = IC { inert_eqs    = solved_eqs
701                                           , inert_eq_tvs = eq_tvs
702                                           , inert_dicts  = solved_dicts
703                                           , inert_ips    = solved_ips
704                                           , inert_irreds = solved_irreds
705                                           , inert_funeqs = solved_funeqs }
706                         , inert_frozen = emptyCts -- All out
707                                          
708                               -- At some point, I used to flush all the solved, in 
709                               -- fear of evidence loops. But I think we are safe, 
710                               -- flushing is why T3064 had become slower
711                         , inert_solved        = solved      -- PredMap emptyTM
712                         , inert_flat_cache    = flat_cache  -- FamHeadMap emptyTM
713                         , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
714                         }
715     in ((frozen, unsolved), is_solved)
716
717   where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
718         unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
719                        eqs `minusVarEnv` solved_eqs
720
721         (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
722         (unsolved_ips, solved_ips)       = extractUnsolvedCMap ips
723         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap dicts
724         (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
725
726         unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
727                    unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
728
729
730
731 extractRelevantInerts :: Ct -> TcS Cts
732 -- Returns the constraints from the inert set that are 'relevant' to react with 
733 -- this constraint. The monad is left with the 'thinner' inerts. 
734 -- NB: This function contains logic specific to the constraint solver, maybe move there?
735 extractRelevantInerts wi 
736   = modifyInertTcS (extract_relevants wi)
737   where extract_relevants wi is 
738           = let (cts,ics') = extract_ics_relevants wi (inert_cans is)
739             in (cts, is { inert_cans = ics' }) 
740             
741         extract_ics_relevants (CDictCan {cc_class = cl}) ics = 
742             let (cts,dict_map) = getRelevantCts cl (inert_dicts ics) 
743             in (cts, ics { inert_dicts = dict_map })
744         extract_ics_relevants ct@(CFunEqCan {}) ics = 
745             let (cts,feqs_map)  = 
746                   let funeq_map = unFamHeadMap $ inert_funeqs ics
747                       fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
748                       lkp = lookupTM fam_head funeq_map
749                       new_funeq_map = alterTM fam_head xtm funeq_map
750                       xtm Nothing    = Nothing
751                       xtm (Just _ct) = Nothing
752                   in case lkp of 
753                     Nothing -> (emptyCts, funeq_map)
754                     Just ct -> (singleCt ct, new_funeq_map)
755             in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
756         extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics = 
757             let (cts, ips_map) = getRelevantCts nm (inert_ips ics) 
758             in (cts, ics { inert_ips = ips_map })
759         extract_ics_relevants (CIrredEvCan { }) ics = 
760             let cts = inert_irreds ics 
761             in (cts, ics { inert_irreds = emptyCts })
762         extract_ics_relevants _ ics = (emptyCts,ics)
763         
764
765 lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
766 -- Is this exact predicate type cached in the solved or canonicals of the InertSet
767 lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
768   = case lookupInSolved solved pty of
769       Just ctev -> return ctev
770       Nothing   -> lookupInInertCans ics pty
771
772 lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
773 -- Returns just if exactly this predicate type exists in the solved.
774 lookupInSolved tm pty = lookupTM pty $ unPredMap tm
775
776 lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
777 -- Returns Just if exactly this pred type exists in the inert canonicals
778 lookupInInertCans ics pty
779   = case (classifyPredType pty) of
780       ClassPred cls _ 
781          -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
782
783       EqPred ty1 _ty2 
784          | Just tv <- getTyVar_maybe ty1      -- Tyvar equation
785          , Just ct <- lookupVarEnv (inert_eqs ics) tv
786          , let ctev = ctEvidence ct
787          , ctEvPred ctev `eqType` pty
788          -> Just ctev
789
790          | Just _ <- splitTyConApp_maybe ty1  -- Family equation
791          , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
792          , let ctev = ctEvidence ct
793          , ctEvPred ctev `eqType` pty
794          -> Just ctev
795
796       IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
797     
798       _other -> Nothing -- NB: No caching for IPs
799 \end{code}
800
801
802
803
804 %************************************************************************
805 %*                                                                      *
806 %*              The TcS solver monad                                    *
807 %*                                                                      *
808 %************************************************************************
809
810 Note [The TcS monad]
811 ~~~~~~~~~~~~~~~~~~~~
812 The TcS monad is a weak form of the main Tc monad
813
814 All you can do is
815     * fail
816     * allocate new variables
817     * fill in evidence variables
818
819 Filling in a dictionary evidence variable means to create a binding
820 for it, so TcS carries a mutable location where the binding can be
821 added.  This is initialised from the innermost implication constraint.
822
823 \begin{code}
824 data TcSEnv
825   = TcSEnv { 
826       tcs_ev_binds    :: EvBindsVar,
827       
828       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
829           -- Global type bindings
830
831       tcs_context :: SimplContext,
832                      
833       tcs_untch :: TcsUntouchables,
834
835       tcs_ic_depth   :: Int,       -- Implication nesting depth
836       tcs_count      :: IORef Int, -- Global step count
837
838       tcs_inerts   :: IORef InertSet, -- Current inert set
839       tcs_worklist :: IORef WorkList, -- Current worklist
840       
841       -- Residual implication constraints that are generated 
842       -- while solving the current worklist.
843       tcs_implics  :: IORef (Bag Implication)
844     }
845
846 type TcsUntouchables = (Untouchables,TcTyVarSet)
847 -- Like the TcM Untouchables, 
848 -- but records extra TcsTv variables generated during simplification
849 -- See Note [Extra TcsTv untouchables] in TcSimplify
850 \end{code}
851
852 \begin{code}
853 data SimplContext
854   = SimplInfer SDoc        -- Inferring type of a let-bound thing
855   | SimplInteractive       -- Inferring type at GHCi prompt
856   | SimplCheck SDoc        -- Checking a type signature or RULE rhs
857
858 instance Outputable SimplContext where
859   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
860   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
861   ppr SimplInteractive = ptext (sLit "SimplInteractive")
862
863 isInteractive :: SimplContext -> Bool
864 isInteractive SimplInteractive = True
865 isInteractive _                = False
866
867 performDefaulting :: SimplContext -> Bool
868 performDefaulting (SimplInfer {})   = False
869 performDefaulting SimplInteractive  = True
870 performDefaulting (SimplCheck {})   = True
871
872 ---------------
873 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
874
875 instance Functor TcS where
876   fmap f m = TcS $ fmap f . unTcS m
877
878 instance Monad TcS where 
879   return x  = TcS (\_ -> return x) 
880   fail err  = TcS (\_ -> fail err) 
881   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
882
883 -- Basic functionality 
884 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
885 wrapTcS :: TcM a -> TcS a 
886 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
887 -- and TcS is supposed to have limited functionality
888 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
889
890 wrapErrTcS :: TcM a -> TcS a 
891 -- The thing wrapped should just fail
892 -- There's no static check; it's up to the user
893 -- Having a variant for each error message is too painful
894 wrapErrTcS = wrapTcS
895
896 wrapWarnTcS :: TcM a -> TcS a 
897 -- The thing wrapped should just add a warning, or no-op
898 -- There's no static check; it's up to the user
899 wrapWarnTcS = wrapTcS
900
901 failTcS, panicTcS :: SDoc -> TcS a
902 failTcS      = wrapTcS . TcM.failWith
903 panicTcS doc = pprPanic "TcCanonical" doc
904
905 traceTcS :: String -> SDoc -> TcS ()
906 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
907
908 bumpStepCountTcS :: TcS ()
909 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
910                                     ; n <- TcM.readTcRef ref
911                                     ; TcM.writeTcRef ref (n+1) }
912
913 traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
914 -- Dump a rule-firing trace
915 traceFireTcS depth doc 
916   = TcS $ \env -> 
917     TcM.ifDOptM Opt_D_dump_cs_trace $ 
918     do { n <- TcM.readTcRef (tcs_count env)
919        ; let msg = int n 
920                 <> text (replicate (tcs_ic_depth env) '>')
921                 <> brackets (int depth) <+> doc
922        ; TcM.dumpTcRn msg }
923
924 runTcS :: SimplContext
925        -> Untouchables         -- Untouchables
926        -> InertSet             -- Initial inert set
927        -> WorkList             -- Initial work list
928        -> TcS a                -- What to run
929        -> TcM (a, Bag EvBind)
930 runTcS context untouch is wl tcs 
931   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
932        ; ev_binds_var <- TcM.newTcEvBinds
933        ; impl_var <- TcM.newTcRef emptyBag
934        ; step_count <- TcM.newTcRef 0
935
936        ; inert_var <- TcM.newTcRef is 
937        ; wl_var <- TcM.newTcRef wl
938
939        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
940                           , tcs_ty_binds = ty_binds_var
941                           , tcs_context  = context
942                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
943                           , tcs_count    = step_count
944                           , tcs_ic_depth = 0
945                           , tcs_inerts   = inert_var
946                           , tcs_worklist = wl_var 
947                           , tcs_implics  = impl_var }
948
949              -- Run the computation
950        ; res <- unTcS tcs env
951              -- Perform the type unifications required
952        ; ty_binds <- TcM.readTcRef ty_binds_var
953        ; mapM_ do_unification (varEnvElts ty_binds)
954
955        ; when debugIsOn $ do {
956              count <- TcM.readTcRef step_count
957            ; when (opt_PprStyle_Debug && count > 0) $
958              TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
959                                 <+> int count <+> ppr context)
960          }
961              -- And return
962        ; ev_binds <- TcM.getTcEvBinds ev_binds_var
963        ; return (res, ev_binds) }
964   where
965     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
966
967
968 doWithInert :: InertSet -> TcS a -> TcS a 
969 doWithInert inert (TcS action)
970   = TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert
971                      ; action (env { tcs_inerts = new_inert_var }) }
972
973 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a 
974 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) 
975   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
976                    , tcs_untch = (_outer_range, outer_tcs)
977                    , tcs_count = count
978                    , tcs_ic_depth = idepth
979                    , tcs_context = ctxt
980                    , tcs_inerts = inert_var
981                    , tcs_worklist = wl_var 
982                    , tcs_implics = _impl_var } -> 
983     do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
984                    -- The inner_range should be narrower than the outer one
985                    -- (thus increasing the set of untouchables) but 
986                    -- the inner Tcs-untouchables must be unioned with the
987                    -- outer ones!
988
989          -- Inherit the inerts from the outer scope
990        ; orig_inerts <- TcM.readTcRef inert_var
991        ; new_inert_var <- TcM.newTcRef orig_inerts
992          -- Inherit residual implications from outer scope (?) or create
993          -- fresh var?                 
994 --     ; orig_implics <- TcM.readTcRef impl_var                   
995        ; new_implics_var <- TcM.newTcRef emptyBag
996                            
997        ; let nest_env = TcSEnv { tcs_ev_binds    = ref
998                                , tcs_ty_binds    = ty_binds
999                                , tcs_untch       = inner_untch
1000                                , tcs_count       = count
1001                                , tcs_ic_depth    = idepth+1
1002                                , tcs_context     = ctxt 
1003                                , tcs_inerts      = new_inert_var
1004                                , tcs_worklist    = wl_var 
1005                                -- NB: worklist is going to be empty anyway, 
1006                                -- so reuse the same ref cell
1007                                , tcs_implics     = new_implics_var
1008                                }
1009        ; thing_inside nest_env } 
1010
1011 recoverTcS :: TcS a -> TcS a -> TcS a
1012 recoverTcS (TcS recovery_code) (TcS thing_inside)
1013   = TcS $ \ env ->
1014     TcM.recoverM (recovery_code env) (thing_inside env)
1015
1016 tryTcS :: TcS a -> TcS a
1017 -- Like runTcS, but from within the TcS monad 
1018 -- Completely afresh inerts and worklist, be careful! 
1019 -- Moreover, we will simply throw away all the evidence generated. 
1020 tryTcS tcs
1021   = TcS (\env -> 
1022              do { wl_var <- TcM.newTcRef emptyWorkList
1023                 ; is_var <- TcM.newTcRef emptyInert
1024
1025                 ; ty_binds_var <- TcM.newTcRef emptyVarEnv
1026                 ; ev_binds_var <- TcM.newTcEvBinds
1027
1028                 ; let env1 = env { tcs_ev_binds = ev_binds_var
1029                                  , tcs_ty_binds = ty_binds_var
1030                                  , tcs_inerts   = is_var
1031                                  , tcs_worklist = wl_var } 
1032                 ; unTcS tcs env1 })
1033
1034 -- Getters and setters of TcEnv fields
1035 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1036
1037 -- Getter of inerts and worklist
1038 getTcSInertsRef :: TcS (IORef InertSet)
1039 getTcSInertsRef = TcS (return . tcs_inerts)
1040
1041 getTcSWorkListRef :: TcS (IORef WorkList) 
1042 getTcSWorkListRef = TcS (return . tcs_worklist) 
1043
1044 getTcSInerts :: TcS InertSet 
1045 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) 
1046
1047
1048 getTcSImplicsRef :: TcS (IORef (Bag Implication))
1049 getTcSImplicsRef = TcS (return . tcs_implics) 
1050
1051 getTcSImplics :: TcS (Bag Implication)
1052 getTcSImplics = getTcSImplicsRef >>= wrapTcS . (TcM.readTcRef)
1053
1054 getTcSWorkList :: TcS WorkList
1055 getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 
1056
1057
1058 getTcSWorkListTvs :: TcS TyVarSet
1059 -- Return the variables of the worklist
1060 getTcSWorkListTvs 
1061   = do { wl <- getTcSWorkList
1062        ; return $
1063          cts_tvs (wl_eqs wl) `unionVarSet` cts_tvs (wl_funeqs wl) `unionVarSet` cts_tvs (wl_rest wl) }
1064   where cts_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet 
1065
1066
1067 updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
1068 updWorkListTcS f 
1069   = updWorkListTcS_return (\w -> ((),f w))
1070
1071 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1072 updWorkListTcS_return f
1073   = do { wl_var <- getTcSWorkListRef
1074        ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1075        ; let (res,new_work) = f wl_curr
1076        ; wrapTcS (TcM.writeTcRef wl_var new_work)
1077        ; return res }
1078     
1079
1080 updTcSImplics :: (Bag Implication -> Bag Implication) -> TcS ()
1081 updTcSImplics f 
1082  = do { impl_ref <- getTcSImplicsRef
1083       ; implics <- wrapTcS (TcM.readTcRef impl_ref)
1084       ; let new_implics = f implics
1085       ; wrapTcS (TcM.writeTcRef impl_ref new_implics) }
1086
1087 emitTcSImplication :: Implication -> TcS ()
1088 emitTcSImplication imp = updTcSImplics (consBag imp)
1089
1090
1091 emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
1092 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
1093 emitFrozenError fl depth 
1094   = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
1095        ; inert_ref <- getTcSInertsRef 
1096        ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
1097        ; let ct = CNonCanonical { cc_ev = fl
1098                                 , cc_depth = depth } 
1099              inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
1100        ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
1101
1102 instance HasDynFlags TcS where
1103     getDynFlags = wrapTcS getDynFlags
1104
1105 getTcSContext :: TcS SimplContext
1106 getTcSContext = TcS (return . tcs_context)
1107
1108 getTcEvBinds :: TcS EvBindsVar
1109 getTcEvBinds = TcS (return . tcs_ev_binds) 
1110
1111 getFlatCache :: TcS CtTypeMap 
1112 getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
1113
1114 updFlatCache :: Ct -> TcS ()
1115 -- Pre: constraint is a flat family equation (equal to a flatten skolem)
1116 updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis })
1117   = modifyInertTcS upd_inert_cache
1118   where upd_inert_cache is = ((), is { inert_flat_cache = FamHeadMap new_fc })
1119                            where new_fc = alterTM pred_key upd_cache fc
1120                                  fc = unFamHeadMap $ inert_flat_cache is
1121         pred_key = mkTyConApp tc xis
1122         upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct 
1123         upd_cache (Just _ct) = Just flat_eq 
1124         upd_cache Nothing    = Just flat_eq
1125 updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
1126                         ppr other_ct
1127                         
1128
1129 getUntouchables :: TcS TcsUntouchables
1130 getUntouchables = TcS (return . tcs_untch)
1131
1132 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1133 getTcSTyBinds = TcS (return . tcs_ty_binds)
1134
1135 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1136 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1137
1138 getTcEvBindsMap :: TcS EvBindMap
1139 getTcEvBindsMap
1140   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
1141        ; wrapTcS $ TcM.readTcRef ev_ref }
1142
1143 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
1144 -- Add a type binding
1145 -- We never do this twice!
1146 setWantedTyBind tv ty 
1147   = do { ref <- getTcSTyBinds
1148        ; wrapTcS $ 
1149          do { ty_binds <- TcM.readTcRef ref
1150             ; when debugIsOn $
1151                   TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
1152                   vcat [ text "TERRIBLE ERROR: double set of meta type variable"
1153                        , ppr tv <+> text ":=" <+> ppr ty
1154                        , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
1155             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1156
1157
1158 \end{code}
1159 Note [Optimizing Spontaneously Solved Coercions]
1160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
1161
1162 Spontaneously solved coercions such as alpha := tau used to be bound as everything else
1163 in the evidence binds. Subsequently they were used for rewriting other wanted or solved
1164 goals. For instance: 
1165
1166 WorkItem = [S] g1 : a ~ tau
1167 Inerts   = [S] g2 : b ~ [a]
1168            [S] g3 : c ~ [(a,a)]
1169
1170 Would result, eventually, after the workitem rewrites the inerts, in the
1171 following evidence bindings:
1172
1173         g1 = ReflCo tau
1174         g2 = ReflCo [a]
1175         g3 = ReflCo [(a,a)]
1176         g2' = g2 ; [g1] 
1177         g3' = g3 ; [(g1,g1)]
1178
1179 This ia annoying because it puts way too much stress to the zonker and
1180 desugarer, since we /know/ at the generation time (spontaneously
1181 solving) that the evidence for a particular evidence variable is the
1182 identity.
1183
1184 For this reason, our solution is to cache inside the GivenSolved
1185 flavor of a constraint the term which is actually solving this
1186 constraint. Whenever we perform a setEvBind, a new flavor is returned
1187 so that if it was a GivenSolved to start with, it remains a
1188 GivenSolved with a new evidence term inside. Then, when we use solved
1189 goals to rewrite other constraints we simply use whatever is in the
1190 GivenSolved flavor and not the constraint cc_id.
1191
1192 In our particular case we'd get the following evidence bindings, eventually: 
1193
1194        g1 = ReflCo tau
1195        g2 = ReflCo [a]
1196        g3 = ReflCo [(a,a)]
1197        g2'= ReflCo [a]
1198        g3'= ReflCo [(a,a)]
1199
1200 Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
1201
1202 \begin{code}
1203
1204
1205 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
1206 warnTcS loc warn_if doc 
1207   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
1208   | otherwise = return ()
1209
1210 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
1211 getDefaultInfo 
1212   = do { ctxt <- getTcSContext
1213        ; (tys, flags) <- wrapTcS TcM.tcGetDefaultTys
1214        ; return (ctxt, tys, flags) }
1215
1216 -- Just get some environments needed for instance looking up and matching
1217 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1218
1219 getInstEnvs :: TcS (InstEnv, InstEnv) 
1220 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
1221
1222 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
1223 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1224
1225 getTopEnv :: TcS HscEnv 
1226 getTopEnv = wrapTcS $ TcM.getTopEnv 
1227
1228 getGblEnv :: TcS TcGblEnv 
1229 getGblEnv = wrapTcS $ TcM.getGblEnv 
1230
1231 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1232 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1233
1234 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
1235 checkWellStagedDFun pred dfun_id loc 
1236   = wrapTcS $ TcM.setCtLoc loc $ 
1237     do { use_stage <- TcM.getStage
1238        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1239   where
1240     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1241     bind_lvl = TcM.topIdLvl dfun_id
1242
1243 pprEq :: TcType -> TcType -> SDoc
1244 pprEq ty1 ty2 = pprType $ mkEqPred ty1 ty2
1245
1246 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
1247 isTouchableMetaTyVar tv 
1248   = do { untch <- getUntouchables
1249        ; return $ isTouchableMetaTyVar_InRange untch tv } 
1250
1251 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
1252 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
1253   = ASSERT2 ( isTcTyVar tv, ppr tv )
1254     case tcTyVarDetails tv of 
1255       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
1256                         -- See Note [Touchable meta type variables] 
1257       MetaTv {}      -> inTouchableRange untch tv 
1258       _              -> False 
1259
1260
1261 \end{code}
1262
1263
1264 Note [Touchable meta type variables]
1265 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1266 Meta type variables allocated *by the constraint solver itself* are always
1267 touchable.  Example: 
1268    instance C a b => D [a] where...
1269 if we use this instance declaration we "make up" a fresh meta type
1270 variable for 'b', which we must later guess.  (Perhaps C has a
1271 functional dependency.)  But since we aren't in the constraint *generator*
1272 we can't allocate a Unique in the touchable range for this implication
1273 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
1274
1275
1276 \begin{code}
1277 -- Flatten skolems
1278 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1279
1280 newFlattenSkolemTy :: TcType -> TcS TcType
1281 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
1282
1283 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
1284 newFlattenSkolemTyVar ty
1285   = do { tv <- wrapTcS $ 
1286                do { uniq <- TcM.newUnique
1287                   ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
1288                   ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
1289        ; traceTcS "New Flatten Skolem Born" $
1290          ppr tv <+> text "[:= " <+> ppr ty <+> text "]"
1291        ; return tv }
1292
1293 -- Instantiations 
1294 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1295
1296 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
1297 instDFunType dfun_id mb_inst_tys 
1298   = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
1299   where
1300     (dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
1301
1302     go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
1303     go [] [] subst = return ([], substTy subst dfun_phi)
1304     go (tv:tvs) (Just ty : mb_tys) subst
1305       = do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
1306            ; return (ty : tys, phi) }
1307     go (tv:tvs) (Nothing : mb_tys) subst
1308       = do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
1309                          -- Don't forget to instantiate the kind!
1310                          -- cf TcMType.tcInstTyVarX
1311            ; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
1312            ; return (ty : tys, phi) }
1313     go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
1314
1315 instFlexiTcS :: TyVar -> TcS TcType 
1316 -- Like TcM.instMetaTyVar but the variable that is created is 
1317 -- always touchable; we are supposed to guess its instantiation.
1318 -- See Note [Touchable meta type variables] 
1319 instFlexiTcS tv = wrapTcS (instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) )
1320
1321 newFlexiTcSTy :: Kind -> TcS TcType  
1322 newFlexiTcSTy knd 
1323   = wrapTcS $
1324     do { uniq <- TcM.newUnique 
1325        ; ref  <- TcM.newMutVar  Flexi 
1326        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
1327        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
1328
1329 isFlexiTcsTv :: TyVar -> Bool
1330 isFlexiTcsTv tv
1331   | not (isTcTyVar tv)                  = False
1332   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
1333   | otherwise                           = False
1334
1335 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1336 instFlexiTcSHelper tvname tvkind
1337   = do { uniq <- TcM.newUnique 
1338        ; ref  <- TcM.newMutVar  Flexi 
1339        ; let name = setNameUnique tvname uniq 
1340              kind = tvkind 
1341        ; return (mkTyVarTy (mkTcTyVar name kind (MetaTv TcsTv ref))) }
1342
1343
1344 -- Creating and setting evidence variables and CtFlavors
1345 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1346
1347 data XEvTerm = 
1348   XEvTerm { ev_comp   :: [EvTerm] -> EvTerm
1349                          -- How to compose evidence 
1350           , ev_decomp :: EvTerm -> [EvTerm]
1351                          -- How to decompose evidence 
1352           }
1353
1354 data MaybeNew = Fresh CtEvidence | Cached EvTerm
1355
1356 isFresh :: MaybeNew -> Bool
1357 isFresh (Fresh {}) = True
1358 isFresh _ = False
1359
1360 getEvTerm :: MaybeNew -> EvTerm
1361 getEvTerm (Fresh ctev) = ctEvTerm ctev
1362 getEvTerm (Cached tm)  = tm
1363
1364 getEvTerms :: [MaybeNew] -> [EvTerm]
1365 getEvTerms = map getEvTerm
1366
1367 freshGoals :: [MaybeNew] -> [CtEvidence]
1368 freshGoals mns = [ ctev | Fresh ctev <- mns ]
1369
1370 setEvBind :: EvVar -> EvTerm -> TcS ()
1371 setEvBind the_ev t
1372   = do { tc_evbinds <- getTcEvBinds
1373        ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev t
1374
1375        ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr the_ev
1376                                      , text "t  =" <+> ppr t ]
1377
1378 #ifndef DEBUG
1379        ; return () }
1380 #else
1381        ; binds <- getTcEvBindsMap
1382        ; let cycle = reaches_tm binds t
1383        ; when cycle (fail_if_co_loop binds) }
1384
1385   where fail_if_co_loop binds
1386           = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr the_ev
1387                                                            , ppr (evBindMapBinds binds) ]
1388                ; when (isEqVar the_ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) }
1389
1390         reaches_tm :: EvBindMap -> EvTerm -> Bool
1391         -- Does any free variable of 'tm' reach 'the_ev'
1392         reaches_tm ebm tm = foldVarSet ((||) . reaches ebm) False (evVarsOfTerm tm)
1393
1394         reaches :: EvBindMap -> Var -> Bool 
1395         -- Does this evvar reach the_ev? 
1396         reaches ebm ev 
1397           | ev == the_ev                                 = True
1398           | Just (EvBind _ evtrm) <- lookupEvBind ebm ev = reaches_tm ebm evtrm
1399           | otherwise                                    = False
1400 #endif
1401
1402 newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew
1403 newWantedEvVar loc pty
1404   = do { is <- getTcSInerts
1405        ; case lookupInInerts is pty of
1406             Just ctev | not (isDerived ctev) 
1407                       -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
1408                             ; return (Cached (ctEvTerm ctev)) }
1409             _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
1410                     ; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
1411                     ; let ctev = Wanted { ctev_wloc = loc
1412                                         , ctev_pred = pty
1413                                         , ctev_evar = new_ev }
1414                     ; return (Fresh ctev) } }
1415
1416 newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence)
1417 -- Returns Nothing    if cached, 
1418 --         Just pred  if not cached
1419 newDerived loc pty
1420   = do { is <- getTcSInerts
1421        ; case lookupInInerts is pty of
1422             Just {} -> return Nothing
1423             _       -> return (Just Derived { ctev_wloc = loc
1424                                             , ctev_pred = pty }) }
1425     
1426 newKindConstraint :: WantedLoc -> TcTyVar -> Kind -> TcS MaybeNew
1427 -- Create new wanted CoVar that constrains the type to have the specified kind. 
1428 newKindConstraint loc tv knd
1429   = do { ty_k <- wrapTcS (instFlexiTcSHelper (tyVarName tv) knd)
1430        ; newWantedEvVar loc (mkTcEqPred (mkTyVarTy tv) ty_k) }
1431
1432 instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew]
1433 instDFunConstraints wl = mapM (newWantedEvVar wl)
1434 \end{code}
1435                 
1436
1437 Note [xCFlavor]
1438 ~~~~~~~~~~~~~~~
1439 A call might look like this:
1440
1441     xCtFlavor ev subgoal-preds evidence-transformer
1442
1443   ev is Given   => use ev_decomp to create new Givens for subgoal-preds, 
1444                    and return them
1445
1446   ev is Wanted  => create new wanteds for subgoal-preds, 
1447                    use ev_comp to bind ev, 
1448                    return fresh wanteds (ie ones not cached in inert_cans or solved)
1449
1450   ev is Derived => create new deriveds for subgoal-preds 
1451                       (unless cached in inert_cans or solved)
1452
1453 Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
1454       Ones that are already cached are not returned
1455
1456 Example
1457     ev : Tree a b ~ Tree c d
1458     xCtFlavor ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
1459                                      , ev_decomp = \c. [nth 1 c, nth 2 c] })
1460               (\fresh-goals.  stuff)
1461
1462 \begin{code}
1463 xCtFlavor :: CtEvidence              -- Original flavor   
1464           -> [TcPredType]          -- New predicate types
1465           -> XEvTerm               -- Instructions about how to manipulate evidence
1466           -> TcS [CtEvidence]
1467 xCtFlavor = xCtFlavor_cache True          
1468
1469 xCtFlavor_cache :: Bool            -- True = if wanted add to the solved bag!    
1470           -> CtEvidence            -- Original flavor   
1471           -> [TcPredType]          -- New predicate types
1472           -> XEvTerm               -- Instructions about how to manipulate evidence
1473           -> TcS [CtEvidence]
1474 xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
1475   = return [ Given { ctev_gloc = gl, ctev_pred = pred, ctev_evtm = sub_tm } 
1476            | (pred, sub_tm) <- zipEqual "xCtFlavor" ptys (ev_decomp xev tm) ]
1477     -- ToDo: consider creating new evidence variables for superclasses
1478   
1479 xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
1480   = do { new_evars <- mapM (newWantedEvVar wl) ptys
1481        ; setEvBind evar (ev_comp xev (getEvTerms new_evars))
1482
1483            -- Add the now-solved wanted constraint to the cache
1484        ; when cache $ addToSolved ctev
1485
1486        ; return (freshGoals new_evars) }
1487     
1488 xCtFlavor_cache _ (Derived { ctev_wloc = wl }) ptys _xev
1489   = do { ders <- mapM (newDerived wl) ptys
1490        ; return (catMaybes ders) }
1491
1492 -----------------------------
1493 rewriteCtFlavor :: CtEvidence
1494                 -> TcPredType   -- new predicate
1495                 -> TcCoercion   -- new ~ old     
1496                 -> TcS (Maybe CtEvidence)
1497 {- 
1498      rewriteCtFlavor old_fl new_pred co
1499 Main purpose: create a new identity (flavor) for new_pred;
1500               unless new_pred is cached already
1501 * Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl
1502 * If old_fl was wanted, create a binding for old_fl, in terms of new_fl
1503 * If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl
1504 * Returns Nothing if new_fl is already cached
1505
1506
1507         Old evidence    New predicate is               Return new evidence
1508         flavour                                        of same flavor
1509         -------------------------------------------------------------------
1510         Wanted          Already solved or in inert     Nothing
1511         or Derived      Not                            Just new_evidence
1512
1513         Given           Already in inert               Nothing
1514                         Not                            Just new_evidence
1515
1516         Solved          NEVER HAPPENS
1517 -}
1518
1519 rewriteCtFlavor = rewriteCtFlavor_cache True
1520 -- Returns Just new_fl iff either (i)  'co' is reflexivity
1521 --                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1522 -- In either case, there is nothing new to do with new_fl
1523
1524 rewriteCtFlavor_cache :: Bool 
1525                 -> CtEvidence
1526                 -> TcPredType   -- new predicate
1527                 -> TcCoercion   -- new ~ old     
1528                 -> TcS (Maybe CtEvidence)
1529 -- If derived, don't even look at the coercion
1530 -- NB: this allows us to sneak away with ``error'' thunks for 
1531 -- coercions that come from derived ids (which don't exist!) 
1532 rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co
1533   = newDerived wl pty_new
1534         
1535 rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
1536   = return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
1537   where
1538     new_tm = mkEvCast old_tm (mkTcSymCo co)  -- mkEvCase optimises ReflCo
1539   
1540 rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co
1541   | isTcReflCo co  -- If just reflexivity then you may re-use the same variable
1542   = return (Just (if pty_old `eqType` pty_new 
1543                   then ctev 
1544                   else ctev { ctev_pred = pty_new }))
1545        -- If the old and new types compare equal (eqType looks through synonyms)
1546        -- then retain the old type, so that error messages come out mentioning synonyms
1547
1548   | otherwise
1549   = do { new_evar <- newWantedEvVar wl pty_new
1550        ; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
1551
1552            -- Add the now-solved wanted constraint to the cache
1553        ; when cache $ addToSolved ctev
1554
1555        ; case new_evar of
1556             Fresh ctev -> return (Just ctev) 
1557             _          -> return Nothing }
1558
1559
1560
1561 -- Matching and looking up classes and family instances
1562 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1563
1564 data MatchInstResult mi
1565   = MatchInstNo         -- No matching instance 
1566   | MatchInstSingle mi  -- Single matching instance
1567   | MatchInstMany       -- Multiple matching instances
1568
1569
1570 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Maybe TcType])) 
1571 -- Look up a class constraint in the instance environment
1572 matchClass clas tys
1573   = do  { let pred = mkClassPred clas tys 
1574         ; instEnvs <- getInstEnvs
1575 --        ; traceTcS "matchClass" $ empty -- text "instEnvs=" <+> ppr instEnvs
1576         ; case lookupInstEnv instEnvs clas tys of {
1577             ([], unifs, _)               -- Nothing matches  
1578                 -> do { traceTcS "matchClass not matching"
1579                                  (vcat [ text "dict" <+> ppr pred, 
1580                                          text "unifs" <+> ppr unifs,
1581                                          ppr instEnvs ]) 
1582                       ; return MatchInstNo  
1583                       } ;  
1584             ([(ispec, inst_tys)], [], _) -- A single match 
1585                 -> do   { let dfun_id = is_dfun ispec
1586                         ; traceTcS "matchClass success"
1587                                    (vcat [text "dict" <+> ppr pred, 
1588                                           text "witness" <+> ppr dfun_id
1589                                            <+> ppr (idType dfun_id) ])
1590                                   -- Record that this dfun is needed
1591                         ; return $ MatchInstSingle (dfun_id, inst_tys)
1592                         } ;
1593             (matches, unifs, _)          -- More than one matches 
1594                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
1595                                    (vcat [text "dict" <+> ppr pred,
1596                                           text "matches" <+> ppr matches,
1597                                           text "unifs" <+> ppr unifs])
1598                         ; return MatchInstMany 
1599                         }
1600         }
1601         }
1602
1603 matchFam :: TyCon -> [Type] -> TcS (Maybe (FamInst, [Type]))
1604 matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
1605 \end{code}
1606
1607 \begin{code}
1608 -- Deferring forall equalities as implications
1609 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1610
1611 deferTcSForAllEq :: (WantedLoc,EvVar)  -- Original wanted equality flavor
1612                  -> ([TyVar],TcType)   -- ForAll tvs1 body1
1613                  -> ([TyVar],TcType)   -- ForAll tvs2 body2
1614                  -> TcS ()
1615 -- Some of this functionality is repeated from TcUnify, 
1616 -- consider having a single place where we create fresh implications. 
1617 deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
1618  = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
1619       ; let tys  = mkTyVarTys skol_tvs
1620             phi1 = Type.substTy subst1 body1
1621             phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
1622             skol_info = UnifyForAllSkol skol_tvs phi1
1623         ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2)
1624         ; coe_inside <- case mev of
1625             Cached ev_tm -> return (evTermCoercion ev_tm)
1626             Fresh ctev   -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
1627                                ; let ev_binds = TcEvBinds ev_binds_var
1628                                      new_ct = mkNonCanonical ctev
1629                                      new_co = evTermCoercion (ctEvTerm ctev)
1630                                ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
1631                                ; loc <- wrapTcS $ TcM.getCtLoc skol_info
1632                                ; let wc = WC { wc_flat  = singleCt new_ct 
1633                                              , wc_impl  = emptyBag
1634                                              , wc_insol = emptyCts }
1635                                      imp = Implic { ic_untch  = all_untouchables
1636                                                   , ic_env    = lcl_env
1637                                                   , ic_skols  = skol_tvs
1638                                                   , ic_given  = []
1639                                                   , ic_wanted = wc 
1640                                                   , ic_insol  = False
1641                                                   , ic_binds  = ev_binds_var
1642                                                   , ic_loc    = loc }
1643                                ; updTcSImplics (consBag imp) 
1644                                ; return (TcLetCo ev_binds new_co) }
1645
1646         ; setEvBind orig_ev $
1647           EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs)
1648         }
1649  where all_untouchables = TouchableRange u u
1650        u = idUnique orig_ev -- HACK: empty range
1651
1652 \end{code}
1653
1654
1655
1656 -- Rewriting with respect to the inert equalities 
1657 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1658 \begin{code}
1659 getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
1660 getInertEqs = do { inert <- getTcSInerts
1661                  ; let ics = inert_cans inert
1662                  ; return (inert_eqs ics, inert_eq_tvs ics) }
1663
1664 getCtCoercion :: EvBindMap -> Ct -> TcCoercion
1665 -- Precondition: A CTyEqCan which is either Wanted or Given, never Derived or Solved!
1666 getCtCoercion _bs ct 
1667   = ASSERT( not (isDerivedCt ct) )
1668     evTermCoercion (ctEvTerm (ctEvidence ct))
1669 {-       ToDo: check with Dimitrios that we can dump this stuff
1670   = case lookupEvBind bs cc_id of
1671         -- Given and bound to a coercion term
1672       Just (EvBind _ (EvCoercion co)) -> co
1673                 -- NB: The constraint could have been rewritten due to spontaneous 
1674                 -- unifications but because we are optimizing away mkRefls the evidence
1675                 -- variable may still have type (alpha ~ [beta]). The constraint may 
1676                 -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
1677                 -- been previously solved by spontaneous unification). So if we are going 
1678                 -- to use the evidence variable for rewriting other constraints, we'd better 
1679                 -- make sure it's of the right type!
1680                 -- Always the ctPred type is more accurate, so we just pick that type
1681
1682       _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
1683       
1684   where 
1685     cc_id = ctId ct
1686 -}
1687 \end{code}
1688
1689