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