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