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