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