makeSolvedByInst is only called on wanteds
[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     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
42
43     newFlattenSkolemTy,                         -- Flatten skolems 
44
45
46     instDFunTypes,                              -- Instantiation
47     instDFunConstraints,          
48     newFlexiTcSTy, 
49
50     compatKind,
51
52     TcsUntouchables,
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     mkDerivedFunDepEqns                       -- 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 qualified TcRnMonad as TcM
83 import qualified TcMType as TcM
84 import qualified TcEnv as TcM 
85        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
86 import TcType
87 import DynFlags
88
89 import Coercion
90 import Class
91 import TyCon
92 import TypeRep 
93
94 import Name
95 import Var
96 import VarEnv
97 import Outputable
98 import Bag
99 import MonadUtils
100 import VarSet
101 import FastString
102
103 import HsBinds               -- for TcEvBinds stuff 
104 import Id 
105 import FunDeps
106
107 import TcRnTypes
108
109 import Control.Monad
110 import Data.IORef
111 \end{code}
112
113
114 %************************************************************************
115 %*                                                                      *
116 %*                       Canonical constraints                          *
117 %*                                                                      *
118 %*   These are the constraints the low-level simplifier works with      *
119 %*                                                                      *
120 %************************************************************************
121
122 \begin{code}
123 -- Types without any type functions inside.  However, note that xi
124 -- types CAN contain unexpanded type synonyms; however, the
125 -- (transitive) expansions of those type synonyms will not contain any
126 -- type functions.
127 type Xi = Type       -- In many comments, "xi" ranges over Xi
128
129 type CanonicalCts = Bag CanonicalCt
130  
131 data CanonicalCt
132   -- Atomic canonical constraints 
133   = CDictCan {  -- e.g.  Num xi
134       cc_id     :: EvVar,
135       cc_flavor :: CtFlavor, 
136       cc_class  :: Class, 
137       cc_tyargs :: [Xi]
138     }
139
140   | CIPCan {    -- ?x::tau
141       -- See note [Canonical implicit parameter constraints].
142       cc_id     :: EvVar,
143       cc_flavor :: CtFlavor,
144       cc_ip_nm  :: IPName Name,
145       cc_ip_ty  :: TcTauType
146     }
147
148   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
149        -- Invariant: 
150        --   * tv not in tvs(xi)   (occurs check)
151        --   * typeKind xi `compatKind` typeKind tv
152        --       See Note [Spontaneous solving and kind compatibility]
153        --   * We prefer unification variables on the left *JUST* for efficiency
154       cc_id     :: EvVar, 
155       cc_flavor :: CtFlavor, 
156       cc_tyvar  :: TcTyVar, 
157       cc_rhs    :: Xi
158     }
159
160   | CFunEqCan {  -- F xis ~ xi  
161                  -- Invariant: * isSynFamilyTyCon cc_fun 
162                  --            * typeKind (F xis) `compatKind` typeKind xi
163       cc_id     :: EvVar,
164       cc_flavor :: CtFlavor, 
165       cc_fun    :: TyCon,       -- A type function
166       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
167       cc_rhs    :: Xi           --    *never* over-saturated (because if so
168                                 --    we should have decomposed)
169                    
170     }
171
172   | CFrozenErr {      -- A "frozen error" does not interact with anything
173                       -- See Note [Frozen Errors]
174       cc_id     :: EvVar,
175       cc_flavor :: CtFlavor
176     }
177
178 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
179 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
180
181 compatKind :: Kind -> Kind -> Bool
182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
183
184 makeSolvedByInst :: CanonicalCt -> CanonicalCt
185 -- Record that a constraint is now solved
186 --        Wanted         -> Given
187 --        Given, Derived -> no-op
188 makeSolvedByInst ct 
189   | Wanted loc <- cc_flavor ct
190   = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
191   | otherwise      -- Only called on wanteds
192   = pprPanic "makeSolvedByInst" (ppr 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 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
593
594 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
595 checkWellStagedDFun pred dfun_id loc 
596   = wrapTcS $ TcM.setCtLoc loc $ 
597     do { use_stage <- TcM.getStage
598        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
599   where
600     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
601     bind_lvl = TcM.topIdLvl dfun_id
602
603 pprEq :: TcType -> TcType -> SDoc
604 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
605
606 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
607 isTouchableMetaTyVar tv 
608   = do { untch <- getUntouchables
609        ; return $ isTouchableMetaTyVar_InRange untch tv } 
610
611 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
612 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
613   = case tcTyVarDetails tv of 
614       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
615                         -- See Note [Touchable meta type variables] 
616       MetaTv {}      -> inTouchableRange untch tv 
617       _              -> False 
618
619
620 \end{code}
621
622
623 Note [Touchable meta type variables]
624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
625 Meta type variables allocated *by the constraint solver itself* are always
626 touchable.  Example: 
627    instance C a b => D [a] where...
628 if we use this instance declaration we "make up" a fresh meta type
629 variable for 'b', which we must later guess.  (Perhaps C has a
630 functional dependency.)  But since we aren't in the constraint *generator*
631 we can't allocate a Unique in the touchable range for this implication
632 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
633
634
635 \begin{code}
636 -- Flatten skolems
637 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
638
639 newFlattenSkolemTy :: TcType -> TcS TcType
640 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
641
642 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
643 newFlattenSkolemTyVar ty
644   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
645                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
646                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
647        ; traceTcS "New Flatten Skolem Born" $ 
648            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
649        ; return tv }
650
651 -- Instantiations 
652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
653
654 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
655 instDFunTypes mb_inst_tys 
656   = mapM inst_tv mb_inst_tys
657   where
658     inst_tv :: Either TyVar TcType -> TcS Type
659     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
660     inst_tv (Right ty) = return ty 
661
662 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
663 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
664
665
666 instFlexiTcS :: TyVar -> TcS TcTyVar 
667 -- Like TcM.instMetaTyVar but the variable that is created is always
668 -- touchable; we are supposed to guess its instantiation. 
669 -- See Note [Touchable meta type variables] 
670 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
671
672 newFlexiTcSTy :: Kind -> TcS TcType  
673 newFlexiTcSTy knd 
674   = wrapTcS $
675     do { uniq <- TcM.newUnique 
676        ; ref  <- TcM.newMutVar  Flexi 
677        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
678        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
679
680 isFlexiTcsTv :: TyVar -> Bool
681 isFlexiTcsTv tv
682   | not (isTcTyVar tv)                  = False
683   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
684   | otherwise                           = False
685
686 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
687 -- Create new wanted CoVar that constrains the type to have the specified kind. 
688 newKindConstraint tv knd 
689   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
690        ; let ty_k = mkTyVarTy tv_k
691        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
692        ; return co_var }
693
694 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
695 instFlexiTcSHelper tvname tvkind
696   = wrapTcS $ 
697     do { uniq <- TcM.newUnique 
698        ; ref  <- TcM.newMutVar  Flexi 
699        ; let name = setNameUnique tvname uniq 
700              kind = tvkind 
701        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
702
703 -- Superclasses and recursive dictionaries 
704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
705
706 newEvVar :: TcPredType -> TcS EvVar
707 newEvVar pty = wrapTcS $ TcM.newEvVar pty
708
709 newDerivedId :: TcPredType -> TcS EvVar 
710 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
711
712 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
713 -- Note we create immutable variables for given or derived, since we
714 -- must bind them to TcEvBinds (because their evidence may involve 
715 -- superclasses). However we should be able to override existing
716 -- 'derived' evidence, even in TcEvBinds 
717 newGivenCoVar ty1 ty2 co 
718   = do { cv <- newCoVar ty1 ty2
719        ; setEvBind cv (EvCoercion co) 
720        ; return cv } 
721
722 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
723 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
724
725 newCoVar :: TcType -> TcType -> TcS EvVar
726 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
727
728 newIPVar :: IPName Name -> TcType -> TcS EvVar 
729 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
730
731 newDictVar :: Class -> [TcType] -> TcS EvVar 
732 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
733 \end{code} 
734
735
736 \begin{code} 
737 -- Matching and looking up classes and family instances
738 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
739
740 data MatchInstResult mi
741   = MatchInstNo         -- No matching instance 
742   | MatchInstSingle mi  -- Single matching instance
743   | MatchInstMany       -- Multiple matching instances
744
745
746 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
747 -- Look up a class constraint in the instance environment
748 matchClass clas tys
749   = do  { let pred = mkClassPred clas tys 
750         ; instEnvs <- getInstEnvs
751         ; case lookupInstEnv instEnvs clas tys of {
752             ([], unifs)               -- Nothing matches  
753                 -> do { traceTcS "matchClass not matching"
754                                  (vcat [ text "dict" <+> ppr pred, 
755                                          text "unifs" <+> ppr unifs ]) 
756                       ; return MatchInstNo  
757                       } ;  
758             ([(ispec, inst_tys)], []) -- A single match 
759                 -> do   { let dfun_id = is_dfun ispec
760                         ; traceTcS "matchClass success"
761                                    (vcat [text "dict" <+> ppr pred, 
762                                           text "witness" <+> ppr dfun_id
763                                            <+> ppr (idType dfun_id) ])
764                                   -- Record that this dfun is needed
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
777 matchFam :: TyCon
778          -> [Type] 
779          -> TcS (MatchInstResult (TyCon, [Type]))
780 matchFam tycon args
781   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
782        ; case mb of 
783            Nothing  -> return MatchInstNo 
784            Just res -> return $ MatchInstSingle res
785        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
786        -- multiple matches. Check. 
787        }
788
789
790 -- Functional dependencies, instantiation of equations
791 -------------------------------------------------------
792
793 mkDerivedFunDepEqns :: WantedLoc
794                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
795                    -> TcS [FlavoredEvVar]    -- All Derived
796 mkDerivedFunDepEqns _   [] = return []
797 mkDerivedFunDepEqns loc eqns
798   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
799        ; evvars <- mapM to_work_item eqns
800        ; return $ concat evvars }
801   where
802     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
803     to_work_item ((qtvs, pairs), d1, d2)
804       = do { let tvs = varSetElems qtvs
805            ; tvs' <- mapM instFlexiTcS tvs
806            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
807                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
808                  flav  = Derived loc'
809            ; mapM (do_one subst flav) pairs }
810
811     do_one subst flav (ty1, ty2)
812        = do { let sty1 = substTy subst ty1
813                   sty2 = substTy subst ty2
814             ; ev <- newCoVar sty1 sty2
815             ; return (mkEvVarX ev flav) }
816
817 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
818 pprEquationDoc (eqn, (p1, _), (p2, _)) 
819   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
820
821 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
822          -> TcM (TidyEnv, SDoc)
823 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
824   = do  { pred1' <- TcM.zonkTcPredType pred1
825         ; pred2' <- TcM.zonkTcPredType pred2
826         ; let { pred1'' = tidyPred tidy_env pred1'
827               ; pred2'' = tidyPred tidy_env pred2' }
828         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
829                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
830                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
831         ; return (tidy_env, msg) }
832 \end{code}