Fix Trac #4401: meta-tyvars allocated by the constraint solver are always touchable
[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     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 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 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
301 -- Precondition: At least one of them should be wanted 
302 combineCtLoc (Wanted loc) _ = loc 
303 combineCtLoc _ (Wanted loc) = loc 
304 combineCtLoc (Derived loc) _ = loc 
305 combineCtLoc _ (Derived loc) = loc 
306 combineCtLoc _ _ = panic "combineCtLoc: both given"
307
308 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
309 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
310 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
311 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
312 \end{code}
313
314
315 %************************************************************************
316 %*                                                                      *
317 %*              The TcS solver monad                                    *
318 %*                                                                      *
319 %************************************************************************
320
321 Note [The TcS monad]
322 ~~~~~~~~~~~~~~~~~~~~
323 The TcS monad is a weak form of the main Tc monad
324
325 All you can do is
326     * fail
327     * allocate new variables
328     * fill in evidence variables
329
330 Filling in a dictionary evidence variable means to create a binding
331 for it, so TcS carries a mutable location where the binding can be
332 added.  This is initialised from the innermost implication constraint.
333
334 \begin{code}
335 data TcSEnv
336   = TcSEnv { 
337       tcs_ev_binds :: EvBindsVar,
338           -- Evidence bindings
339
340       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
341           -- Global type bindings
342
343       tcs_context :: SimplContext,
344
345       tcs_untch :: Untouchables
346     }
347
348 data SimplContext
349   = SimplInfer          -- Inferring type of a let-bound thing
350   | SimplRuleLhs        -- Inferring type of a RULE lhs
351   | SimplInteractive    -- Inferring type at GHCi prompt
352   | SimplCheck          -- Checking a type signature or RULE rhs
353
354 instance Outputable SimplContext where
355   ppr SimplInfer       = ptext (sLit "SimplInfer")
356   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
357   ppr SimplInteractive = ptext (sLit "SimplInteractive")
358   ppr SimplCheck       = ptext (sLit "SimplCheck")
359
360 isInteractive :: SimplContext -> Bool
361 isInteractive SimplInteractive = True
362 isInteractive _                = False
363
364 simplEqsOnly :: SimplContext -> Bool
365 -- Simplify equalities only, not dictionaries
366 -- This is used for the LHS of rules; ee
367 -- Note [Simplifying RULE lhs constraints] in TcSimplify
368 simplEqsOnly SimplRuleLhs = True
369 simplEqsOnly _            = False
370
371 performDefaulting :: SimplContext -> Bool
372 performDefaulting SimplInfer       = False
373 performDefaulting SimplRuleLhs     = False
374 performDefaulting SimplInteractive = True
375 performDefaulting SimplCheck       = True
376
377 ---------------
378 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
379
380 instance Functor TcS where
381   fmap f m = TcS $ fmap f . unTcS m
382
383 instance Monad TcS where 
384   return x  = TcS (\_ -> return x) 
385   fail err  = TcS (\_ -> fail err) 
386   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
387
388 -- Basic functionality 
389 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 wrapTcS :: TcM a -> TcS a 
391 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
392 -- and TcS is supposed to have limited functionality
393 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
394
395 wrapErrTcS :: TcM a -> TcS a 
396 -- The thing wrapped should just fail
397 -- There's no static check; it's up to the user
398 -- Having a variant for each error message is too painful
399 wrapErrTcS = wrapTcS
400
401 wrapWarnTcS :: TcM a -> TcS a 
402 -- The thing wrapped should just add a warning, or no-op
403 -- There's no static check; it's up to the user
404 wrapWarnTcS = wrapTcS
405
406 failTcS, panicTcS :: SDoc -> TcS a
407 failTcS      = wrapTcS . TcM.failWith
408 panicTcS doc = pprPanic "TcCanonical" doc
409
410 traceTcS :: String -> SDoc -> TcS ()
411 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
412
413 traceTcS0 :: String -> SDoc -> TcS ()
414 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
415
416 runTcS :: SimplContext
417        -> Untouchables         -- Untouchables
418        -> TcS a                -- What to run
419        -> TcM (a, Bag EvBind)
420 runTcS context untouch tcs 
421   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
422        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
423        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
424                           , tcs_ty_binds = ty_binds_var
425                           , tcs_context = context
426                           , tcs_untch   = untouch }
427
428              -- Run the computation
429        ; res <- unTcS tcs env
430
431              -- Perform the type unifications required
432        ; ty_binds <- TcM.readTcRef ty_binds_var
433        ; mapM_ do_unification (varEnvElts ty_binds)
434
435              -- And return
436        ; ev_binds <- TcM.readTcRef evb_ref
437        ; return (res, evBindMapBinds ev_binds) }
438   where
439     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
440
441        
442 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a 
443 nestImplicTcS ref untch (TcS thing_inside)
444   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> 
445     let 
446        nest_env = TcSEnv { tcs_ev_binds = ref
447                          , tcs_ty_binds = ty_binds
448                          , tcs_untch    = untch
449                          , tcs_context  = ctxtUnderImplic ctxt }
450     in 
451     thing_inside nest_env
452
453 ctxtUnderImplic :: SimplContext -> SimplContext
454 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
455 ctxtUnderImplic SimplRuleLhs = SimplCheck
456 ctxtUnderImplic ctxt         = ctxt
457
458 tryTcS :: TcS a -> TcS a 
459 -- Like runTcS, but from within the TcS monad 
460 -- Ignore all the evidence generated, and do not affect caller's evidence!
461 tryTcS tcs 
462   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
463                     ; ev_binds_var <- TcM.newTcEvBinds
464                     ; let env1 = env { tcs_ev_binds = ev_binds_var
465                                      , tcs_ty_binds = ty_binds_var }
466                     ; unTcS tcs env1 })
467
468 -- Update TcEvBinds 
469 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
470
471 getDynFlags :: TcS DynFlags
472 getDynFlags = wrapTcS TcM.getDOpts
473
474 getTcSContext :: TcS SimplContext
475 getTcSContext = TcS (return . tcs_context)
476
477 getTcEvBinds :: TcS EvBindsVar
478 getTcEvBinds = TcS (return . tcs_ev_binds) 
479
480 getUntouchables :: TcS Untouchables 
481 getUntouchables = TcS (return . tcs_untch)
482
483 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
484 getTcSTyBinds = TcS (return . tcs_ty_binds)
485
486 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
487 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
488
489
490 getTcEvBindsBag :: TcS EvBindMap
491 getTcEvBindsBag
492   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
493        ; wrapTcS $ TcM.readTcRef ev_ref }
494
495 setWantedCoBind :: CoVar -> Coercion -> TcS () 
496 setWantedCoBind cv co 
497   = setEvBind cv (EvCoercion co)
498      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
499
500 setDerivedCoBind :: CoVar -> Coercion -> TcS () 
501 setDerivedCoBind cv co 
502   = setEvBind cv (EvCoercion co)
503
504 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
505 -- Add a type binding
506 setWantedTyBind tv ty 
507   = do { ref <- getTcSTyBinds
508        ; wrapTcS $ 
509          do { ty_binds <- TcM.readTcRef ref
510             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
511
512 setIPBind :: EvVar -> EvTerm -> TcS () 
513 setIPBind = setEvBind 
514
515 setDictBind :: EvVar -> EvTerm -> TcS () 
516 setDictBind = setEvBind 
517
518 setEvBind :: EvVar -> EvTerm -> TcS () 
519 -- Internal
520 setEvBind ev rhs 
521   = do { tc_evbinds <- getTcEvBinds 
522        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
523
524 newTcEvBindsTcS :: TcS EvBindsVar
525 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
526
527 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
528 warnTcS loc warn_if doc 
529   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
530   | otherwise = return ()
531
532 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
533 getDefaultInfo 
534   = do { ctxt <- getTcSContext
535        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
536        ; return (ctxt, tys, flags) }
537
538 -- Just get some environments needed for instance looking up and matching
539 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
540
541 getInstEnvs :: TcS (InstEnv, InstEnv) 
542 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
543
544 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
545 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
546
547 getTopEnv :: TcS HscEnv 
548 getTopEnv = wrapTcS $ TcM.getTopEnv 
549
550 getGblEnv :: TcS TcGblEnv 
551 getGblEnv = wrapTcS $ TcM.getGblEnv 
552
553 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
554 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555
556 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
557 checkWellStagedDFun pred dfun_id loc 
558   = wrapTcS $ TcM.setCtLoc loc $ 
559     do { use_stage <- TcM.getStage
560        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
561   where
562     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
563     bind_lvl = TcM.topIdLvl dfun_id
564
565 pprEq :: TcType -> TcType -> SDoc
566 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
567
568 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
569 isTouchableMetaTyVar tv 
570   = case tcTyVarDetails tv of
571       MetaTv TcsTv _ -> return True     -- See Note [Touchable meta type variables]
572       MetaTv {}      -> do { untch <- getUntouchables
573                            ; return (inTouchableRange untch tv) }
574       _              -> return False
575 \end{code}
576
577 Note [Touchable meta type variables]
578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
579 Meta type variables allocated *by the constraint solver itself* are always
580 touchable.  Example: 
581    instance C a b => D [a] where...
582 if we use this instance declaration we "make up" a fresh meta type
583 variable for 'b', which we must later guess.  (Perhaps C has a
584 functional dependency.)  But since we aren't in the constraint *generator*
585 we can't allocate a Unique in the touchable range for this implication
586 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
587
588
589 \begin{code}
590 -- Flatten skolems
591 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
592
593 newFlattenSkolemTy :: TcType -> TcS TcType
594 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
595
596 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
597 newFlattenSkolemTyVar ty
598   = wrapTcS $ do { uniq <- TcM.newUnique
599                  ; let name = mkSysTvName uniq (fsLit "f")
600                  ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
601
602 -- Instantiations 
603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604
605 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
606 instDFunTypes mb_inst_tys 
607   = mapM inst_tv mb_inst_tys
608   where
609     inst_tv :: Either TyVar TcType -> TcS Type
610     inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
611     inst_tv (Right ty) = return ty 
612
613 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
614 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
615
616 newFlexiTcS :: TyVar -> TcS TcTyVar
617 -- Make a TcsTv meta tyvar; it is always touchable,
618 -- but we are supposed to guess its instantiation
619 -- See Note [Touchable meta type variables]
620 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
621
622 -- Superclasses and recursive dictionaries 
623 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
624
625 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
626 newGivOrDerEvVar pty evtrm 
627   = do { ev <- wrapTcS $ TcM.newEvVar pty 
628        ; setEvBind ev evtrm 
629        ; return ev }
630
631 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
632 -- Note we create immutable variables for given or derived, since we
633 -- must bind them to TcEvBinds (because their evidence may involve 
634 -- superclasses). However we should be able to override existing
635 -- 'derived' evidence, even in TcEvBinds 
636 newGivOrDerCoVar ty1 ty2 co 
637   = do { cv <- newCoVar ty1 ty2
638        ; setEvBind cv (EvCoercion co) 
639        ; return cv } 
640
641 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
642 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
643
644 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
645 newKindConstraint ty kind =  wrapTcS $ TcM.newKindConstraint ty kind
646
647 newCoVar :: TcType -> TcType -> TcS EvVar 
648 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
649
650 newIPVar :: IPName Name -> TcType -> TcS EvVar 
651 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
652
653 newDictVar :: Class -> [TcType] -> TcS EvVar 
654 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
655 \end{code} 
656
657
658 \begin{code} 
659 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool 
660 -- In a call (isGoodRecEv ev wv), we are considering solving wv 
661 -- using some term that involves ev, such as:
662 -- by setting           wv = ev
663 -- or                   wv = EvCast x |> ev
664 -- etc. 
665 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
666 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
667 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
668 --
669 -- Guarded means: more instance calls than superclass selections. We
670 -- compute this by chasing the evidence, adding +1 for every instance
671 -- call (constructor) and -1 for every superclass selection (destructor).
672 --
673 -- See Note [Superclasses and recursive dictionaries] in TcInteract
674 isGoodRecEv ev_var (WantedEvVar wv _)
675   = do { tc_evbinds <- getTcEvBindsBag 
676        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
677        ; return $ case mb of 
678                     Nothing -> True 
679                     Just min_guardedness -> min_guardedness > 0
680        }
681
682   where chase_ev_var :: EvBindMap   -- Evidence binds 
683                  -> EvVar           -- Target variable whose gravity we want to return
684                  -> Int             -- Current gravity 
685                  -> [EvVar]         -- Visited nodes
686                  -> EvVar           -- Current node 
687                  -> TcS (Maybe Int)
688         chase_ev_var assocs trg curr_grav visited orig
689             | trg == orig         = return $ Just curr_grav
690             | orig `elem` visited = return $ Nothing 
691             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
692             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
693
694 {-  No longer needed: evidence is in the EvBinds
695             | isTcTyVar orig && isMetaTyVar orig 
696             = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
697                  ; case meta_details of 
698                      Flexi -> return Nothing 
699                      Indirect tyco -> chase_ev assocs trg curr_grav 
700                                              (orig:visited) (EvCoercion tyco)
701                            }
702 -}
703             | otherwise = return Nothing 
704
705         chase_ev assocs trg curr_grav visited (EvId v) 
706             = chase_ev_var assocs trg curr_grav visited v
707         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
708             = chase_ev_var assocs trg (curr_grav-1) visited d_id
709         chase_ev assocs trg curr_grav visited (EvCast v co)
710             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
711                  ; m2 <- chase_co assocs trg curr_grav visited co
712                  ; return (comb_chase_res Nothing [m1,m2]) } 
713
714         chase_ev assocs trg curr_grav visited (EvCoercion co)
715             = chase_co assocs trg curr_grav visited co
716         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars) 
717             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
718                  ; return (comb_chase_res Nothing chase_results) } 
719
720         chase_co assocs trg curr_grav visited co 
721             = -- Look for all the coercion variables in the coercion 
722               -- chase them, and combine the results. This is OK since the
723               -- coercion will not contain any superclass terms -- anything 
724               -- that involves dictionaries will be bound in assocs. 
725               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
726                                              (tyVarsOfType co)
727               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
728                     ; return (comb_chase_res Nothing chase_results) } 
729
730         comb_chase_res f []                   = f 
731         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest 
732         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
733         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest 
734
735
736 -- Matching and looking up classes and family instances
737 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
738
739 data MatchInstResult mi
740   = MatchInstNo         -- No matching instance 
741   | MatchInstSingle mi  -- Single matching instance
742   | MatchInstMany       -- Multiple matching instances
743
744
745 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
746 -- Look up a class constraint in the instance environment
747 matchClass clas tys
748   = do  { let pred = mkClassPred clas tys 
749         ; instEnvs <- getInstEnvs
750         ; case lookupInstEnv instEnvs clas tys of {
751             ([], unifs)               -- Nothing matches  
752                 -> do { traceTcS "matchClass not matching"
753                                  (vcat [ text "dict" <+> ppr pred, 
754                                          text "unifs" <+> ppr unifs ]) 
755                       ; return MatchInstNo  
756                       } ;  
757             ([(ispec, inst_tys)], []) -- A single match 
758                 -> do   { let dfun_id = is_dfun ispec
759                         ; traceTcS "matchClass success"
760                                    (vcat [text "dict" <+> ppr pred, 
761                                           text "witness" <+> ppr dfun_id
762                                            <+> ppr (idType dfun_id) ])
763                                   -- Record that this dfun is needed
764                         ; record_dfun_usage dfun_id
765                         ; return $ MatchInstSingle (dfun_id, inst_tys) 
766                         } ;
767             (matches, unifs)          -- More than one matches 
768                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
769                                    (vcat [text "dict" <+> ppr pred,
770                                           text "matches" <+> ppr matches,
771                                           text "unifs" <+> ppr unifs])
772                         ; return MatchInstMany 
773                         }
774         }
775         }
776   where record_dfun_usage :: Id -> TcS () 
777         record_dfun_usage dfun_id 
778           = do { hsc_env <- getTopEnv 
779                ; let  dfun_name = idName dfun_id
780                       dfun_mod  = ASSERT( isExternalName dfun_name ) 
781                                   nameModule dfun_name
782                ; if isInternalName dfun_name ||    -- Internal name => defined in this module
783                     modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
784                  then return () -- internal, or in another package
785                  else do updInstUses dfun_id 
786                }
787
788         updInstUses :: Id -> TcS () 
789         updInstUses dfun_id 
790             = do { tcg_env <- getGblEnv 
791                  ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env) 
792                                             (`addOneToNameSet` idName dfun_id) 
793                  }
794
795 matchFam :: TyCon 
796          -> [Type] 
797          -> TcS (MatchInstResult (TyCon, [Type]))
798 matchFam tycon args
799   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
800        ; case mb of 
801            Nothing  -> return MatchInstNo 
802            Just res -> return $ MatchInstSingle res
803        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
804        -- multiple matches. Check. 
805        }
806
807
808 -- Functional dependencies, instantiation of equations
809 -------------------------------------------------------
810
811 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
812                    -> TcS [WantedEvVar] 
813 mkWantedFunDepEqns _   [] = return []
814 mkWantedFunDepEqns loc eqns
815   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
816        ; wevvars <- mapM to_work_item eqns
817        ; return $ concat wevvars }
818   where
819     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
820     to_work_item ((qtvs, pairs), _, _)
821       = do { let tvs = varSetElems qtvs
822            ; tvs' <- mapM newFlexiTcS tvs
823            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
824            ; mapM (do_one subst) pairs }
825
826     do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 
827                                        sty2 = substTy subst ty2 
828                                 ; ev <- newWantedCoVar sty1 sty2
829                                 ; return (WantedEvVar ev loc) }
830
831 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
832 pprEquationDoc (eqn, (p1, _), (p2, _)) 
833   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
834 \end{code}