Merge branch 'master' of http://darcs.haskell.org/ghc
[ghc.git] / compiler / typecheck / TcSMonad.lhs
1 \begin{code}
2 -- Type definitions for the constraint solver
3 module TcSMonad ( 
4
5        -- Canonical constraints
6     CanonicalCts, emptyCCan, andCCan, andCCans, 
7     singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, 
8     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
9     isCFrozenErr,
10
11     WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
12     workListFromEq, workListFromNonEq,
13     workListFromEqs, workListFromNonEqs, foldrWorkListM,
14
15     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
16     deCanonicalise, mkFrozenError,
17
18     isWanted, isGiven, isDerived,
19     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
20
21     isFlexiTcsTv,
22
23     canRewrite, canSolve,
24     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
25     getWantedLoc,
26
27     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
28     traceFireTcS, bumpStepCountTcS,
29     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
30     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
31
32        -- Creation of evidence variables
33     newEvVar, newCoVar, newGivenCoVar,
34     newDerivedId, 
35     newIPVar, newDictVar, newKindConstraint,
36
37        -- Setting evidence variables 
38     setCoBind, setIPBind, setDictBind, setEvBind,
39
40     setWantedTyBind,
41
42     getInstEnvs, getFamInstEnvs,                -- Getting the environments
43     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
44     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
45
46     newFlattenSkolemTy,                         -- Flatten skolems 
47
48
49     instDFunTypes,                              -- Instantiation
50     instDFunConstraints,          
51     newFlexiTcSTy, instFlexiTcS,
52
53     compatKind,
54
55     TcsUntouchables,
56     isTouchableMetaTyVar,
57     isTouchableMetaTyVar_InRange, 
58
59     getDefaultInfo, getDynFlags,
60
61     matchClass, matchFam, MatchInstResult (..), 
62     checkWellStagedDFun, 
63     warnTcS,
64     pprEq                                   -- Smaller utils, re-exported from TcM 
65                                              -- TODO (DV): these are only really used in the 
66                                              -- instance matcher in TcSimplify. I am wondering
67                                              -- if the whole instance matcher simply belongs
68                                              -- here 
69 ) where 
70
71 #include "HsVersions.h"
72
73 import HscTypes
74 import BasicTypes 
75
76 import Inst
77 import InstEnv 
78 import FamInst 
79 import FamInstEnv
80
81 import qualified TcRnMonad as TcM
82 import qualified TcMType as TcM
83 import qualified TcEnv as TcM 
84        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
85 import TcType
86 import DynFlags
87
88 import Coercion
89 import Class
90 import TyCon
91 import TypeRep 
92
93 import Name
94 import Var
95 import VarEnv
96 import Outputable
97 import Bag
98 import MonadUtils
99 import VarSet
100 import FastString
101
102 import HsBinds               -- for TcEvBinds stuff 
103 import Id 
104
105 import TcRnTypes
106 #ifdef DEBUG
107 import Control.Monad( when )
108 #endif
109 import Data.IORef
110 \end{code}
111
112
113 %************************************************************************
114 %*                                                                      *
115 %*                       Canonical constraints                          *
116 %*                                                                      *
117 %*   These are the constraints the low-level simplifier works with      *
118 %*                                                                      *
119 %************************************************************************
120
121 \begin{code}
122 -- Types without any type functions inside.  However, note that xi
123 -- types CAN contain unexpanded type synonyms; however, the
124 -- (transitive) expansions of those type synonyms will not contain any
125 -- type functions.
126 type Xi = Type       -- In many comments, "xi" ranges over Xi
127
128 type CanonicalCts = Bag CanonicalCt
129  
130 data CanonicalCt
131   -- Atomic canonical constraints 
132   = CDictCan {  -- e.g.  Num xi
133       cc_id     :: EvVar,
134       cc_flavor :: CtFlavor, 
135       cc_class  :: Class, 
136       cc_tyargs :: [Xi]
137     }
138
139   | CIPCan {    -- ?x::tau
140       -- See note [Canonical implicit parameter constraints].
141       cc_id     :: EvVar,
142       cc_flavor :: CtFlavor,
143       cc_ip_nm  :: IPName Name,
144       cc_ip_ty  :: TcTauType
145     }
146
147   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
148        -- Invariant: 
149        --   * tv not in tvs(xi)   (occurs check)
150        --   * typeKind xi `compatKind` typeKind tv
151        --       See Note [Spontaneous solving and kind compatibility]
152        --   * We prefer unification variables on the left *JUST* for efficiency
153       cc_id     :: EvVar, 
154       cc_flavor :: CtFlavor, 
155       cc_tyvar  :: TcTyVar, 
156       cc_rhs    :: Xi
157     }
158
159   | CFunEqCan {  -- F xis ~ xi  
160                  -- Invariant: * isSynFamilyTyCon cc_fun 
161                  --            * typeKind (F xis) `compatKind` typeKind xi
162       cc_id     :: EvVar,
163       cc_flavor :: CtFlavor, 
164       cc_fun    :: TyCon,       -- A type function
165       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
166       cc_rhs    :: Xi           --    *never* over-saturated (because if so
167                                 --    we should have decomposed)
168                    
169     }
170
171   | CFrozenErr {      -- A "frozen error" does not interact with anything
172                       -- See Note [Frozen Errors]
173       cc_id     :: EvVar,
174       cc_flavor :: CtFlavor
175     }
176
177 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
178 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
179
180 compatKind :: Kind -> Kind -> Bool
181 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
182
183 deCanonicalise :: CanonicalCt -> FlavoredEvVar
184 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
185
186 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
187 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
188 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
189 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
190 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
191 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
192
193 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
194 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
195 tyVarsOfCDict _ct                            = emptyVarSet 
196
197 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
198 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
199
200 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
201 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
202
203 instance Outputable CanonicalCt where
204   ppr (CDictCan d fl cls tys)     
205       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
206   ppr (CIPCan ip fl ip_nm ty)     
207       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
208   ppr (CTyEqCan co fl tv ty)      
209       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
210   ppr (CFunEqCan co fl tc tys ty) 
211       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
212   ppr (CFrozenErr co fl)
213       = ppr fl <+> pprEvVarWithType co
214 \end{code}
215
216 Note [Canonical implicit parameter constraints]
217 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
218 The type in a canonical implicit parameter constraint doesn't need to
219 be a xi (type-function-free type) since we can defer the flattening
220 until checking this type for equality with another type.  If we
221 encounter two IP constraints with the same name, they MUST have the
222 same type, and at that point we can generate a flattened equality
223 constraint between the types.  (On the other hand, the types in two
224 class constraints for the same class MAY be equal, so they need to be
225 flattened in the first place to facilitate comparing them.)
226
227 \begin{code}
228 singleCCan :: CanonicalCt -> CanonicalCts 
229 singleCCan = unitBag 
230
231 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
232 andCCan = unionBags
233
234 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
235 extendCCans = snocBag 
236
237 andCCans :: [CanonicalCts] -> CanonicalCts 
238 andCCans = unionManyBags
239
240 emptyCCan :: CanonicalCts 
241 emptyCCan = emptyBag
242
243 isEmptyCCan :: CanonicalCts -> Bool
244 isEmptyCCan = isEmptyBag
245
246 isCTyEqCan :: CanonicalCt -> Bool 
247 isCTyEqCan (CTyEqCan {})  = True 
248 isCTyEqCan (CFunEqCan {}) = False
249 isCTyEqCan _              = False 
250
251 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
252 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
253 isCDictCan_Maybe _              = Nothing
254
255 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
256 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
257 isCIPCan_Maybe _                = Nothing
258
259 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
260 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
261 isCFunEqCan_Maybe _ = Nothing
262
263 isCFrozenErr :: CanonicalCt -> Bool
264 isCFrozenErr (CFrozenErr {}) = True
265 isCFrozenErr _               = False
266
267
268 -- A mixture of Given, Wanted, and Derived constraints. 
269 -- We split between equalities and the rest to process equalities first. 
270 data WorkList = WorkList { weqs  :: CanonicalCts 
271                                  -- NB: weqs includes equalities /and/ family equalities
272                          , wrest :: CanonicalCts }
273
274 unionWorkList :: WorkList -> WorkList -> WorkList
275 unionWorkList wl1 wl2
276   = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
277              , wrest = wrest wl1 `andCCan` wrest wl2 }
278
279 unionWorkLists :: [WorkList] -> WorkList 
280 unionWorkLists = foldr unionWorkList emptyWorkList
281
282 isEmptyWorkList :: WorkList -> Bool
283 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
284
285 emptyWorkList :: WorkList
286 emptyWorkList
287   = WorkList { weqs = emptyBag, wrest = emptyBag }
288
289 workListFromEq :: CanonicalCt -> WorkList
290 workListFromEq = workListFromEqs . singleCCan
291
292 workListFromNonEq :: CanonicalCt -> WorkList
293 workListFromNonEq = workListFromNonEqs . singleCCan 
294
295 workListFromNonEqs :: CanonicalCts -> WorkList
296 workListFromNonEqs cts
297   = WorkList { weqs = emptyCCan, wrest = cts }
298
299 workListFromEqs :: CanonicalCts -> WorkList
300 workListFromEqs cts
301   = WorkList { weqs = cts, wrest = emptyCCan }
302
303 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r) 
304                            -> r -> WorkList -> m r
305 -- Prioritizes equalities
306 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
307   = do { r1 <- foldrBagM on_ct r eqs
308        ; foldrBagM on_ct r1 rest }
309
310 instance Outputable WorkList where 
311   ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
312                 , text "WorkList (Other)      = " <+> ppr (wrest wl) ]
313
314 \end{code}
315
316
317
318 %************************************************************************
319 %*                                                                      *
320                     CtFlavor
321          The "flavor" of a canonical constraint
322 %*                                                                      *
323 %************************************************************************
324
325 \begin{code}
326 getWantedLoc :: CanonicalCt -> WantedLoc
327 getWantedLoc ct 
328   = ASSERT (isWanted (cc_flavor ct))
329     case cc_flavor ct of 
330       Wanted wl -> wl 
331       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
332
333 isWantedCt :: CanonicalCt -> Bool
334 isWantedCt ct = isWanted (cc_flavor ct)
335 isGivenCt :: CanonicalCt -> Bool
336 isGivenCt ct = isGiven (cc_flavor ct)
337 isDerivedCt :: CanonicalCt -> Bool
338 isDerivedCt ct = isDerived (cc_flavor ct)
339
340 canSolve :: CtFlavor -> CtFlavor -> Bool 
341 -- canSolve ctid1 ctid2 
342 -- The constraint ctid1 can be used to solve ctid2 
343 -- "to solve" means a reaction where the active parts of the two constraints match.
344 --  active(F xis ~ xi) = F xis 
345 --  active(tv ~ xi)    = tv 
346 --  active(D xis)      = D xis 
347 --  active(IP nm ty)   = nm 
348 --
349 -- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
350 -----------------------------------------
351 canSolve (Given {})   _            = True 
352 canSolve (Wanted {})  (Derived {}) = True
353 canSolve (Wanted {})  (Wanted {})  = True
354 canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
355 canSolve _ _ = False                       -- (There is no *evidence* for a derived.)
356
357 canRewrite :: CtFlavor -> CtFlavor -> Bool 
358 -- canRewrite ctid1 ctid2 
359 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
360 canRewrite = canSolve 
361
362 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
363 -- Precondition: At least one of them should be wanted 
364 combineCtLoc (Wanted loc) _    = loc 
365 combineCtLoc _ (Wanted loc)    = loc 
366 combineCtLoc (Derived loc ) _  = loc 
367 combineCtLoc _ (Derived loc )  = loc 
368 combineCtLoc _ _ = panic "combineCtLoc: both given"
369
370 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
371 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk)
372 mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk)
373 mkGivenFlavor (Given   loc) sk  = Given (setCtLocOrigin loc sk)
374
375
376 mkWantedFlavor :: CtFlavor -> CtFlavor
377 mkWantedFlavor (Wanted  loc) = Wanted loc
378 mkWantedFlavor (Derived loc) = Wanted loc
379 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
380 \end{code}
381
382 %************************************************************************
383 %*                                                                      *
384 %*              The TcS solver monad                                    *
385 %*                                                                      *
386 %************************************************************************
387
388 Note [The TcS monad]
389 ~~~~~~~~~~~~~~~~~~~~
390 The TcS monad is a weak form of the main Tc monad
391
392 All you can do is
393     * fail
394     * allocate new variables
395     * fill in evidence variables
396
397 Filling in a dictionary evidence variable means to create a binding
398 for it, so TcS carries a mutable location where the binding can be
399 added.  This is initialised from the innermost implication constraint.
400
401 \begin{code}
402 data TcSEnv
403   = TcSEnv { 
404       tcs_ev_binds :: EvBindsVar,
405           -- Evidence bindings
406
407       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
408           -- Global type bindings
409
410       tcs_context :: SimplContext,
411                      
412       tcs_untch :: TcsUntouchables,
413
414       tcs_ic_depth :: Int,      -- Implication nesting depth
415       tcs_count    :: IORef Int -- Global step count
416     }
417
418 type TcsUntouchables = (Untouchables,TcTyVarSet)
419 -- Like the TcM Untouchables, 
420 -- but records extra TcsTv variables generated during simplification
421 -- See Note [Extra TcsTv untouchables] in TcSimplify
422 \end{code}
423
424 \begin{code}
425 data SimplContext
426   = SimplInfer SDoc        -- Inferring type of a let-bound thing
427   | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
428   | SimplInteractive       -- Inferring type at GHCi prompt
429   | SimplCheck SDoc        -- Checking a type signature or RULE rhs
430
431 instance Outputable SimplContext where
432   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
433   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
434   ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
435   ppr SimplInteractive = ptext (sLit "SimplInteractive")
436
437 isInteractive :: SimplContext -> Bool
438 isInteractive SimplInteractive = True
439 isInteractive _                = False
440
441 simplEqsOnly :: SimplContext -> Bool
442 -- Simplify equalities only, not dictionaries
443 -- This is used for the LHS of rules; ee
444 -- Note [Simplifying RULE lhs constraints] in TcSimplify
445 simplEqsOnly (SimplRuleLhs {}) = True
446 simplEqsOnly _                 = False
447
448 performDefaulting :: SimplContext -> Bool
449 performDefaulting (SimplInfer {})   = False
450 performDefaulting (SimplRuleLhs {}) = False
451 performDefaulting SimplInteractive  = True
452 performDefaulting (SimplCheck {})   = True
453
454 ---------------
455 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
456
457 instance Functor TcS where
458   fmap f m = TcS $ fmap f . unTcS m
459
460 instance Monad TcS where 
461   return x  = TcS (\_ -> return x) 
462   fail err  = TcS (\_ -> fail err) 
463   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
464
465 -- Basic functionality 
466 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
467 wrapTcS :: TcM a -> TcS a 
468 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
469 -- and TcS is supposed to have limited functionality
470 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
471
472 wrapErrTcS :: TcM a -> TcS a 
473 -- The thing wrapped should just fail
474 -- There's no static check; it's up to the user
475 -- Having a variant for each error message is too painful
476 wrapErrTcS = wrapTcS
477
478 wrapWarnTcS :: TcM a -> TcS a 
479 -- The thing wrapped should just add a warning, or no-op
480 -- There's no static check; it's up to the user
481 wrapWarnTcS = wrapTcS
482
483 failTcS, panicTcS :: SDoc -> TcS a
484 failTcS      = wrapTcS . TcM.failWith
485 panicTcS doc = pprPanic "TcCanonical" doc
486
487 traceTcS :: String -> SDoc -> TcS ()
488 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
489
490 bumpStepCountTcS :: TcS ()
491 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
492                                     ; n <- TcM.readTcRef ref
493                                     ; TcM.writeTcRef ref (n+1) }
494
495 traceFireTcS :: Int -> SDoc -> TcS ()
496 -- Dump a rule-firing trace
497 traceFireTcS depth doc 
498   = TcS $ \env -> 
499     TcM.ifDOptM Opt_D_dump_cs_trace $ 
500     do { n <- TcM.readTcRef (tcs_count env)
501        ; let msg = int n 
502                 <> text (replicate (tcs_ic_depth env) '>')
503                 <> brackets (int depth) <+> doc
504        ; TcM.dumpTcRn msg }
505
506 runTcS :: SimplContext
507        -> Untouchables         -- Untouchables
508        -> TcS a                -- What to run
509        -> TcM (a, Bag EvBind)
510 runTcS context untouch tcs 
511   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
512        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
513        ; step_count <- TcM.newTcRef 0
514        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
515                           , tcs_ty_binds = ty_binds_var
516                           , tcs_context  = context
517                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
518                           , tcs_count    = step_count
519                           , tcs_ic_depth = 0
520                           }
521
522              -- Run the computation
523        ; res <- unTcS tcs env
524              -- Perform the type unifications required
525        ; ty_binds <- TcM.readTcRef ty_binds_var
526        ; mapM_ do_unification (varEnvElts ty_binds)
527
528 #ifdef DEBUG
529        ; count <- TcM.readTcRef step_count
530        ; when (count > 0) $
531          TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
532                             <+> int count <+> ppr context)
533 #endif
534              -- And return
535        ; ev_binds      <- TcM.readTcRef evb_ref
536        ; return (res, evBindMapBinds ev_binds) }
537   where
538     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
539
540 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
541 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
542   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds 
543                    , tcs_untch = (_outer_range, outer_tcs)
544                    , tcs_count = count
545                    , tcs_ic_depth = idepth
546                    , tcs_context = ctxt } ->
547     let 
548        inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
549                    -- The inner_range should be narrower than the outer one
550                    -- (thus increasing the set of untouchables) but 
551                    -- the inner Tcs-untouchables must be unioned with the
552                    -- outer ones!
553        nest_env = TcSEnv { tcs_ev_binds = ref
554                          , tcs_ty_binds = ty_binds
555                          , tcs_untch    = inner_untch
556                          , tcs_count    = count
557                          , tcs_ic_depth = idepth+1
558                          , tcs_context  = ctxtUnderImplic ctxt }
559     in 
560     thing_inside nest_env
561
562 recoverTcS :: TcS a -> TcS a -> TcS a
563 recoverTcS (TcS recovery_code) (TcS thing_inside)
564   = TcS $ \ env ->
565     TcM.recoverM (recovery_code env) (thing_inside env)
566
567 ctxtUnderImplic :: SimplContext -> SimplContext
568 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
569 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 
570                                                <+> doubleQuotes (ftext n))
571 ctxtUnderImplic ctxt              = ctxt
572
573 tryTcS :: TcS a -> TcS a
574 -- Like runTcS, but from within the TcS monad 
575 -- Ignore all the evidence generated, and do not affect caller's evidence!
576 tryTcS tcs 
577   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
578                     ; ev_binds_var <- TcM.newTcEvBinds
579                     ; let env1 = env { tcs_ev_binds = ev_binds_var
580                                      , tcs_ty_binds = ty_binds_var }
581                     ; unTcS tcs env1 })
582
583 -- Update TcEvBinds 
584 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585
586 getDynFlags :: TcS DynFlags
587 getDynFlags = wrapTcS TcM.getDOpts
588
589 getTcSContext :: TcS SimplContext
590 getTcSContext = TcS (return . tcs_context)
591
592 getTcEvBinds :: TcS EvBindsVar
593 getTcEvBinds = TcS (return . tcs_ev_binds) 
594
595 getUntouchables :: TcS TcsUntouchables
596 getUntouchables = TcS (return . tcs_untch)
597
598 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
599 getTcSTyBinds = TcS (return . tcs_ty_binds)
600
601 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
602 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
603
604
605 getTcEvBindsBag :: TcS EvBindMap
606 getTcEvBindsBag
607   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
608        ; wrapTcS $ TcM.readTcRef ev_ref }
609
610 setCoBind :: CoVar -> Coercion -> TcS () 
611 setCoBind cv co = setEvBind cv (EvCoercion co)
612
613 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
614 -- Add a type binding
615 -- We never do this twice!
616 setWantedTyBind tv ty 
617   = do { ref <- getTcSTyBinds
618        ; wrapTcS $ 
619          do { ty_binds <- TcM.readTcRef ref
620 #ifdef DEBUG
621             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
622               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
623                    , ppr tv <+> text ":=" <+> ppr ty
624                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
625 #endif
626             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
627
628 setIPBind :: EvVar -> EvTerm -> TcS () 
629 setIPBind = setEvBind 
630
631 setDictBind :: EvVar -> EvTerm -> TcS () 
632 setDictBind = setEvBind 
633
634 setEvBind :: EvVar -> EvTerm -> TcS () 
635 -- Internal
636 setEvBind ev rhs 
637   = do { tc_evbinds <- getTcEvBinds
638        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
639
640 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
641 warnTcS loc warn_if doc 
642   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
643   | otherwise = return ()
644
645 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
646 getDefaultInfo 
647   = do { ctxt <- getTcSContext
648        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
649        ; return (ctxt, tys, flags) }
650
651 -- Just get some environments needed for instance looking up and matching
652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
653
654 getInstEnvs :: TcS (InstEnv, InstEnv) 
655 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
656
657 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
658 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
659
660 getTopEnv :: TcS HscEnv 
661 getTopEnv = wrapTcS $ TcM.getTopEnv 
662
663 getGblEnv :: TcS TcGblEnv 
664 getGblEnv = wrapTcS $ TcM.getGblEnv 
665
666 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
667 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
668
669 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
670 checkWellStagedDFun pred dfun_id loc 
671   = wrapTcS $ TcM.setCtLoc loc $ 
672     do { use_stage <- TcM.getStage
673        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
674   where
675     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
676     bind_lvl = TcM.topIdLvl dfun_id
677
678 pprEq :: TcType -> TcType -> SDoc
679 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
680
681 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
682 isTouchableMetaTyVar tv 
683   = do { untch <- getUntouchables
684        ; return $ isTouchableMetaTyVar_InRange untch tv } 
685
686 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
687 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
688   = case tcTyVarDetails tv of 
689       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
690                         -- See Note [Touchable meta type variables] 
691       MetaTv {}      -> inTouchableRange untch tv 
692       _              -> False 
693
694
695 \end{code}
696
697
698 Note [Touchable meta type variables]
699 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
700 Meta type variables allocated *by the constraint solver itself* are always
701 touchable.  Example: 
702    instance C a b => D [a] where...
703 if we use this instance declaration we "make up" a fresh meta type
704 variable for 'b', which we must later guess.  (Perhaps C has a
705 functional dependency.)  But since we aren't in the constraint *generator*
706 we can't allocate a Unique in the touchable range for this implication
707 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
708
709
710 \begin{code}
711 -- Flatten skolems
712 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
713
714 newFlattenSkolemTy :: TcType -> TcS TcType
715 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
716
717 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
718 newFlattenSkolemTyVar ty
719   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
720                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
721                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
722        ; traceTcS "New Flatten Skolem Born" $ 
723            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
724        ; return tv }
725
726 -- Instantiations 
727 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728
729 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
730 instDFunTypes mb_inst_tys 
731   = mapM inst_tv mb_inst_tys
732   where
733     inst_tv :: Either TyVar TcType -> TcS Type
734     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
735     inst_tv (Right ty) = return ty 
736
737 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
738 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
739
740
741 instFlexiTcS :: TyVar -> TcS TcTyVar 
742 -- Like TcM.instMetaTyVar but the variable that is created is always
743 -- touchable; we are supposed to guess its instantiation. 
744 -- See Note [Touchable meta type variables] 
745 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
746
747 newFlexiTcSTy :: Kind -> TcS TcType  
748 newFlexiTcSTy knd 
749   = wrapTcS $
750     do { uniq <- TcM.newUnique 
751        ; ref  <- TcM.newMutVar  Flexi 
752        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
753        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
754
755 isFlexiTcsTv :: TyVar -> Bool
756 isFlexiTcsTv tv
757   | not (isTcTyVar tv)                  = False
758   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
759   | otherwise                           = False
760
761 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
762 -- Create new wanted CoVar that constrains the type to have the specified kind. 
763 newKindConstraint tv knd 
764   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
765        ; let ty_k = mkTyVarTy tv_k
766        ; co_var <- newCoVar (mkTyVarTy tv) ty_k
767        ; return co_var }
768
769 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
770 instFlexiTcSHelper tvname tvkind
771   = wrapTcS $ 
772     do { uniq <- TcM.newUnique 
773        ; ref  <- TcM.newMutVar  Flexi 
774        ; let name = setNameUnique tvname uniq 
775              kind = tvkind 
776        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
777
778 -- Superclasses and recursive dictionaries 
779 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
780
781 newEvVar :: TcPredType -> TcS EvVar
782 newEvVar pty = wrapTcS $ TcM.newEvVar pty
783
784 newDerivedId :: TcPredType -> TcS EvVar 
785 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
786
787 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
788 -- Note we create immutable variables for given or derived, since we
789 -- must bind them to TcEvBinds (because their evidence may involve 
790 -- superclasses). However we should be able to override existing
791 -- 'derived' evidence, even in TcEvBinds 
792 newGivenCoVar ty1 ty2 co 
793   = do { cv <- newCoVar ty1 ty2
794        ; setEvBind cv (EvCoercion co) 
795        ; return cv } 
796
797 newCoVar :: TcType -> TcType -> TcS EvVar
798 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
799
800 newIPVar :: IPName Name -> TcType -> TcS EvVar 
801 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
802
803 newDictVar :: Class -> [TcType] -> TcS EvVar 
804 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
805 \end{code} 
806
807
808 \begin{code} 
809 -- Matching and looking up classes and family instances
810 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
811
812 data MatchInstResult mi
813   = MatchInstNo         -- No matching instance 
814   | MatchInstSingle mi  -- Single matching instance
815   | MatchInstMany       -- Multiple matching instances
816
817
818 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
819 -- Look up a class constraint in the instance environment
820 matchClass clas tys
821   = do  { let pred = mkClassPred clas tys 
822         ; instEnvs <- getInstEnvs
823         ; case lookupInstEnv instEnvs clas tys of {
824             ([], unifs)               -- Nothing matches  
825                 -> do { traceTcS "matchClass not matching"
826                                  (vcat [ text "dict" <+> ppr pred, 
827                                          text "unifs" <+> ppr unifs ]) 
828                       ; return MatchInstNo  
829                       } ;  
830             ([(ispec, inst_tys)], []) -- A single match 
831                 -> do   { let dfun_id = is_dfun ispec
832                         ; traceTcS "matchClass success"
833                                    (vcat [text "dict" <+> ppr pred, 
834                                           text "witness" <+> ppr dfun_id
835                                            <+> ppr (idType dfun_id) ])
836                                   -- Record that this dfun is needed
837                         ; return $ MatchInstSingle (dfun_id, inst_tys)
838                         } ;
839             (matches, unifs)          -- More than one matches 
840                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
841                                    (vcat [text "dict" <+> ppr pred,
842                                           text "matches" <+> ppr matches,
843                                           text "unifs" <+> ppr unifs])
844                         ; return MatchInstMany 
845                         }
846         }
847         }
848
849 matchFam :: TyCon
850          -> [Type] 
851          -> TcS (MatchInstResult (TyCon, [Type]))
852 matchFam tycon args
853   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
854        ; case mb of 
855            Nothing  -> return MatchInstNo 
856            Just res -> return $ MatchInstSingle res
857        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
858        -- multiple matches. Check. 
859        }
860 \end{code}