TcSMonad.lhs 29.3 KB
Newer Older
1
2
3
4
5
6
\begin{code}
-- Type definitions for the constraint solver
module TcSMonad ( 

       -- Canonical constraints
    CanonicalCts, emptyCCan, andCCan, andCCans, 
7
    singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, 
8
9
    isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
    isCFrozenErr,
10

11
12
13
14
    WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
    workListFromEq, workListFromNonEq,
    workListFromEqs, workListFromNonEqs, foldrWorkListM,

15
    CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
16
    deCanonicalise, mkFrozenError,
17

18
19
    isWanted, isGiven, isDerived,
    isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
20

21
22
    isFlexiTcsTv,

23
    canRewrite, canSolve,
24
25
    combineCtLoc, mkGivenFlavor, mkWantedFlavor,
    getWantedLoc,
26

27
28
    TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
    traceFireTcS, bumpStepCountTcS,
29
    tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
30
31
    SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,

32
       -- Creation of evidence variables
33
    newEvVar, newCoVar, newGivenCoVar,
34
    newDerivedId, 
35
36
37
    newIPVar, newDictVar, newKindConstraint,

       -- Setting evidence variables 
38
    setCoBind, setIPBind, setDictBind, setEvBind,
39
40
41

    setWantedTyBind,

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
54
    compatKind,

55
    TcsUntouchables,
56
    isTouchableMetaTyVar,
57
    isTouchableMetaTyVar_InRange, 
58
59
60
61
62
63

    getDefaultInfo, getDynFlags,

    matchClass, matchFam, MatchInstResult (..), 
    checkWellStagedDFun, 
    warnTcS,
64
    pprEq                                   -- Smaller utils, re-exported from TcM 
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
                                             -- TODO (DV): these are only really used in the 
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
                                             -- here 
) where 

#include "HsVersions.h"

import HscTypes
import BasicTypes 

import Inst
import InstEnv 
import FamInst 
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM 
       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
import TcType
import DynFlags

import Coercion
import Class
import TyCon
91
92
import TypeRep 

93
94
import Name
import Var
95
import VarEnv
96
97
98
99
100
101
102
103
import Outputable
import Bag
import MonadUtils
import VarSet
import FastString

import HsBinds               -- for TcEvBinds stuff 
import Id 
Ian Lynagh's avatar
Ian Lynagh committed
104
import TcRnTypes
105
106
import Data.IORef

107
#ifdef DEBUG
108
import StaticFlags( opt_PprStyle_Debug )
109
110
import Control.Monad( when )
#endif
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
\end{code}


%************************************************************************
%*									*
%*                       Canonical constraints                          *
%*                                                                      *
%*   These are the constraints the low-level simplifier works with      *
%*									*
%************************************************************************

\begin{code}
-- Types without any type functions inside.  However, note that xi
-- types CAN contain unexpanded type synonyms; however, the
-- (transitive) expansions of those type synonyms will not contain any
-- type functions.
type Xi = Type       -- In many comments, "xi" ranges over Xi

type CanonicalCts = Bag CanonicalCt
 
data CanonicalCt
  -- Atomic canonical constraints 
  = CDictCan {  -- e.g.  Num xi
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor, 
      cc_class  :: Class, 
      cc_tyargs :: [Xi]
    }

  | CIPCan {	-- ?x::tau
      -- See note [Canonical implicit parameter constraints].
      cc_id     :: EvVar,
143
      cc_flavor :: CtFlavor,
144
145
146
147
148
149
150
      cc_ip_nm  :: IPName Name,
      cc_ip_ty  :: TcTauType
    }

  | CTyEqCan {  -- tv ~ xi	(recall xi means function free)
       -- Invariant: 
       --   * tv not in tvs(xi)   (occurs check)
151
152
       --   * typeKind xi `compatKind` typeKind tv
       --       See Note [Spontaneous solving and kind compatibility]
153
       --   * We prefer unification variables on the left *JUST* for efficiency
154
155
      cc_id     :: EvVar, 
      cc_flavor :: CtFlavor, 
156
157
      cc_tyvar  :: TcTyVar, 
      cc_rhs    :: Xi
158
159
160
161
    }

  | CFunEqCan {  -- F xis ~ xi  
                 -- Invariant: * isSynFamilyTyCon cc_fun 
162
                 --            * typeKind (F xis) `compatKind` typeKind xi
163
164
165
166
167
168
169
170
171
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor, 
      cc_fun    :: TyCon,	-- A type function
      cc_tyargs :: [Xi],	-- Either under-saturated or exactly saturated
      cc_rhs    :: Xi      	--    *never* over-saturated (because if so
      		      		--    we should have decomposed)
                   
    }

