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