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