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