172
173
174
175
176
  | CFrozenErr {      -- A "frozen error" does not interact with anything
                      -- See Note [Frozen Errors]
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor
    }
177

178
179
180
181
182
mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }

compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
183

184
185
deCanonicalise :: CanonicalCt -> FlavoredEvVar
deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
186
187
188
189
190

tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) 	       = tyVarsOfTypes tys
191
192
tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
193

194
195
196
197
198
199
200
tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCDict _ct                            = emptyVarSet 

tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet

201
202
203
204
205
206
207
208
209
210
211
212
tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet

instance Outputable CanonicalCt where
  ppr (CDictCan d fl cls tys)     
      = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
  ppr (CIPCan ip fl ip_nm ty)     
      = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
  ppr (CTyEqCan co fl tv ty)      
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
  ppr (CFunEqCan co fl tc tys ty) 
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
213
214
  ppr (CFrozenErr co fl)
      = ppr fl <+> pprEvVarWithType co
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
\end{code}

Note [Canonical implicit parameter constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type in a canonical implicit parameter constraint doesn't need to
be a xi (type-function-free type) since we can defer the flattening
until checking this type for equality with another type.  If we
encounter two IP constraints with the same name, they MUST have the
same type, and at that point we can generate a flattened equality
constraint between the types.  (On the other hand, the types in two
class constraints for the same class MAY be equal, so they need to be
flattened in the first place to facilitate comparing them.)

\begin{code}
singleCCan :: CanonicalCt -> CanonicalCts 
singleCCan = unitBag 

andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
andCCan = unionBags

extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
extendCCans = snocBag 

andCCans :: [CanonicalCts] -> CanonicalCts 
andCCans = unionManyBags

emptyCCan :: CanonicalCts 
emptyCCan = emptyBag

isEmptyCCan :: CanonicalCts -> Bool
isEmptyCCan = isEmptyBag
246

247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
isCTyEqCan :: CanonicalCt -> Bool 
isCTyEqCan (CTyEqCan {})  = True 
isCTyEqCan (CFunEqCan {}) = False
isCTyEqCan _              = False 

isCDictCan_Maybe :: CanonicalCt -> Maybe Class
isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
isCDictCan_Maybe _              = Nothing

isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
isCIPCan_Maybe _                = Nothing

isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
isCFunEqCan_Maybe _ = Nothing
263

264
265
266
isCFrozenErr :: CanonicalCt -> Bool
isCFrozenErr (CFrozenErr {}) = True
isCFrozenErr _               = False
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314


-- A mixture of Given, Wanted, and Derived constraints. 
-- We split between equalities and the rest to process equalities first. 
data WorkList = WorkList { weqs  :: CanonicalCts 
                                 -- NB: weqs includes equalities /and/ family equalities
                         , wrest :: CanonicalCts }

unionWorkList :: WorkList -> WorkList -> WorkList
unionWorkList wl1 wl2
  = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
             , wrest = wrest wl1 `andCCan` wrest wl2 }

unionWorkLists :: [WorkList] -> WorkList 
unionWorkLists = foldr unionWorkList emptyWorkList

isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)

emptyWorkList :: WorkList
emptyWorkList
  = WorkList { weqs = emptyBag, wrest = emptyBag }

workListFromEq :: CanonicalCt -> WorkList
workListFromEq = workListFromEqs . singleCCan

workListFromNonEq :: CanonicalCt -> WorkList
workListFromNonEq = workListFromNonEqs . singleCCan 

