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