Merge branch 'master' into type-nats
[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, isCTyEqCan, 
8     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
9     isCFrozenErr,
10
11     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
12     deCanonicalise, mkFrozenError,
13     makeSolvedByInst,
14
15     isWanted, isGiven, isDerived,
16     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
17
18     isFlexiTcsTv,
19
20     canRewrite, canSolve,
21     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
22     getWantedLoc,
23
24     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
25     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
27
28        -- Creation of evidence variables
29     newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
30     newDerivedId, 
31     newIPVar, newDictVar, newKindConstraint,
32
33        -- Setting evidence variables 
34     setWantedCoBind,
35     setIPBind, setDictBind, setEvBind,
36
37     setWantedTyBind,
38
39     getInstEnvs, getFamInstEnvs,                -- Getting the environments
40     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
41     tcsLookupClass, tcsLookupTyCon,
42     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
43
44     newFlattenSkolemTy,                         -- Flatten skolems 
45
46
47     instDFunTypes,                              -- Instantiation
48     instDFunConstraints,          
49     newFlexiTcSTy, 
50
51     compatKind,
52
53     TcsUntouchables,
54     isTouchableMetaTyVar,
55     isTouchableMetaTyVar_InRange, 
56
57     getDefaultInfo, getDynFlags,
58
59     matchClass, matchFam, MatchInstResult (..), 
60     checkWellStagedDFun, 
61     warnTcS,
62     pprEq,                                   -- Smaller utils, re-exported from TcM 
63                                              -- TODO (DV): these are only really used in the 
64                                              -- instance matcher in TcSimplify. I am wondering
65                                              -- if the whole instance matcher simply belongs
66                                              -- here 
67
68
69     mkDerivedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
70
71 ) where 
72
73 #include "HsVersions.h"
74
75 import HscTypes
76 import BasicTypes 
77
78 import Inst
79 import InstEnv 
80 import FamInst 
81 import FamInstEnv
82
83 import qualified TcRnMonad as TcM
84 import qualified TcMType as TcM
85 import qualified TcEnv as TcM 
86        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys
87        , tcLookupClass, tcLookupTyCon )
88 import TcType
89 import DynFlags
90
91 import Coercion
92 import Class
93 import TyCon
94 import TypeRep 
95
96 import Name
97 import Var
98 import VarEnv
99 import Outputable
100 import Bag
101 import MonadUtils
102 import VarSet
103 import FastString
104
105 import HsBinds               -- for TcEvBinds stuff 
106 import Id 
107 import FunDeps
108
109 import TcRnTypes
110
111 import Control.Monad
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        --   * typeKind xi `compatKind` typeKind tv
154        --       See Note [Spontaneous solving and kind compatibility]
155        --   * We prefer unification variables on the left *JUST* for efficiency
156       cc_id     :: EvVar, 
157       cc_flavor :: CtFlavor, 
158       cc_tyvar  :: TcTyVar, 
159       cc_rhs    :: Xi
160     }
161
162   | CFunEqCan {  -- F xis ~ xi  
163                  -- Invariant: * isSynFamilyTyCon cc_fun 
164                  --            * typeKind (F xis) `compatKind` typeKind xi
165       cc_id     :: EvVar,
166       cc_flavor :: CtFlavor, 
167       cc_fun    :: TyCon,       -- A type function
168       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
169       cc_rhs    :: Xi           --    *never* over-saturated (because if so
170                                 --    we should have decomposed)
171                    
172     }
173
174   | CFrozenErr {      -- A "frozen error" does not interact with anything
175                       -- See Note [Frozen Errors]
176       cc_id     :: EvVar,
177       cc_flavor :: CtFlavor
178     }
179
180 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
181 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
182
183 compatKind :: Kind -> Kind -> Bool
184 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
185
186 makeSolvedByInst :: CanonicalCt -> CanonicalCt
187 -- Record that a constraint is now solved
188 --        Wanted         -> Given
189 --        Given, Derived -> no-op
190 makeSolvedByInst ct 
191   | Wanted loc <- cc_flavor ct = ct { cc_flavor = mkGivenFlavor (Wanted loc) UnkSkol }
192   | otherwise                  = ct
193
194 deCanonicalise :: CanonicalCt -> FlavoredEvVar
195 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
196
197 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
198 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
199 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
200 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
201 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
202 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
203
204 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
205 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
206 tyVarsOfCDict _ct                            = emptyVarSet 
207
208 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
209 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
210
211 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
212 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
213
214 instance Outputable CanonicalCt where
215   ppr (CDictCan d fl cls tys)     
216       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
217   ppr (CIPCan ip fl ip_nm ty)     
218       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
219   ppr (CTyEqCan co fl tv ty)      
220       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
221   ppr (CFunEqCan co fl tc tys ty) 
222       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
223   ppr (CFrozenErr co fl)
224       = ppr fl <+> pprEvVarWithType co
225 \end{code}
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
257 isCTyEqCan :: CanonicalCt -> Bool 
258 isCTyEqCan (CTyEqCan {})  = True 
259 isCTyEqCan (CFunEqCan {}) = False
260 isCTyEqCan _              = False 
261
262 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
263 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
264 isCDictCan_Maybe _              = Nothing
265
266 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
267 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
268 isCIPCan_Maybe _                = Nothing
269
270 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
271 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
272 isCFunEqCan_Maybe _ = Nothing
273
274 isCFrozenErr :: CanonicalCt -> Bool
275 isCFrozenErr (CFrozenErr {}) = True
276 isCFrozenErr _               = False
277 \end{code}
278
279 %************************************************************************
280 %*                                                                      *
281                     CtFlavor
282          The "flavor" of a canonical constraint
283 %*                                                                      *
284 %************************************************************************
285
286 \begin{code}
287 getWantedLoc :: CanonicalCt -> WantedLoc
288 getWantedLoc ct 
289   = ASSERT (isWanted (cc_flavor ct))
290     case cc_flavor ct of 
291       Wanted wl -> wl 
292       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
293
294 isWantedCt :: CanonicalCt -> Bool
295 isWantedCt ct = isWanted (cc_flavor ct)
296 isGivenCt :: CanonicalCt -> Bool
297 isGivenCt ct = isGiven (cc_flavor ct)
298 isDerivedCt :: CanonicalCt -> Bool
299 isDerivedCt ct = isDerived (cc_flavor ct)
300
301 canSolve :: CtFlavor -> CtFlavor -> Bool 
302 -- canSolve ctid1 ctid2 
303 -- The constraint ctid1 can be used to solve ctid2 
304 -- "to solve" means a reaction where the active parts of the two constraints match.
305 --  active(F xis ~ xi) = F xis 
306 --  active(tv ~ xi)    = tv 
307 --  active(D xis)      = D xis 
308 --  active(IP nm ty)   = nm 
309 -----------------------------------------
310 canSolve (Given {})   _            = True 
311 canSolve (Derived {}) (Wanted {})  = False -- DV: changing the semantics
312 canSolve (Derived {}) (Derived {}) = True  -- DV: changing the semantics of derived 
313 canSolve (Wanted {})  (Wanted {})  = True
314 canSolve _ _ = False
315
316 canRewrite :: CtFlavor -> CtFlavor -> Bool 
317 -- canRewrite ctid1 ctid2 
318 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
319 canRewrite = canSolve 
320
321 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
322 -- Precondition: At least one of them should be wanted 
323 combineCtLoc (Wanted loc) _    = loc 
324 combineCtLoc _ (Wanted loc)    = loc 
325 combineCtLoc (Derived loc ) _  = loc 
326 combineCtLoc _ (Derived loc )  = loc 
327 combineCtLoc _ _ = panic "combineCtLoc: both given"
328
329 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
330 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
331 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
332 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
333
334 mkWantedFlavor :: CtFlavor -> CtFlavor
335 mkWantedFlavor (Wanted  loc) = Wanted loc
336 mkWantedFlavor (Derived loc) = Wanted loc
337 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
338 \end{code}
339
340 %************************************************************************
341 %*                                                                      *
342 %*              The TcS solver monad                                    *
343 %*                                                                      *
344 %************************************************************************
345
346 Note [The TcS monad]
347 ~~~~~~~~~~~~~~~~~~~~
348 The TcS monad is a weak form of the main Tc monad
349
350 All you can do is
351     * fail
352     * allocate new variables
353     * fill in evidence variables
354
355 Filling in a dictionary evidence variable means to create a binding
356 for it, so TcS carries a mutable location where the binding can be
357 added.  This is initialised from the innermost implication constraint.
358
359 \begin{code}
360 data TcSEnv
361   = TcSEnv { 
362       tcs_ev_binds :: EvBindsVar,
363           -- Evidence bindings
364
365       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
366           -- Global type bindings
367
368       tcs_context :: SimplContext,
369                      
370       tcs_untch :: TcsUntouchables
371     }
372
373 type TcsUntouchables = (Untouchables,TcTyVarSet)
374 -- Like the TcM Untouchables, 
375 -- but records extra TcsTv variables generated during simplification
376 -- See Note [Extra TcsTv untouchables] in TcSimplify
377 \end{code}
378
379 \begin{code}
380 data SimplContext
381   = SimplInfer          -- Inferring type of a let-bound thing
382   | SimplRuleLhs        -- Inferring type of a RULE lhs
383   | SimplInteractive    -- Inferring type at GHCi prompt
384   | SimplCheck          -- Checking a type signature or RULE rhs
385   deriving Eq
386
387 instance Outputable SimplContext where
388   ppr SimplInfer       = ptext (sLit "SimplInfer")
389   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
390   ppr SimplInteractive = ptext (sLit "SimplInteractive")
391   ppr SimplCheck       = ptext (sLit "SimplCheck")
392
393 isInteractive :: SimplContext -> Bool
394 isInteractive SimplInteractive = True
395 isInteractive _                = False
396
397 simplEqsOnly :: SimplContext -> Bool
398 -- Simplify equalities only, not dictionaries
399 -- This is used for the LHS of rules; ee
400 -- Note [Simplifying RULE lhs constraints] in TcSimplify
401 simplEqsOnly SimplRuleLhs = True
402 simplEqsOnly _            = False
403
404 performDefaulting :: SimplContext -> Bool
405 performDefaulting SimplInfer       = False
406 performDefaulting SimplRuleLhs     = False
407 performDefaulting SimplInteractive = True
408 performDefaulting SimplCheck       = True
409
410 ---------------
411 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
412
413 instance Functor TcS where
414   fmap f m = TcS $ fmap f . unTcS m
415
416 instance Monad TcS where 
417   return x  = TcS (\_ -> return x) 
418   fail err  = TcS (\_ -> fail err) 
419   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
420
421 -- Basic functionality 
422 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
423 wrapTcS :: TcM a -> TcS a 
424 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
425 -- and TcS is supposed to have limited functionality
426 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
427
428 wrapErrTcS :: TcM a -> TcS a 
429 -- The thing wrapped should just fail
430 -- There's no static check; it's up to the user
431 -- Having a variant for each error message is too painful
432 wrapErrTcS = wrapTcS
433
434 wrapWarnTcS :: TcM a -> TcS a 
435 -- The thing wrapped should just add a warning, or no-op
436 -- There's no static check; it's up to the user
437 wrapWarnTcS = wrapTcS
438
439 failTcS, panicTcS :: SDoc -> TcS a
440 failTcS      = wrapTcS . TcM.failWith
441 panicTcS doc = pprPanic "TcCanonical" doc
442
443 traceTcS :: String -> SDoc -> TcS ()
444 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
445
446 traceTcS0 :: String -> SDoc -> TcS ()
447 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
448
449 runTcS :: SimplContext
450        -> Untouchables         -- Untouchables
451        -> TcS a                -- What to run
452        -> TcM (a, Bag EvBind)
453 runTcS context untouch tcs 
454   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
455        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
456        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
457                           , tcs_ty_binds = ty_binds_var
458                           , tcs_context  = context
459                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
460                           }
461
462              -- Run the computation
463        ; res <- unTcS tcs env
464              -- Perform the type unifications required
465        ; ty_binds <- TcM.readTcRef ty_binds_var
466        ; mapM_ do_unification (varEnvElts ty_binds)
467
468              -- And return
469        ; ev_binds      <- TcM.readTcRef evb_ref
470        ; return (res, evBindMapBinds ev_binds) }
471   where
472     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
473
474 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
475 nestImplicTcS ref untch (TcS thing_inside)
476   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
477                      tcs_context = ctxt } ->
478     let 
479        nest_env = TcSEnv { tcs_ev_binds = ref
480                          , tcs_ty_binds = ty_binds
481                          , tcs_untch    = untch
482                          , tcs_context  = ctxtUnderImplic ctxt }
483     in 
484     thing_inside nest_env
485
486 recoverTcS :: TcS a -> TcS a -> TcS a
487 recoverTcS (TcS recovery_code) (TcS thing_inside)
488   = TcS $ \ env ->
489     TcM.recoverM (recovery_code env) (thing_inside env)
490
491 ctxtUnderImplic :: SimplContext -> SimplContext
492 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
493 ctxtUnderImplic SimplRuleLhs = SimplCheck
494 ctxtUnderImplic ctxt         = ctxt
495
496 tryTcS :: TcS a -> TcS a
497 -- Like runTcS, but from within the TcS monad 
498 -- Ignore all the evidence generated, and do not affect caller's evidence!
499 tryTcS tcs 
500   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
501                     ; ev_binds_var <- TcM.newTcEvBinds
502                     ; let env1 = env { tcs_ev_binds = ev_binds_var
503                                      , tcs_ty_binds = ty_binds_var }
504                     ; unTcS tcs env1 })
505
506 -- Update TcEvBinds 
507 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
508
509 getDynFlags :: TcS DynFlags
510 getDynFlags = wrapTcS TcM.getDOpts
511
512 getTcSContext :: TcS SimplContext
513 getTcSContext = TcS (return . tcs_context)
514
515 getTcEvBinds :: TcS EvBindsVar
516 getTcEvBinds = TcS (return . tcs_ev_binds) 
517
518 getUntouchables :: TcS TcsUntouchables
519 getUntouchables = TcS (return . tcs_untch)
520
521 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
522 getTcSTyBinds = TcS (return . tcs_ty_binds)
523
524 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
525 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
526
527
528 getTcEvBindsBag :: TcS EvBindMap
529 getTcEvBindsBag
530   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
531        ; wrapTcS $ TcM.readTcRef ev_ref }
532
533 setWantedCoBind :: CoVar -> Coercion -> TcS () 
534 setWantedCoBind cv co 
535   = setEvBind cv (EvCoercion co)
536      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
537
538 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
539 -- Add a type binding
540 -- We never do this twice!
541 setWantedTyBind tv ty 
542   = do { ref <- getTcSTyBinds
543        ; wrapTcS $ 
544          do { ty_binds <- TcM.readTcRef ref
545 #ifdef DEBUG
546             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
547               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
548                    , ppr tv <+> text ":=" <+> ppr ty
549                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
550 #endif
551             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
552
553 setIPBind :: EvVar -> EvTerm -> TcS () 
554 setIPBind = setEvBind 
555
556 setDictBind :: EvVar -> EvTerm -> TcS () 
557 setDictBind = setEvBind 
558
559 setEvBind :: EvVar -> EvTerm -> TcS () 
560 -- Internal
561 setEvBind ev rhs 
562   = do { tc_evbinds <- getTcEvBinds
563        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
564
565 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
566 warnTcS loc warn_if doc 
567   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
568   | otherwise = return ()
569
570 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
571 getDefaultInfo 
572   = do { ctxt <- getTcSContext
573        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
574        ; return (ctxt, tys, flags) }
575
576 -- Just get some environments needed for instance looking up and matching
577 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578
579 getInstEnvs :: TcS (InstEnv, InstEnv) 
580 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
581
582 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
583 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
584
585 getTopEnv :: TcS HscEnv 
586 getTopEnv = wrapTcS $ TcM.getTopEnv 
587
588 getGblEnv :: TcS TcGblEnv 
589 getGblEnv = wrapTcS $ TcM.getGblEnv 
590
591 tcsLookupClass :: Name -> TcS Class
592 tcsLookupClass name = wrapTcS (TcM.tcLookupClass name)
593
594 tcsLookupTyCon :: Name -> TcS TyCon
595 tcsLookupTyCon name = wrapTcS (TcM.tcLookupTyCon name)
596
597 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
598 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
599
600 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
601 checkWellStagedDFun pred dfun_id loc 
602   = wrapTcS $ TcM.setCtLoc loc $ 
603     do { use_stage <- TcM.getStage
604        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
605   where
606     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
607     bind_lvl = TcM.topIdLvl dfun_id
608
609 pprEq :: TcType -> TcType -> SDoc
610 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
611
612 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
613 isTouchableMetaTyVar tv 
614   = do { untch <- getUntouchables
615        ; return $ isTouchableMetaTyVar_InRange untch tv } 
616
617 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
618 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
619   = case tcTyVarDetails tv of 
620       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
621                         -- See Note [Touchable meta type variables] 
622       MetaTv {}      -> inTouchableRange untch tv 
623       _              -> False 
624
625
626 \end{code}
627
628
629 Note [Touchable meta type variables]
630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
631 Meta type variables allocated *by the constraint solver itself* are always
632 touchable.  Example: 
633    instance C a b => D [a] where...
634 if we use this instance declaration we "make up" a fresh meta type
635 variable for 'b', which we must later guess.  (Perhaps C has a
636 functional dependency.)  But since we aren't in the constraint *generator*
637 we can't allocate a Unique in the touchable range for this implication
638 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
639
640
641 \begin{code}
642 -- Flatten skolems
643 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
644
645 newFlattenSkolemTy :: TcType -> TcS TcType
646 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
647
648 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
649 newFlattenSkolemTyVar ty
650   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
651                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
652                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
653        ; traceTcS "New Flatten Skolem Born" $ 
654            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
655        ; return tv }
656
657 -- Instantiations 
658 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
659
660 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
661 instDFunTypes mb_inst_tys 
662   = mapM inst_tv mb_inst_tys
663   where
664     inst_tv :: Either TyVar TcType -> TcS Type
665     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
666     inst_tv (Right ty) = return ty 
667
668 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
669 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
670
671
672 instFlexiTcS :: TyVar -> TcS TcTyVar 
673 -- Like TcM.instMetaTyVar but the variable that is created is always
674 -- touchable; we are supposed to guess its instantiation. 
675 -- See Note [Touchable meta type variables] 
676 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
677
678 newFlexiTcSTy :: Kind -> TcS TcType  
679 newFlexiTcSTy knd 
680   = wrapTcS $
681     do { uniq <- TcM.newUnique 
682        ; ref  <- TcM.newMutVar  Flexi 
683        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
684        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
685
686 isFlexiTcsTv :: TyVar -> Bool
687 isFlexiTcsTv tv
688   | not (isTcTyVar tv)                  = False
689   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
690   | otherwise                           = False
691
692 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
693 -- Create new wanted CoVar that constrains the type to have the specified kind. 
694 newKindConstraint tv knd 
695   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
696        ; let ty_k = mkTyVarTy tv_k
697        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
698        ; return co_var }
699
700 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
701 instFlexiTcSHelper tvname tvkind
702   = wrapTcS $ 
703     do { uniq <- TcM.newUnique 
704        ; ref  <- TcM.newMutVar  Flexi 
705        ; let name = setNameUnique tvname uniq 
706              kind = tvkind 
707        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
708
709 -- Superclasses and recursive dictionaries 
710 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
711
712 newEvVar :: TcPredType -> TcS EvVar
713 newEvVar pty = wrapTcS $ TcM.newEvVar pty
714
715 newDerivedId :: TcPredType -> TcS EvVar 
716 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
717
718 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
719 -- Note we create immutable variables for given or derived, since we
720 -- must bind them to TcEvBinds (because their evidence may involve 
721 -- superclasses). However we should be able to override existing
722 -- 'derived' evidence, even in TcEvBinds 
723 newGivenCoVar ty1 ty2 co 
724   = do { cv <- newCoVar ty1 ty2
725        ; setEvBind cv (EvCoercion co) 
726        ; return cv } 
727
728 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
729 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
730
731 newCoVar :: TcType -> TcType -> TcS EvVar
732 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
733
734 newIPVar :: IPName Name -> TcType -> TcS EvVar 
735 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
736
737 newDictVar :: Class -> [TcType] -> TcS EvVar 
738 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
739 \end{code} 
740
741
742 \begin{code} 
743 -- Matching and looking up classes and family instances
744 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
745
746 data MatchInstResult mi
747   = MatchInstNo         -- No matching instance 
748   | MatchInstSingle mi  -- Single matching instance
749   | MatchInstMany       -- Multiple matching instances
750
751
752 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
753 -- Look up a class constraint in the instance environment
754 matchClass clas tys
755   = do  { let pred = mkClassPred clas tys 
756         ; instEnvs <- getInstEnvs
757         ; case lookupInstEnv instEnvs clas tys of {
758             ([], unifs)               -- Nothing matches  
759                 -> do { traceTcS "matchClass not matching"
760                                  (vcat [ text "dict" <+> ppr pred, 
761                                          text "unifs" <+> ppr unifs ]) 
762                       ; return MatchInstNo  
763                       } ;  
764             ([(ispec, inst_tys)], []) -- A single match 
765                 -> do   { let dfun_id = is_dfun ispec
766                         ; traceTcS "matchClass success"
767                                    (vcat [text "dict" <+> ppr pred, 
768                                           text "witness" <+> ppr dfun_id
769                                            <+> ppr (idType dfun_id) ])
770                                   -- Record that this dfun is needed
771                         ; return $ MatchInstSingle (dfun_id, inst_tys)
772                         } ;
773             (matches, unifs)          -- More than one matches 
774                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
775                                    (vcat [text "dict" <+> ppr pred,
776                                           text "matches" <+> ppr matches,
777                                           text "unifs" <+> ppr unifs])
778                         ; return MatchInstMany 
779                         }
780         }
781         }
782
783 matchFam :: TyCon
784          -> [Type] 
785          -> TcS (MatchInstResult (TyCon, [Type]))
786 matchFam tycon args
787   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
788        ; case mb of 
789            Nothing  -> return MatchInstNo 
790            Just res -> return $ MatchInstSingle res
791        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
792        -- multiple matches. Check. 
793        }
794
795
796 -- Functional dependencies, instantiation of equations
797 -------------------------------------------------------
798
799 mkDerivedFunDepEqns :: WantedLoc
800                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
801                    -> TcS [FlavoredEvVar]    -- All Derived
802 mkDerivedFunDepEqns _   [] = return []
803 mkDerivedFunDepEqns loc eqns
804   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
805        ; evvars <- mapM to_work_item eqns
806        ; return $ concat evvars }
807   where
808     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
809     to_work_item ((qtvs, pairs), d1, d2)
810       = do { let tvs = varSetElems qtvs
811            ; tvs' <- mapM instFlexiTcS tvs
812            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
813                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
814                  flav  = Derived loc'
815            ; mapM (do_one subst flav) pairs }
816
817     do_one subst flav (ty1, ty2)
818        = do { let sty1 = substTy subst ty1
819                   sty2 = substTy subst ty2
820             ; ev <- newCoVar sty1 sty2
821             ; return (mkEvVarX ev flav) }
822
823 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
824 pprEquationDoc (eqn, (p1, _), (p2, _)) 
825   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
826
827 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
828          -> TcM (TidyEnv, SDoc)
829 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
830   = do  { pred1' <- TcM.zonkTcPredType pred1
831         ; pred2' <- TcM.zonkTcPredType pred2
832         ; let { pred1'' = tidyPred tidy_env pred1'
833               ; pred2'' = tidyPred tidy_env pred2' }
834         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
835                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
836                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
837         ; return (tidy_env, msg) }
838 \end{code}