workListFromNonEqs :: CanonicalCts -> WorkList
workListFromNonEqs cts
  = WorkList { weqs = emptyCCan, wrest = cts }

workListFromEqs :: CanonicalCts -> WorkList
workListFromEqs cts
  = WorkList { weqs = cts, wrest = emptyCCan }

foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r) 
                           -> r -> WorkList -> m r
-- Prioritizes equalities
foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
  = do { r1 <- foldrBagM on_ct r eqs
       ; foldrBagM on_ct r1 rest }

instance Outputable WorkList where 
  ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
                , text "WorkList (Other)      = " <+> ppr (wrest wl) ]

315
316
\end{code}

317
318


319
320
321
322
323
324
325
326
%************************************************************************
%*									*
                    CtFlavor
         The "flavor" of a canonical constraint
%*									*
%************************************************************************

\begin{code}
327
328
329
330
331
332
333
getWantedLoc :: CanonicalCt -> WantedLoc
getWantedLoc ct 
  = ASSERT (isWanted (cc_flavor ct))
    case cc_flavor ct of 
      Wanted wl -> wl 
      _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty

334
isWantedCt :: CanonicalCt -> Bool
335
isWantedCt ct = isWanted (cc_flavor ct)
336
337
338
339
isGivenCt :: CanonicalCt -> Bool
isGivenCt ct = isGiven (cc_flavor ct)
isDerivedCt :: CanonicalCt -> Bool
isDerivedCt ct = isDerived (cc_flavor ct)
340

341
342
343
canSolve :: CtFlavor -> CtFlavor -> Bool 
-- canSolve ctid1 ctid2 
-- The constraint ctid1 can be used to solve ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
344
345
346
347
348
-- "to solve" means a reaction where the active parts of the two constraints match.
--  active(F xis ~ xi) = F xis 
--  active(tv ~ xi)    = tv 
--  active(D xis)      = D xis 
--  active(IP nm ty)   = nm 
349
350
--
-- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
351
-----------------------------------------
352
canSolve (Given {})   _            = True 
353
canSolve (Wanted {})  (Derived {}) = True
354
canSolve (Wanted {})  (Wanted {})  = True
355
356
canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
canSolve _ _ = False  	       	     	   -- (There is no *evidence* for a derived.)
357

358
359
canRewrite :: CtFlavor -> CtFlavor -> Bool 
-- canRewrite ctid1 ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
360
-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
361
canRewrite = canSolve 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
362

363
364
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted 
365
366
combineCtLoc (Wanted loc) _    = loc 
combineCtLoc _ (Wanted loc)    = loc 
367
368
combineCtLoc (Derived loc ) _  = loc 
combineCtLoc _ (Derived loc )  = loc 
369
combineCtLoc _ _ = panic "combineCtLoc: both given"
370
371

mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
372
373
374
375
mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Given   loc) sk  = Given (setCtLocOrigin loc sk)

376
377

