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