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