8d5093da840ffc726ae86bb4a1f676edd575a6cd
[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 Data.IORef
110 \end{code}
111
112
113 %************************************************************************
114 %*                                                                      *
115 %*                       Canonical constraints                          *
116 %*                                                                      *
117 %*   These are the constraints the low-level simplifier works with      *
118 %*                                                                      *
119 %************************************************************************
120
121 \begin{code}
122 -- Types without any type functions inside.  However, note that xi
123 -- types CAN contain unexpanded type synonyms; however, the
124 -- (transitive) expansions of those type synonyms will not contain any
125 -- type functions.
126 type Xi = Type       -- In many comments, "xi" ranges over Xi
127
128 type CanonicalCts = Bag CanonicalCt
129  
130 data CanonicalCt
131   -- Atomic canonical constraints 
132   = CDictCan {  -- e.g.  Num xi
133       cc_id     :: EvVar,
134       cc_flavor :: CtFlavor, 
135       cc_class  :: Class, 
136       cc_tyargs :: [Xi]
137     }
138
139   | CIPCan {    -- ?x::tau
140       -- See note [Canonical implicit parameter constraints].
141       cc_id     :: EvVar,
142       cc_flavor :: CtFlavor,
143       cc_ip_nm  :: IPName Name,
144       cc_ip_ty  :: TcTauType
145     }
146
147   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
148        -- Invariant: 
149        --   * tv not in tvs(xi)   (occurs check)
150        --   * typeKind xi `compatKind` typeKind tv
151        --       See Note [Spontaneous solving and kind compatibility]
152        --   * We prefer unification variables on the left *JUST* for efficiency
153       cc_id     :: EvVar, 
154       cc_flavor :: CtFlavor, 
155       cc_tyvar  :: TcTyVar, 
156       cc_rhs    :: Xi
157     }
158
159   | CFunEqCan {  -- F xis ~ xi  
160                  -- Invariant: * isSynFamilyTyCon cc_fun 
161                  --            * typeKind (F xis) `compatKind` typeKind xi
162       cc_id     :: EvVar,
163       cc_flavor :: CtFlavor, 
164       cc_fun    :: TyCon,       -- A type function
165       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
166       cc_rhs    :: Xi           --    *never* over-saturated (because if so
167                                 --    we should have decomposed)
168                    
169     }
170
171   | CFrozenErr {      -- A "frozen error" does not interact with anything
172                       -- See Note [Frozen Errors]
173       cc_id     :: EvVar,
174       cc_flavor :: CtFlavor
175     }
176
177 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
178 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
179
180 compatKind :: Kind -> Kind -> Bool
181 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
182
183 makeSolvedByInst :: CanonicalCt -> CanonicalCt
184 -- Record that a constraint is now solved
185 --        Wanted         -> Given
186 --        Given, Derived -> no-op
187 makeSolvedByInst ct 
188   | Wanted loc <- cc_flavor ct
189   = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
190   | otherwise      -- Only called on wanteds
191   = pprPanic "makeSolvedByInst" (ppr ct)
192
193 deCanonicalise :: CanonicalCt -> FlavoredEvVar
194 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
195
196 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
197 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
198 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
199 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
200 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
201 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
202
203 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
204 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
205 tyVarsOfCDict _ct                            = emptyVarSet 
206
207 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
208 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
209
210 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
211 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
212
213 instance Outputable CanonicalCt where
214   ppr (CDictCan d fl cls tys)     
215       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
216   ppr (CIPCan ip fl ip_nm ty)     
217       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
218   ppr (CTyEqCan co fl tv ty)      
219       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
220   ppr (CFunEqCan co fl tc tys ty) 
221       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
222   ppr (CFrozenErr co fl)
223       = ppr fl <+> pprEvVarWithType co
224 \end{code}
225
226 Note [Canonical implicit parameter constraints]
227 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
228 The type in a canonical implicit parameter constraint doesn't need to
229 be a xi (type-function-free type) since we can defer the flattening
230 until checking this type for equality with another type.  If we
231 encounter two IP constraints with the same name, they MUST have the
232 same type, and at that point we can generate a flattened equality
233 constraint between the types.  (On the other hand, the types in two
234 class constraints for the same class MAY be equal, so they need to be
235 flattened in the first place to facilitate comparing them.)
236
237 \begin{code}
238 singleCCan :: CanonicalCt -> CanonicalCts 
239 singleCCan = unitBag 
240
241 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
242 andCCan = unionBags
243
244 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
245 extendCCans = snocBag 
246
247 andCCans :: [CanonicalCts] -> CanonicalCts 
248 andCCans = unionManyBags
249
250 emptyCCan :: CanonicalCts 
251 emptyCCan = emptyBag
252
253 isEmptyCCan :: CanonicalCts -> Bool
254 isEmptyCCan = isEmptyBag
255
256 isCTyEqCan :: CanonicalCt -> Bool 
257 isCTyEqCan (CTyEqCan {})  = True 
258 isCTyEqCan (CFunEqCan {}) = False
259 isCTyEqCan _              = False 
260
261 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
262 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
263 isCDictCan_Maybe _              = Nothing
264
265 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
266 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
267 isCIPCan_Maybe _                = Nothing
268
269 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
270 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
271 isCFunEqCan_Maybe _ = Nothing
272
273 isCFrozenErr :: CanonicalCt -> Bool
274 isCFrozenErr (CFrozenErr {}) = True
275 isCFrozenErr _               = False
276 \end{code}
277
278 %************************************************************************
279 %*                                                                      *
280                     CtFlavor
281          The "flavor" of a canonical constraint
282 %*                                                                      *
283 %************************************************************************
284
285 \begin{code}
286 getWantedLoc :: CanonicalCt -> WantedLoc
287 getWantedLoc ct 
288   = ASSERT (isWanted (cc_flavor ct))
289     case cc_flavor ct of 
290       Wanted wl -> wl 
291       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
292
293 isWantedCt :: CanonicalCt -> Bool
294 isWantedCt ct = isWanted (cc_flavor ct)
295 isGivenCt :: CanonicalCt -> Bool
296 isGivenCt ct = isGiven (cc_flavor ct)
297 isDerivedCt :: CanonicalCt -> Bool
298 isDerivedCt ct = isDerived (cc_flavor ct)
299
300 canSolve :: CtFlavor -> CtFlavor -> Bool 
301 -- canSolve ctid1 ctid2 
302 -- The constraint ctid1 can be used to solve ctid2 
303 -- "to solve" means a reaction where the active parts of the two constraints match.
304 --  active(F xis ~ xi) = F xis 
305 --  active(tv ~ xi)    = tv 
306 --  active(D xis)      = D xis 
307 --  active(IP nm ty)   = nm 
308 -----------------------------------------
309 canSolve (Given {})   _            = True 
310 canSolve (Derived {}) (Wanted {})  = False -- DV: changing the semantics
311 canSolve (Derived {}) (Derived {}) = True  -- DV: changing the semantics of derived 
312 canSolve (Wanted {})  (Wanted {})  = True
313 canSolve _ _ = False
314
315 canRewrite :: CtFlavor -> CtFlavor -> Bool 
316 -- canRewrite ctid1 ctid2 
317 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
318 canRewrite = canSolve 
319
320 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
321 -- Precondition: At least one of them should be wanted 
322 combineCtLoc (Wanted loc) _    = loc 
323 combineCtLoc _ (Wanted loc)    = loc 
324 combineCtLoc (Derived loc ) _  = loc 
325 combineCtLoc _ (Derived loc )  = loc 
326 combineCtLoc _ _ = panic "combineCtLoc: both given"
327
328 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
329 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk)
330 mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk)
331 mkGivenFlavor (Given   loc) sk  = Given (setCtLocOrigin loc sk)
332
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}