mkWantedFlavor :: CtFlavor -> CtFlavor
378
379
380
mkWantedFlavor (Wanted  loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
\end{code}

%************************************************************************
%*									*
%*		The TcS solver monad                                    *
%*									*
%************************************************************************

Note [The TcS monad]
~~~~~~~~~~~~~~~~~~~~
The TcS monad is a weak form of the main Tc monad

All you can do is
    * fail
    * allocate new variables
    * fill in evidence variables

Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added.  This is initialised from the innermost implication constraint.

\begin{code}
data TcSEnv
  = TcSEnv { 
      tcs_ev_binds :: EvBindsVar,
          -- Evidence bindings

408
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
409
410
          -- Global type bindings

411
      tcs_context :: SimplContext,
412
                     
413
414
415
416
      tcs_untch :: TcsUntouchables,

      tcs_ic_depth :: Int,	-- Implication nesting depth
      tcs_count    :: IORef Int	-- Global step count
417
418
    }

419
420
421
422
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify
423
424
425
\end{code}

\begin{code}
426
data SimplContext
427
428
429
430
  = SimplInfer SDoc	   -- Inferring type of a let-bound thing
  | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
  | SimplInteractive	   -- Inferring type at GHCi prompt
  | SimplCheck SDoc	   -- Checking a type signature or RULE rhs
431
432

instance Outputable SimplContext where
433
434
435
  ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
  ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
  ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
436
437
438
439
440
441
442
443
444
445
  ppr SimplInteractive = ptext (sLit "SimplInteractive")

isInteractive :: SimplContext -> Bool
isInteractive SimplInteractive = True
isInteractive _                = False

simplEqsOnly :: SimplContext -> Bool
-- Simplify equalities only, not dictionaries
-- This is used for the LHS of rules; ee
-- Note [Simplifying RULE lhs constraints] in TcSimplify
446
447
simplEqsOnly (SimplRuleLhs {}) = True
simplEqsOnly _                 = False
448
449

performDefaulting :: SimplContext -> Bool
450
451
452
453
performDefaulting (SimplInfer {})   = False
performDefaulting (SimplRuleLhs {}) = False
performDefaulting SimplInteractive  = True
performDefaulting (SimplCheck {})   = True
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490

---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 

instance Functor TcS where
  fmap f m = TcS $ fmap f . unTcS m

instance Monad TcS where 
  return x  = TcS (\_ -> return x) 
  fail err  = TcS (\_ -> fail err) 
  m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)

-- Basic functionality 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wrapTcS :: TcM a -> TcS a 
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds

wrapErrTcS :: TcM a -> TcS a 
-- The thing wrapped should just fail
-- There's no static check; it's up to the user
-- Having a variant for each error message is too painful
wrapErrTcS = wrapTcS

wrapWarnTcS :: TcM a -> TcS a 
-- The thing wrapped should just add a warning, or no-op
-- There's no static check; it's up to the user
wrapWarnTcS = wrapTcS

failTcS, panicTcS :: SDoc -> TcS a
failTcS      = wrapTcS . TcM.failWith
panicTcS doc = pprPanic "TcCanonical" doc

traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

traceFireTcS :: Int -> SDoc -> TcS ()
-- Dump a rule-firing trace
traceFireTcS depth doc 
  = TcS $ \env -> 
    TcM.ifDOptM Opt_D_dump_cs_trace $ 
    do { n <- TcM.readTcRef (tcs_count env)
       ; let msg = int n 
                <> text (replicate (tcs_ic_depth env) '>')
                <> brackets (int depth) <+> doc
       ; 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
516
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
517
                          , tcs_context  = context
518
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
519
520
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
521
                          }
522
523

	     -- Run the computation
524
       ; res <- unTcS tcs env
525
526
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
527
       ; mapM_ do_unification (varEnvElts ty_binds)
528

529
530
#ifdef DEBUG
       ; count <- TcM.readTcRef step_count
531
       ; when (opt_PprStyle_Debug && count > 0) $
532
533
         TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
                            <+> int count <+> ppr context)
534
#endif
535
             -- And return
536
       ; ev_binds      <- TcM.readTcRef evb_ref
537
       ; return (res, evBindMapBinds ev_binds) }
538
539
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
540

541
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
542
543
544
545
546
547
nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds 
    	    	   , tcs_untch = (_outer_range, outer_tcs)
		   , tcs_count = count
		   , tcs_ic_depth = idepth
                   , tcs_context = ctxt } ->
548
    let 
549
550
551
552
553
       inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
       		   -- The inner_range should be narrower than the outer one
		   -- (thus increasing the set of untouchables) but 
		   -- the inner Tcs-untouchables must be unioned with the
		   -- outer ones!
554
555
       nest_env = TcSEnv { tcs_ev_binds = ref
                         , tcs_ty_binds = ty_binds
556
557
558
                         , tcs_untch    = inner_untch
                         , tcs_count    = count
                         , tcs_ic_depth = idepth+1
559
                         , tcs_context  = ctxtUnderImplic ctxt }
560
    in 
561
    thing_inside nest_env
562

563
564
565
566
567
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

568
569
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
570
571
572
ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 
                                               <+> doubleQuotes (ftext n))
ctxtUnderImplic ctxt              = ctxt
573

