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