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