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