Optimised the representation of Inert Sets to use Maps to get to the relevant inert...
[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
10     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
11     mkWantedConstraints, deCanonicaliseWanted, 
12     makeGivens, makeSolvedByInst,
13
14     CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, 
15     isGivenCt, isWantedCt, 
16
17     DerivedOrig (..), 
18     canRewrite, canSolve,
19     combineCtLoc, mkGivenFlavor,
20
21     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
22     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
23     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
24        
25        -- Creation of evidence variables
26
27     newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar, 
28     newIPVar, newDictVar, newKindConstraint,
29
30        -- Setting evidence variables 
31     setWantedCoBind, setDerivedCoBind, 
32     setIPBind, setDictBind, setEvBind,
33
34     setWantedTyBind,
35
36     newTcEvBindsTcS,
37  
38     getInstEnvs, getFamInstEnvs,                -- Getting the environments 
39     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
40     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
41
42
43     newFlattenSkolemTy,                         -- Flatten skolems 
44
45
46     instDFunTypes,                              -- Instantiation
47     instDFunConstraints,                        
48
49     isGoodRecEv,
50
51     zonkTcTypeTcS,                              -- Zonk through the TyBinds of the Tcs Monad
52     compatKind,
53
54
55     isTouchableMetaTyVar,
56     isTouchableMetaTyVar_InRange, 
57
58     getDefaultInfo, getDynFlags,
59
60     matchClass, matchFam, MatchInstResult (..), 
61     checkWellStagedDFun, 
62     warnTcS,
63     pprEq,                                   -- Smaller utils, re-exported from TcM 
64                                              -- TODO (DV): these are only really used in the 
65                                              -- instance matcher in TcSimplify. I am wondering
66                                              -- if the whole instance matcher simply belongs
67                                              -- here 
68
69
70     mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
71
72 ) where 
73
74 #include "HsVersions.h"
75
76 import HscTypes
77 import BasicTypes 
78
79 import Inst
80 import InstEnv 
81 import FamInst 
82 import FamInstEnv
83
84 import NameSet ( addOneToNameSet ) 
85
86 import qualified TcRnMonad as TcM
87 import qualified TcMType as TcM
88 import qualified TcEnv as TcM 
89        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
90 import TcType
91 import Module 
92 import DynFlags
93
94 import Coercion
95 import Class
96 import TyCon
97 import TypeRep 
98
99 import Name
100 import Var
101 import VarEnv
102 import Outputable
103 import Bag
104 import MonadUtils
105 import VarSet
106 import FastString
107
108 import HsBinds               -- for TcEvBinds stuff 
109 import Id 
110 import FunDeps
111
112 import TcRnTypes
113
114 import Data.IORef
115 \end{code}
116
117
118 %************************************************************************
119 %*                                                                      *
120 %*                       Canonical constraints                          *
121 %*                                                                      *
122 %*   These are the constraints the low-level simplifier works with      *
123 %*                                                                      *
124 %************************************************************************
125
126 \begin{code}
127 -- Types without any type functions inside.  However, note that xi
128 -- types CAN contain unexpanded type synonyms; however, the
129 -- (transitive) expansions of those type synonyms will not contain any
130 -- type functions.
131 type Xi = Type       -- In many comments, "xi" ranges over Xi
132
133 type CanonicalCts = Bag CanonicalCt
134  
135 data CanonicalCt
136   -- Atomic canonical constraints 
137   = CDictCan {  -- e.g.  Num xi
138       cc_id     :: EvVar,
139       cc_flavor :: CtFlavor, 
140       cc_class  :: Class, 
141       cc_tyargs :: [Xi]
142     }
143
144   | CIPCan {    -- ?x::tau
145       -- See note [Canonical implicit parameter constraints].
146       cc_id     :: EvVar,
147       cc_flavor :: CtFlavor,
148       cc_ip_nm  :: IPName Name,
149       cc_ip_ty  :: TcTauType
150     }
151
152   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
153        -- Invariant: 
154        --   * tv not in tvs(xi)   (occurs check)
155        --   * If constraint is given then typeKind xi `compatKind` typeKind tv 
156        --                See Note [Spontaneous solving and kind compatibility] 
157        --   * If 'xi' is a flatten skolem then 'tv' can only be: 
158        --              - a flatten skolem or a unification variable
159        --     i.e. equalities prefer flatten skolems in their LHS 
160        --     See Note [Loopy Spontaneous Solving, Example 4]
161        --     Also related to [Flatten Skolem Equivalence Classes]
162       cc_id     :: EvVar, 
163       cc_flavor :: CtFlavor, 
164       cc_tyvar  :: TcTyVar, 
165       cc_rhs    :: Xi
166     }
167
168   | CFunEqCan {  -- F xis ~ xi  
169                  -- Invariant: * isSynFamilyTyCon cc_fun 
170                  --            * cc_rhs is not a touchable unification variable 
171                  --                   See Note [No touchables as FunEq RHS]
172                  --            * If constraint is given then 
173                  --                 typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
174       cc_id     :: EvVar,
175       cc_flavor :: CtFlavor, 
176       cc_fun    :: TyCon,       -- A type function
177       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
178       cc_rhs    :: Xi           --    *never* over-saturated (because if so
179                                 --    we should have decomposed)
180                    
181     }
182
183 compatKind :: Kind -> Kind -> Bool 
184 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
185
186 makeGivens :: CanonicalCts -> CanonicalCts
187 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
188            -- The UnkSkol doesn't matter because these givens are
189            -- not contradictory (else we'd have rejected them already)
190
191 makeSolvedByInst :: CanonicalCt -> CanonicalCt
192 -- Record that a constraint is now solved
193 --        Wanted         -> Derived
194 --        Given, Derived -> no-op
195 makeSolvedByInst ct 
196   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
197   | otherwise                  = ct
198
199 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
200 mkWantedConstraints flats implics 
201   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
202
203 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
204 deCanonicaliseWanted ct 
205   = WARN( not (isWanted $ cc_flavor ct), ppr ct ) 
206     let Wanted loc = cc_flavor ct 
207     in WantedEvVar (cc_id ct) loc
208
209 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
210 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
211 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
212 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
213 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
214
215 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
216 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
217 tyVarsOfCDict _ct                            = emptyVarSet 
218
219 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
220 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
221
222 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
223 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
224
225 instance Outputable CanonicalCt where
226   ppr (CDictCan d fl cls tys)     
227       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
228   ppr (CIPCan ip fl ip_nm ty)     
229       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
230   ppr (CTyEqCan co fl tv ty)      
231       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
232   ppr (CFunEqCan co fl tc tys ty) 
233       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
234 \end{code}
235
236
237 Note [No touchables as FunEq RHS]
238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
239 Notice that (F xis ~ beta), where beta is an touchable unification
240 variable, is not canonical.  Why?  
241   * If (F xis ~ beta) was the only wanted constraint, we'd 
242     definitely want to spontaneously-unify it
243
244   * But suppose we had an earlier wanted (beta ~ Int), and 
245     have already spontaneously unified it.  Then we have an
246     identity given (id : beta ~ Int) in the inert set.  
247
248   * But (F xis ~ beta) does not react with that given (because we
249     don't subsitute on the RHS of a function equality).  So there's a
250     serious danger that we'd spontaneously unify it a second time.
251
252 Hence the invariant.
253
254 The invariant is 
255
256 Note [Canonical implicit parameter constraints]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 The type in a canonical implicit parameter constraint doesn't need to
259 be a xi (type-function-free type) since we can defer the flattening
260 until checking this type for equality with another type.  If we
261 encounter two IP constraints with the same name, they MUST have the
262 same type, and at that point we can generate a flattened equality
263 constraint between the types.  (On the other hand, the types in two
264 class constraints for the same class MAY be equal, so they need to be
265 flattened in the first place to facilitate comparing them.)
266
267 \begin{code}
268 singleCCan :: CanonicalCt -> CanonicalCts 
269 singleCCan = unitBag 
270
271 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
272 andCCan = unionBags
273
274 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
275 extendCCans = snocBag 
276
277 andCCans :: [CanonicalCts] -> CanonicalCts 
278 andCCans = unionManyBags
279
280 emptyCCan :: CanonicalCts 
281 emptyCCan = emptyBag
282
283 isEmptyCCan :: CanonicalCts -> Bool
284 isEmptyCCan = isEmptyBag
285
286 isCTyEqCan :: CanonicalCt -> Bool 
287 isCTyEqCan (CTyEqCan {})  = True 
288 isCTyEqCan (CFunEqCan {}) = False
289 isCTyEqCan _              = False 
290
291 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
292 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
293 isCDictCan_Maybe _              = Nothing
294
295 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
296 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
297 isCIPCan_Maybe _                = Nothing
298
299 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
300 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
301 isCFunEqCan_Maybe _ = Nothing
302
303 \end{code}
304
305 %************************************************************************
306 %*                                                                      *
307                     CtFlavor
308          The "flavor" of a canonical constraint
309 %*                                                                      *
310 %************************************************************************
311
312 \begin{code}
313 data CtFlavor 
314   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
315   | Derived WantedLoc DerivedOrig
316                       -- We have evidence for this constraint in TcEvBinds;
317                       --   *however* this evidence can contain wanteds, so 
318                       --   it's valid only provisionally to the solution of
319                       --   these wanteds 
320   | Wanted WantedLoc  -- We have no evidence bindings for this constraint. 
321
322 data DerivedOrig = DerSC | DerInst 
323 -- Deriveds are either superclasses of other wanteds or deriveds, or partially 
324 -- solved wanteds from instances. 
325
326 instance Outputable CtFlavor where 
327   ppr (Given _)    = ptext (sLit "[Given]")
328   ppr (Wanted _)   = ptext (sLit "[Wanted]")
329   ppr (Derived {}) = ptext (sLit "[Derived]") 
330
331 isWanted :: CtFlavor -> Bool 
332 isWanted (Wanted {}) = True
333 isWanted _           = False
334
335 isGiven :: CtFlavor -> Bool 
336 isGiven (Given {}) = True 
337 isGiven _          = False 
338
339 isDerived :: CtFlavor -> Bool 
340 isDerived (Derived {}) = True
341 isDerived _            = False
342
343 isDerivedSC :: CtFlavor -> Bool 
344 isDerivedSC (Derived _ DerSC) = True 
345 isDerivedSC _                 = False 
346
347 isDerivedByInst :: CtFlavor -> Bool 
348 isDerivedByInst (Derived _ DerInst) = True 
349 isDerivedByInst _                   = False 
350
351 isWantedCt :: CanonicalCt -> Bool 
352 isWantedCt ct = isWanted (cc_flavor ct)
353 isGivenCt :: CanonicalCt -> Bool 
354 isGivenCt ct = isGiven (cc_flavor ct) 
355
356 canSolve :: CtFlavor -> CtFlavor -> Bool 
357 -- canSolve ctid1 ctid2 
358 -- The constraint ctid1 can be used to solve ctid2 
359 -- "to solve" means a reaction where the active parts of the two constraints match.
360 --  active(F xis ~ xi) = F xis 
361 --  active(tv ~ xi)    = tv 
362 --  active(D xis)      = D xis 
363 --  active(IP nm ty)   = nm 
364 -----------------------------------------
365 canSolve (Given {})   _            = True 
366 canSolve (Derived {}) (Wanted {})  = True 
367 canSolve (Derived {}) (Derived {}) = True 
368 canSolve (Wanted {})  (Wanted {})  = True
369 canSolve _ _ = False
370
371 canRewrite :: CtFlavor -> CtFlavor -> Bool 
372 -- canRewrite ctid1 ctid2 
373 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
374 canRewrite = canSolve 
375
376 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
377 -- Precondition: At least one of them should be wanted 
378 combineCtLoc (Wanted loc) _    = loc 
379 combineCtLoc _ (Wanted loc)    = loc 
380 combineCtLoc (Derived loc _) _ = loc 
381 combineCtLoc _ (Derived loc _) = loc 
382 combineCtLoc _ _ = panic "combineCtLoc: both given"
383
384 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
385 mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
386 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
387 mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
388 \end{code}
389
390
391 %************************************************************************
392 %*                                                                      *
393 %*              The TcS solver monad                                    *
394 %*                                                                      *
395 %************************************************************************
396
397 Note [The TcS monad]
398 ~~~~~~~~~~~~~~~~~~~~
399 The TcS monad is a weak form of the main Tc monad
400
401 All you can do is
402     * fail
403     * allocate new variables
404     * fill in evidence variables
405
406 Filling in a dictionary evidence variable means to create a binding
407 for it, so TcS carries a mutable location where the binding can be
408 added.  This is initialised from the innermost implication constraint.
409
410 \begin{code}
411 data TcSEnv
412   = TcSEnv { 
413       tcs_ev_binds :: EvBindsVar,
414           -- Evidence bindings
415
416       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
417           -- Global type bindings
418
419       tcs_context :: SimplContext,
420
421       tcs_untch :: Untouchables
422     }
423
424 data SimplContext
425   = SimplInfer          -- Inferring type of a let-bound thing
426   | SimplRuleLhs        -- Inferring type of a RULE lhs
427   | SimplInteractive    -- Inferring type at GHCi prompt
428   | SimplCheck          -- Checking a type signature or RULE rhs
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 traceTcS0 :: String -> SDoc -> TcS ()
490 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
491
492 runTcS :: SimplContext
493        -> Untouchables         -- Untouchables
494        -> TcS a                -- What to run
495        -> TcM (a, Bag EvBind)
496 runTcS context untouch tcs 
497   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
498        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
499        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
500                           , tcs_ty_binds = ty_binds_var
501                           , tcs_context = context
502                           , tcs_untch   = untouch }
503
504              -- Run the computation
505        ; res <- unTcS tcs env
506
507              -- Perform the type unifications required
508        ; ty_binds <- TcM.readTcRef ty_binds_var
509        ; mapM_ do_unification (varEnvElts ty_binds)
510
511              -- And return
512        ; ev_binds <- TcM.readTcRef evb_ref
513        ; return (res, evBindMapBinds ev_binds) }
514   where
515     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
516
517        
518 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a 
519 nestImplicTcS ref untch (TcS thing_inside)
520   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> 
521     let 
522        nest_env = TcSEnv { tcs_ev_binds = ref
523                          , tcs_ty_binds = ty_binds
524                          , tcs_untch    = untch
525                          , tcs_context  = ctxtUnderImplic ctxt }
526     in 
527     thing_inside nest_env
528
529 recoverTcS :: TcS a -> TcS a -> TcS a
530 recoverTcS (TcS recovery_code) (TcS thing_inside)
531   = TcS $ \ env ->
532     TcM.recoverM (recovery_code env) (thing_inside env)
533
534 ctxtUnderImplic :: SimplContext -> SimplContext
535 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
536 ctxtUnderImplic SimplRuleLhs = SimplCheck
537 ctxtUnderImplic ctxt         = ctxt
538
539 tryTcS :: TcS a -> TcS a 
540 -- Like runTcS, but from within the TcS monad 
541 -- Ignore all the evidence generated, and do not affect caller's evidence!
542 tryTcS tcs 
543   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
544                     ; ev_binds_var <- TcM.newTcEvBinds
545                     ; let env1 = env { tcs_ev_binds = ev_binds_var
546                                      , tcs_ty_binds = ty_binds_var }
547                     ; unTcS tcs env1 })
548
549 -- Update TcEvBinds 
550 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
551
552 getDynFlags :: TcS DynFlags
553 getDynFlags = wrapTcS TcM.getDOpts
554
555 getTcSContext :: TcS SimplContext
556 getTcSContext = TcS (return . tcs_context)
557
558 getTcEvBinds :: TcS EvBindsVar
559 getTcEvBinds = TcS (return . tcs_ev_binds) 
560
561 getUntouchables :: TcS Untouchables 
562 getUntouchables = TcS (return . tcs_untch)
563
564 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
565 getTcSTyBinds = TcS (return . tcs_ty_binds)
566
567 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
568 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
569
570
571 getTcEvBindsBag :: TcS EvBindMap
572 getTcEvBindsBag
573   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
574        ; wrapTcS $ TcM.readTcRef ev_ref }
575
576 setWantedCoBind :: CoVar -> Coercion -> TcS () 
577 setWantedCoBind cv co 
578   = setEvBind cv (EvCoercion co)
579      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
580
581 setDerivedCoBind :: CoVar -> Coercion -> TcS () 
582 setDerivedCoBind cv co 
583   = setEvBind cv (EvCoercion co)
584
585 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
586 -- Add a type binding
587 setWantedTyBind tv ty 
588   = do { ref <- getTcSTyBinds
589        ; wrapTcS $ 
590          do { ty_binds <- TcM.readTcRef ref
591             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
592
593 setIPBind :: EvVar -> EvTerm -> TcS () 
594 setIPBind = setEvBind 
595
596 setDictBind :: EvVar -> EvTerm -> TcS () 
597 setDictBind = setEvBind 
598
599 setEvBind :: EvVar -> EvTerm -> TcS () 
600 -- Internal
601 setEvBind ev rhs 
602   = do { tc_evbinds <- getTcEvBinds 
603        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
604
605 newTcEvBindsTcS :: TcS EvBindsVar
606 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
607
608 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
609 warnTcS loc warn_if doc 
610   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
611   | otherwise = return ()
612
613 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
614 getDefaultInfo 
615   = do { ctxt <- getTcSContext
616        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
617        ; return (ctxt, tys, flags) }
618
619 -- Just get some environments needed for instance looking up and matching
620 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
621
622 getInstEnvs :: TcS (InstEnv, InstEnv) 
623 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
624
625 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
626 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
627
628 getTopEnv :: TcS HscEnv 
629 getTopEnv = wrapTcS $ TcM.getTopEnv 
630
631 getGblEnv :: TcS TcGblEnv 
632 getGblEnv = wrapTcS $ TcM.getGblEnv 
633
634 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
635 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636
637 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
638 checkWellStagedDFun pred dfun_id loc 
639   = wrapTcS $ TcM.setCtLoc loc $ 
640     do { use_stage <- TcM.getStage
641        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
642   where
643     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
644     bind_lvl = TcM.topIdLvl dfun_id
645
646 pprEq :: TcType -> TcType -> SDoc
647 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
648
649 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
650 isTouchableMetaTyVar tv 
651   = do { untch <- getUntouchables
652        ; return $ isTouchableMetaTyVar_InRange untch tv } 
653
654 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool 
655 isTouchableMetaTyVar_InRange untch tv 
656   = case tcTyVarDetails tv of 
657       MetaTv TcsTv _ -> True    -- See Note [Touchable meta type variables] 
658       MetaTv {}      -> inTouchableRange untch tv 
659       _              -> False 
660
661
662 \end{code}
663
664
665 Note [Touchable meta type variables]
666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
667 Meta type variables allocated *by the constraint solver itself* are always
668 touchable.  Example: 
669    instance C a b => D [a] where...
670 if we use this instance declaration we "make up" a fresh meta type
671 variable for 'b', which we must later guess.  (Perhaps C has a
672 functional dependency.)  But since we aren't in the constraint *generator*
673 we can't allocate a Unique in the touchable range for this implication
674 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
675
676
677 \begin{code}
678 -- Flatten skolems
679 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
680
681 newFlattenSkolemTy :: TcType -> TcS TcType
682 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
683
684 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
685 newFlattenSkolemTyVar ty
686   = wrapTcS $ do { uniq <- TcM.newUnique
687                  ; let name = mkSysTvName uniq (fsLit "f")
688                  ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
689
690 -- Instantiations 
691 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
692
693 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
694 instDFunTypes mb_inst_tys 
695   = mapM inst_tv mb_inst_tys
696   where
697     inst_tv :: Either TyVar TcType -> TcS Type
698     inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
699     inst_tv (Right ty) = return ty 
700
701 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
702 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
703
704
705 -- newFlexiTcS :: TyVar -> TcS TcTyVar
706 -- -- Make a TcsTv meta tyvar; it is always touchable,
707 -- -- but we are supposed to guess its instantiation
708 -- -- See Note [Touchable meta type variables]
709 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
710
711 newFlexiTcS :: TyVar -> TcS TcTyVar 
712 -- Like TcM.instMetaTyVar but the variable that is created is always
713 -- touchable; we are supposed to guess its instantiation. 
714 -- See Note [Touchable meta type variables] 
715 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
716
717 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)  
718 -- Create new wanted CoVar that constrains the type to have the specified kind. 
719 newKindConstraint tv knd 
720   = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd 
721        ; let ty_k = mkTyVarTy tv_k
722        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
723        ; return (co_var, ty_k) }
724
725 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
726 newFlexiTcSHelper tvname tvkind
727   = wrapTcS $ 
728     do { uniq <- TcM.newUnique 
729        ; ref  <- TcM.newMutVar  Flexi 
730        ; let name = setNameUnique tvname uniq 
731              kind = tvkind 
732        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
733
734 -- Superclasses and recursive dictionaries 
735 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
736
737 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
738 newGivOrDerEvVar pty evtrm 
739   = do { ev <- wrapTcS $ TcM.newEvVar pty 
740        ; setEvBind ev evtrm 
741        ; return ev }
742
743 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
744 -- Note we create immutable variables for given or derived, since we
745 -- must bind them to TcEvBinds (because their evidence may involve 
746 -- superclasses). However we should be able to override existing
747 -- 'derived' evidence, even in TcEvBinds 
748 newGivOrDerCoVar ty1 ty2 co 
749   = do { cv <- newCoVar ty1 ty2
750        ; setEvBind cv (EvCoercion co) 
751        ; return cv } 
752
753 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
754 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
755
756
757 newCoVar :: TcType -> TcType -> TcS EvVar 
758 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
759
760 newIPVar :: IPName Name -> TcType -> TcS EvVar 
761 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
762
763 newDictVar :: Class -> [TcType] -> TcS EvVar 
764 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
765 \end{code} 
766
767
768 \begin{code} 
769 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool 
770 -- In a call (isGoodRecEv ev wv), we are considering solving wv 
771 -- using some term that involves ev, such as:
772 -- by setting           wv = ev
773 -- or                   wv = EvCast x |> ev
774 -- etc. 
775 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
776 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
777 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
778 --
779 -- Guarded means: more instance calls than superclass selections. We
780 -- compute this by chasing the evidence, adding +1 for every instance
781 -- call (constructor) and -1 for every superclass selection (destructor).
782 --
783 -- See Note [Superclasses and recursive dictionaries] in TcInteract
784 isGoodRecEv ev_var (WantedEvVar wv _)
785   = do { tc_evbinds <- getTcEvBindsBag 
786        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
787        ; return $ case mb of 
788                     Nothing -> True 
789                     Just min_guardedness -> min_guardedness > 0
790        }
791
792   where chase_ev_var :: EvBindMap   -- Evidence binds 
793                  -> EvVar           -- Target variable whose gravity we want to return
794                  -> Int             -- Current gravity 
795                  -> [EvVar]         -- Visited nodes
796                  -> EvVar           -- Current node 
797                  -> TcS (Maybe Int)
798         chase_ev_var assocs trg curr_grav visited orig
799             | trg == orig         = return $ Just curr_grav
800             | orig `elem` visited = return $ Nothing 
801             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
802             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
803
804 {-  No longer needed: evidence is in the EvBinds
805             | isTcTyVar orig && isMetaTyVar orig 
806             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
807                  ; case meta_details of 
808                      Flexi -> return Nothing 
809                      Indirect tyco -> chase_ev assocs trg curr_grav 
810                                              (orig:visited) (EvCoercion tyco)
811                            }
812 -}
813             | otherwise = return Nothing 
814
815         chase_ev assocs trg curr_grav visited (EvId v) 
816             = chase_ev_var assocs trg curr_grav visited v
817         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
818             = chase_ev_var assocs trg (curr_grav-1) visited d_id
819         chase_ev assocs trg curr_grav visited (EvCast v co)
820             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
821                  ; m2 <- chase_co assocs trg curr_grav visited co
822                  ; return (comb_chase_res Nothing [m1,m2]) } 
823
824         chase_ev assocs trg curr_grav visited (EvCoercion co)
825             = chase_co assocs trg curr_grav visited co
826         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars) 
827             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
828                  ; return (comb_chase_res Nothing chase_results) } 
829
830         chase_co assocs trg curr_grav visited co 
831             = -- Look for all the coercion variables in the coercion 
832               -- chase them, and combine the results. This is OK since the
833               -- coercion will not contain any superclass terms -- anything 
834               -- that involves dictionaries will be bound in assocs. 
835               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
836                                              (tyVarsOfType co)
837               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
838                     ; return (comb_chase_res Nothing chase_results) } 
839
840         comb_chase_res f []                   = f 
841         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest 
842         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
843         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest 
844
845
846 -- Matching and looking up classes and family instances
847 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
848
849 data MatchInstResult mi
850   = MatchInstNo         -- No matching instance 
851   | MatchInstSingle mi  -- Single matching instance
852   | MatchInstMany       -- Multiple matching instances
853
854
855 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
856 -- Look up a class constraint in the instance environment
857 matchClass clas tys
858   = do  { let pred = mkClassPred clas tys 
859         ; instEnvs <- getInstEnvs
860         ; case lookupInstEnv instEnvs clas tys of {
861             ([], unifs)               -- Nothing matches  
862                 -> do { traceTcS "matchClass not matching"
863                                  (vcat [ text "dict" <+> ppr pred, 
864                                          text "unifs" <+> ppr unifs ]) 
865                       ; return MatchInstNo  
866                       } ;  
867             ([(ispec, inst_tys)], []) -- A single match 
868                 -> do   { let dfun_id = is_dfun ispec
869                         ; traceTcS "matchClass success"
870                                    (vcat [text "dict" <+> ppr pred, 
871                                           text "witness" <+> ppr dfun_id
872                                            <+> ppr (idType dfun_id) ])
873                                   -- Record that this dfun is needed
874                         ; record_dfun_usage dfun_id
875                         ; return $ MatchInstSingle (dfun_id, inst_tys) 
876                         } ;
877             (matches, unifs)          -- More than one matches 
878                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
879                                    (vcat [text "dict" <+> ppr pred,
880                                           text "matches" <+> ppr matches,
881                                           text "unifs" <+> ppr unifs])
882                         ; return MatchInstMany 
883                         }
884         }
885         }
886   where record_dfun_usage :: Id -> TcS () 
887         record_dfun_usage dfun_id 
888           = do { hsc_env <- getTopEnv 
889                ; let  dfun_name = idName dfun_id
890                       dfun_mod  = ASSERT( isExternalName dfun_name ) 
891                                   nameModule dfun_name
892                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
893                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
894                  then return () -- internal, or in another package
895                  else do updInstUses dfun_id 
896                }
897
898         updInstUses :: Id -> TcS () 
899         updInstUses dfun_id 
900             = do { tcg_env <- getGblEnv 
901                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env) 
902                                             (`addOneToNameSet` idName dfun_id) 
903                  }
904
905 matchFam :: TyCon 
906          -> [Type] 
907          -> TcS (MatchInstResult (TyCon, [Type]))
908 matchFam tycon args
909   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
910        ; case mb of 
911            Nothing  -> return MatchInstNo 
912            Just res -> return $ MatchInstSingle res
913        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
914        -- multiple matches. Check. 
915        }
916
917
918 zonkTcTypeTcS :: TcType -> TcS TcType
919 -- Zonk through the TyBinds of the Tcs Monad
920 zonkTcTypeTcS ty 
921   = do { subst <- getTcSTyBindsMap >>= return . varEnvElts 
922        ; let (dom,rng)  = unzip subst 
923              apply_once = substTyWith dom rng 
924        ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
925        ; return (substTyWith dom rng_idemp ty) }
926
927                         
928
929
930
931
932 -- Functional dependencies, instantiation of equations
933 -------------------------------------------------------
934
935 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
936                    -> TcS [WantedEvVar] 
937 mkWantedFunDepEqns _   [] = return []
938 mkWantedFunDepEqns loc eqns
939   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
940        ; wevvars <- mapM to_work_item eqns
941        ; return $ concat wevvars }
942   where
943     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
944     to_work_item ((qtvs, pairs), _, _)
945       = do { let tvs = varSetElems qtvs
946            ; tvs' <- mapM newFlexiTcS tvs
947            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
948            ; mapM (do_one subst) pairs }
949
950     do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 
951                                        sty2 = substTy subst ty2 
952                                 ; ev <- newWantedCoVar sty1 sty2
953                                 ; return (WantedEvVar ev loc) }
954
955 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
956 pprEquationDoc (eqn, (p1, _), (p2, _)) 
957   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
958 \end{code}