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