574
tryTcS :: TcS a -> TcS a
575
576
-- Like runTcS, but from within the TcS monad 
-- Ignore all the evidence generated, and do not affect caller's evidence!
577
tryTcS tcs 
578
  = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
579
580
                    ; ev_binds_var <- TcM.newTcEvBinds
                    ; let env1 = env { tcs_ev_binds = ev_binds_var
581
                                     , tcs_ty_binds = ty_binds_var }
582
                    ; unTcS tcs env1 })
583
584
585
586
587
588
589
590
591
592
593
594
595

-- Update TcEvBinds 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getDynFlags :: TcS DynFlags
getDynFlags = wrapTcS TcM.getDOpts

getTcSContext :: TcS SimplContext
getTcSContext = TcS (return . tcs_context)

getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds) 

596
getUntouchables :: TcS TcsUntouchables
597
598
getUntouchables = TcS (return . tcs_untch)

599
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
600
601
getTcSTyBinds = TcS (return . tcs_ty_binds)

602
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
603
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
604
605


606
607
608
609
610
getTcEvBindsBag :: TcS EvBindMap
getTcEvBindsBag
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

611
612
setCoBind :: CoVar -> Coercion -> TcS () 
setCoBind cv co = setEvBind cv (EvCoercion co)
613
614
615

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
616
-- We never do this twice!
617
618
619
620
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
621
622
623
624
625
626
#ifdef DEBUG
            ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
              vcat [ text "TERRIBLE ERROR: double set of meta type variable"
                   , ppr tv <+> text ":=" <+> ppr ty
                   , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
#endif
627
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
628
629
630
631
632
633
634
635
636
637

setIPBind :: EvVar -> EvTerm -> TcS () 
setIPBind = setEvBind 

setDictBind :: EvVar -> EvTerm -> TcS () 
setDictBind = setEvBind 

setEvBind :: EvVar -> EvTerm -> TcS () 
-- Internal
setEvBind ev rhs 
638
  = do { tc_evbinds <- getTcEvBinds
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
       ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }

warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
warnTcS loc warn_if doc 
  | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
  | otherwise = return ()

getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
getDefaultInfo 
  = do { ctxt <- getTcSContext
       ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
       ; return (ctxt, tys, flags) }

-- Just get some environments needed for instance looking up and matching
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getInstEnvs :: TcS (InstEnv, InstEnv) 
getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 

getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs

getTopEnv :: TcS HscEnv 
getTopEnv = wrapTcS $ TcM.getTopEnv 

getGblEnv :: TcS TcGblEnv 
getGblEnv = wrapTcS $ TcM.getGblEnv 

-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
checkWellStagedDFun pred dfun_id loc 
  = wrapTcS $ TcM.setCtLoc loc $ 
    do { use_stage <- TcM.getStage
       ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
  where
    pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
    bind_lvl = TcM.topIdLvl dfun_id

pprEq :: TcType -> TcType -> SDoc
pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)

isTouchableMetaTyVar :: TcTyVar -> TcS Bool
683
isTouchableMetaTyVar tv 
684
685
686
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

687
688
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
689
  = case tcTyVarDetails tv of 
690
691
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
692
693
694
695
      MetaTv {}      -> inTouchableRange untch tv 
      _              -> False 


696
697
\end{code}

698

699
700
701
702
703
704
705
706
707
708
Note [Touchable meta type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Meta type variables allocated *by the constraint solver itself* are always
touchable.  Example: 
   instance C a b => D [a] where...
if we use this instance declaration we "make up" a fresh meta type
variable for 'b', which we must later guess.  (Perhaps C has a
functional dependency.)  But since we aren't in the constraint *generator*
we can't allocate a Unique in the touchable range for this implication
constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
709
710


711
\begin{code}
712
713
714
715
716
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
717
718
719

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
720
  = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
721
                            ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
722
723
724
725
                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
       ; traceTcS "New Flatten Skolem Born" $ 
           (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
       ; return tv }
726
727
728
729
730

-- Instantiations 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
731
732
733
734
instDFunTypes mb_inst_tys 
  = mapM inst_tv mb_inst_tys
  where
    inst_tv :: Either TyVar TcType -> TcS Type
735
    inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
736
    inst_tv (Right ty) = return ty 
737
738
739
740

instDFunConstraints :: TcThetaType -> TcS [EvVar] 
instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 

741

742
instFlexiTcS :: TyVar -> TcS TcTyVar 
743
744
745
-- Like TcM.instMetaTyVar but the variable that is created is always
-- touchable; we are supposed to guess its instantiation. 
-- See Note [Touchable meta type variables] 
746
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
747

748
749
750
751
752
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
753
       ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
754
755
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

756
757
758
759
760
761
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

762
newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
763
764
-- Create new wanted CoVar that constrains the type to have the specified kind. 
newKindConstraint tv knd 
765
  = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
766
       ; let ty_k = mkTyVarTy tv_k
767
       ; co_var <- newCoVar (mkTyVarTy tv) ty_k
768
       ; return co_var }
769

770
771
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper tvname tvkind
772
773
774
775
776
777
  = wrapTcS $ 
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
       ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
778
779
780
781

-- Superclasses and recursive dictionaries 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

782
783
newEvVar :: TcPredType -> TcS EvVar
newEvVar pty = wrapTcS $ TcM.newEvVar pty
784

785
786
787
788
newDerivedId :: TcPredType -> TcS EvVar 
newDerivedId pty = wrapTcS $ TcM.newEvVar pty

newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
789
790
791
792
-- Note we create immutable variables for given or derived, since we
-- must bind them to TcEvBinds (because their evidence may involve 
-- superclasses). However we should be able to override existing
-- 'derived' evidence, even in TcEvBinds 
793
newGivenCoVar ty1 ty2 co 
794
795
796
797
  = do { cv <- newCoVar ty1 ty2
       ; setEvBind cv (EvCoercion co) 
       ; return cv } 

798
newCoVar :: TcType -> TcType -> TcS EvVar
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 

newIPVar :: IPName Name -> TcType -> TcS EvVar 
newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 

newDictVar :: Class -> [TcType] -> TcS EvVar 
newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
\end{code} 


\begin{code} 
-- Matching and looking up classes and family instances
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data MatchInstResult mi
  = MatchInstNo         -- No matching instance 
  | MatchInstSingle mi  -- Single matching instance
  | MatchInstMany       -- Multiple matching instances


matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
-- Look up a class constraint in the instance environment
matchClass clas tys
  = do	{ let pred = mkClassPred clas tys 
        ; instEnvs <- getInstEnvs
824
        ; case lookupInstEnv instEnvs clas tys of {
825
826
827
828
829
830
831
832
833
834
835
            ([], unifs)               -- Nothing matches  
                -> do { traceTcS "matchClass not matching"
                                 (vcat [ text "dict" <+> ppr pred, 
                                         text "unifs" <+> ppr unifs ]) 
                      ; return MatchInstNo  
                      } ;  
	    ([(ispec, inst_tys)], []) -- A single match 
		-> do	{ let dfun_id = is_dfun ispec
			; traceTcS "matchClass success"
				   (vcat [text "dict" <+> ppr pred, 
				          text "witness" <+> ppr dfun_id
836
                                           <+> ppr (idType dfun_id) ])
837
				  -- Record that this dfun is needed
838
                        ; return $ MatchInstSingle (dfun_id, inst_tys)
839
840
841
842
843
844
845
846
847
848
                        } ;
     	    (matches, unifs)          -- More than one matches 
		-> do	{ traceTcS "matchClass multiple matches, deferring choice"
			           (vcat [text "dict" <+> ppr pred,
				   	  text "matches" <+> ppr matches,
				   	  text "unifs" <+> ppr unifs])
                        ; return MatchInstMany 
		        }
	}
        }
849
850

matchFam :: TyCon
851
852
853
854
855
856
857
858
859
860
861
         -> [Type] 
         -> TcS (MatchInstResult (TyCon, [Type]))
matchFam tycon args
  = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
       ; case mb of 
           Nothing  -> return MatchInstNo 
           Just res -> return $ MatchInstSingle res
       -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
       -- multiple matches. Check. 
       }
\end{code}