TcSMonad.lhs 33.6 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
    isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
batterseapower's avatar
batterseapower committed
9
    isCIrredEvCan, 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

dimitris's avatar
dimitris committed
18
19
20
    isWanted, isGivenOrSolved, isDerived,
    isGivenOrSolvedCt, isGivenCt_maybe, 
    isWantedCt, isDerivedCt, pprFlavorArising,
21

22
23
    isFlexiTcsTv,

24
    canRewrite, canSolve,
dimitris's avatar
dimitris committed
25
26
    combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
    mkWantedFlavor,
27
    getWantedLoc,
28

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

34
       -- Creation of evidence variables
batterseapower's avatar
batterseapower committed
35
36
37
    newEvVar,
    newDerivedId, newGivenEqVar,
    newEqVar, newIPVar, newDictVar, newKindConstraint,
38
39

       -- Setting evidence variables 
batterseapower's avatar
batterseapower committed
40
41
42
43
    setEqBind,
    setIPBind,
    setDictBind,
    setEvBind,
44
45
46

    setWantedTyBind,

dimitris's avatar
dimitris committed
47
48
    lookupFlatCacheMap, updateFlatCacheMap,

49
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
50
    getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
51
    getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
52
53

    newFlattenSkolemTy,                         -- Flatten skolems 
54

55
56

    instDFunTypes,                              -- Instantiation
57
    instDFunConstraints,          
58
    newFlexiTcSTy, instFlexiTcS,
59

60
61
    compatKind,

62
    TcsUntouchables,
63
    isTouchableMetaTyVar,
64
    isTouchableMetaTyVar_InRange, 
65
66
67
68
69
70

    getDefaultInfo, getDynFlags,

    matchClass, matchFam, MatchInstResult (..), 
    checkWellStagedDFun, 
    warnTcS,
71
    pprEq                                   -- Smaller utils, re-exported from TcM 
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 
91
       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
92
import Kind
93
94
95
96
97
98
import TcType
import DynFlags

import Coercion
import Class
import TyCon
99
100
import TypeRep 

101
102
import Name
import Var
103
import VarEnv
104
105
106
107
import Outputable
import Bag
import MonadUtils
import VarSet
108
import Pair
109
110
111
112
import FastString

import HsBinds               -- for TcEvBinds stuff 
import Id 
Ian Lynagh's avatar
Ian Lynagh committed
113
import TcRnTypes
114
115
import Data.IORef

dimitris's avatar
dimitris committed
116
117
import qualified Data.Map as Map

118
#ifdef DEBUG
119
import StaticFlags( opt_PprStyle_Debug )
120
121
import Control.Monad( when )
#endif
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
\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,
154
      cc_flavor :: CtFlavor,
155
156
157
158
      cc_ip_nm  :: IPName Name,
      cc_ip_ty  :: TcTauType
    }

batterseapower's avatar
batterseapower committed
159
160
161
162
163
164
  | CIrredEvCan {
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor,
      cc_ty     :: Xi
    }

165
166
167
  | CTyEqCan {  -- tv ~ xi	(recall xi means function free)
       -- Invariant: 
       --   * tv not in tvs(xi)   (occurs check)
168
169
       --   * typeKind xi `compatKind` typeKind tv
       --       See Note [Spontaneous solving and kind compatibility]
170
       --   * We prefer unification variables on the left *JUST* for efficiency
171
172
      cc_id     :: EvVar, 
      cc_flavor :: CtFlavor, 
173
174
      cc_tyvar  :: TcTyVar, 
      cc_rhs    :: Xi
175
176
177
178
    }

  | CFunEqCan {  -- F xis ~ xi  
                 -- Invariant: * isSynFamilyTyCon cc_fun 
179
                 --            * typeKind (F xis) `compatKind` typeKind xi
180
181
182
183
184
185
186
187
188
      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)
                   
    }

189
190
191
192
193
  | CFrozenErr {      -- A "frozen error" does not interact with anything
                      -- See Note [Frozen Errors]
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor
    }
194

195
196
197
198
199
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 
200

201
202
deCanonicalise :: CanonicalCt -> FlavoredEvVar
deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
203
204
205
206
207

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
208
tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
batterseapower's avatar
batterseapower committed
209
tyVarsOfCanonical (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
210
tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
211

212
213
214
215
216
217
218
tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCDict _ct                            = emptyVarSet 

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

219
220
221
222
223
224
225
226
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)
batterseapower's avatar
batterseapower committed
227
228
  ppr (CIrredEvCan v fl ty)
      = ppr fl <+> ppr v <+> dcolon <+> ppr ty
229
  ppr (CTyEqCan co fl tv ty)      
230
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
231
  ppr (CFunEqCan co fl tc tys ty) 
232
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
233
234
  ppr (CFrozenErr co fl)
      = ppr fl <+> pprEvVarWithType co
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
\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
266

267
268
269
270
271
272
273
274
275
276
277
278
279
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

batterseapower's avatar
batterseapower committed
280
281
282
283
isCIrredEvCan :: CanonicalCt -> Bool
isCIrredEvCan (CIrredEvCan {}) = True
isCIrredEvCan _                = False

284
285
286
isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
isCFunEqCan_Maybe _ = Nothing
287

288
289
290
isCFrozenErr :: CanonicalCt -> Bool
isCFrozenErr (CFrozenErr {}) = True
isCFrozenErr _               = False
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338


-- 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) ]

339
340
\end{code}

341
342


343
344
345
346
347
348
349
350
%************************************************************************
%*									*
                    CtFlavor
         The "flavor" of a canonical constraint
%*									*
%************************************************************************

\begin{code}
351
352
353
354
355
356
357
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

358
isWantedCt :: CanonicalCt -> Bool
359
isWantedCt ct = isWanted (cc_flavor ct)
360
361
isDerivedCt :: CanonicalCt -> Bool
isDerivedCt ct = isDerived (cc_flavor ct)
362

dimitris's avatar
dimitris committed
363
364
365
366
367
368
369
isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)

isGivenOrSolvedCt :: CanonicalCt -> Bool
isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)


370
371
372
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
373
374
375
376
377
-- "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 
378
379
--
-- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
380
-----------------------------------------
381
canSolve (Given {})   _            = True 
382
canSolve (Wanted {})  (Derived {}) = True
383
canSolve (Wanted {})  (Wanted {})  = True
384
385
canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
canSolve _ _ = False  	       	     	   -- (There is no *evidence* for a derived.)
386

387
388
canRewrite :: CtFlavor -> CtFlavor -> Bool 
-- canRewrite ctid1 ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
389
-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
390
canRewrite = canSolve 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
391

392
393
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted 
dimitris's avatar
dimitris committed
394
395
396
397
combineCtLoc (Wanted loc) _    = loc
combineCtLoc _ (Wanted loc)    = loc
combineCtLoc (Derived loc ) _  = loc
combineCtLoc _ (Derived loc )  = loc
398
combineCtLoc _ _ = panic "combineCtLoc: both given"
399

dimitris's avatar
dimitris committed
400
401
402
403
404
mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
mkSolvedFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
mkSolvedFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
405

dimitris's avatar
dimitris committed
406
407
408
409
mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
410
411

mkWantedFlavor :: CtFlavor -> CtFlavor
412
413
mkWantedFlavor (Wanted  loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
dimitris's avatar
dimitris committed
414
mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
\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

442
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
443
444
          -- Global type bindings

445
      tcs_context :: SimplContext,
446
                     
447
448
      tcs_untch :: TcsUntouchables,

dimitris's avatar
dimitris committed
449
450
451
452
      tcs_ic_depth   :: Int,       -- Implication nesting depth
      tcs_count      :: IORef Int, -- Global step count

      tcs_flat_map   :: IORef FlatCache
453
454
    }

dimitris's avatar
dimitris committed
455
data FlatCache 
batterseapower's avatar
batterseapower committed
456
  = FlatCache { givenFlatCache  :: Map.Map FunEqHead (TcType,EqVar,CtFlavor)
dimitris's avatar
dimitris committed
457
                -- Invariant: all CtFlavors here satisfy isGiven
batterseapower's avatar
batterseapower committed
458
              , wantedFlatCache :: Map.Map FunEqHead (TcType,EqVar,CtFlavor) }
dimitris's avatar
dimitris committed
459
460
461
462
463
464
465
466
467
                -- Invariant: all CtFlavors here satisfy isWanted

emptyFlatCache :: FlatCache
emptyFlatCache 
 = FlatCache { givenFlatCache  = Map.empty, wantedFlatCache = Map.empty }

newtype FunEqHead = FunEqHead (TyCon,[Xi])

instance Eq FunEqHead where
dimitris's avatar
dimitris committed
468
  FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2
dimitris's avatar
dimitris committed
469
470
471
472

instance Ord FunEqHead where
  FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2) 
    = case compare tc1 tc2 of 
dimitris's avatar
dimitris committed
473
        EQ    -> cmpTypes xis1 xis2
dimitris's avatar
dimitris committed
474
475
        other -> other

476
477
478
479
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify
480
481
482
\end{code}

\begin{code}
483
data SimplContext
484
485
486
487
  = 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
488
489

instance Outputable SimplContext where
490
491
492
  ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
  ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
  ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
493
494
495
496
497
498
499
500
501
502
  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
503
504
simplEqsOnly (SimplRuleLhs {}) = True
simplEqsOnly _                 = False
505
506

performDefaulting :: SimplContext -> Bool
507
508
509
510
performDefaulting (SimplInfer {})   = False
performDefaulting (SimplRuleLhs {}) = False
performDefaulting SimplInteractive  = True
performDefaulting (SimplCheck {})   = True
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547

---------------
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

548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
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 }
563
564

runTcS :: SimplContext
565
       -> Untouchables 	       -- Untouchables
566
       -> TcS a		       -- What to run
567
       -> TcM (a, Bag EvBind)
568
runTcS context untouch tcs 
569
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
570
       ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
571
       ; step_count <- TcM.newTcRef 0
dimitris's avatar
dimitris committed
572
       ; flat_cache_var <- TcM.newTcRef emptyFlatCache
573
574
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
575
                          , tcs_context  = context
576
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
577
578
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
dimitris's avatar
dimitris committed
579
                          , tcs_flat_map = flat_cache_var
580
                          }
581
582

	     -- Run the computation
583
       ; res <- unTcS tcs env
584
585
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
586
       ; mapM_ do_unification (varEnvElts ty_binds)
587

588
589
#ifdef DEBUG
       ; count <- TcM.readTcRef step_count
590
       ; when (opt_PprStyle_Debug && count > 0) $
591
592
         TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
                            <+> int count <+> ppr context)
593
#endif
594
             -- And return
595
       ; ev_binds      <- TcM.readTcRef evb_ref
596
       ; return (res, evBindMapBinds ev_binds) }
597
598
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
599

600
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
601
602
603
604
605
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
dimitris's avatar
dimitris committed
606
607
608
609
                   , tcs_context = ctxt 
                   , tcs_flat_map = orig_flat_cache_var
                   } ->
    do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
610
611
612
613
       		   -- 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!
dimitris's avatar
dimitris committed
614
615

       ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
616
617
618
       ; flat_cache_var  <- TcM.newTcRef orig_flat_cache
       -- One could be more conservative as well: 
       -- ; flat_cache_var  <- TcM.newTcRef emptyFlatCache 
dimitris's avatar
dimitris committed
619
620
621
622
623
624
625
626
627
628
629
630

                            -- Consider copying the results the tcs_flat_map of the 
                            -- incomping constraint, but we must make sure that we
                            -- have pushed everything in, which seems somewhat fragile
       ; let nest_env = TcSEnv { tcs_ev_binds = ref
                               , tcs_ty_binds = ty_binds
                               , tcs_untch    = inner_untch
                               , tcs_count    = count
                               , tcs_ic_depth = idepth+1
                               , tcs_context  = ctxtUnderImplic ctxt 
                               , tcs_flat_map = flat_cache_var }
       ; thing_inside nest_env }
631

632
633
634
635
636
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

637
638
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
639
640
641
ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 
                                               <+> doubleQuotes (ftext n))
ctxtUnderImplic ctxt              = ctxt
642

643
tryTcS :: TcS a -> TcS a
dimitris's avatar
dimitris committed
644
-- Like runTcS, but from within the TcS monad
645
-- Ignore all the evidence generated, and do not affect caller's evidence!
dimitris's avatar
dimitris committed
646
tryTcS tcs
647
  = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
648
                    ; ev_binds_var <- TcM.newTcEvBinds
dimitris's avatar
dimitris committed
649
                    ; flat_cache_var <- TcM.newTcRef emptyFlatCache
650
                    ; let env1 = env { tcs_ev_binds = ev_binds_var
dimitris's avatar
dimitris committed
651
652
653
                                     , tcs_ty_binds = ty_binds_var
                                     , tcs_flat_map = flat_cache_var }
                   ; unTcS tcs env1 })
654
655
656
657
658
659
660
661
662
663
664
665
666

-- 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) 

667
getUntouchables :: TcS TcsUntouchables
668
669
getUntouchables = TcS (return . tcs_untch)

670
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
671
672
getTcSTyBinds = TcS (return . tcs_ty_binds)

673
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
674
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
675

dimitris's avatar
dimitris committed
676
677
678
679
680
getFlatCacheMapVar :: TcS (IORef FlatCache)
getFlatCacheMapVar
  = TcS (return . tcs_flat_map)

lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor 
batterseapower's avatar
batterseapower committed
681
                   -> TcS (Maybe (TcType,EqVar,CtFlavor))
dimitris's avatar
dimitris committed
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
-- For givens, we lookup in given flat cache
lookupFlatCacheMap tc xis (Given {})
  = do { cache_ref <- getFlatCacheMapVar
       ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
       ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
-- For wanteds, we first lookup in givenFlatCache.
-- If we get nothing back then we lookup in wantedFlatCache.
lookupFlatCacheMap tc xis (Wanted {})
  = do { cache_ref <- getFlatCacheMapVar
       ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
       ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
           Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
           other   -> return other }
lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing

updateFlatCacheMap :: TyCon -> [Xi]
batterseapower's avatar
batterseapower committed
698
699
                   -> TcType -> CtFlavor -> EqVar -> TcS ()
updateFlatCacheMap _tc _xis _tv (Derived {}) _eqv
dimitris's avatar
dimitris committed
700
  = return () -- Not caching deriveds
batterseapower's avatar
batterseapower committed
701
updateFlatCacheMap tc xis ty fl eqv
dimitris's avatar
dimitris committed
702
703
704
705
  = do { cache_ref <- getFlatCacheMapVar
       ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
       ; let new_cache_map
              | isGivenOrSolved fl
batterseapower's avatar
batterseapower committed
706
              = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,eqv,fl) $
dimitris's avatar
dimitris committed
707
708
                                             givenFlatCache cache_map }
              | isWanted fl
batterseapower's avatar
batterseapower committed
709
              = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,eqv,fl) $
dimitris's avatar
dimitris committed
710
711
712
713
                                              wantedFlatCache cache_map }
              | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
       ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }

714

715
716
717
718
719
getTcEvBindsBag :: TcS EvBindMap
getTcEvBindsBag
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

batterseapower's avatar
batterseapower committed
720
721
setEqBind :: EqVar -> LCoercion -> TcS () 
setEqBind eqv co = setEvBind eqv (EvCoercionBox co)
722
723
724

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
725
-- We never do this twice!
726
727
728
729
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
730
731
732
733
734
735
#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
736
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
737
738
739
740
741
742
743
744
745

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

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

setEvBind :: EvVar -> EvTerm -> TcS () 
-- Internal
batterseapower's avatar
batterseapower committed
746
setEvBind ev t
747
  = do { tc_evbinds <- getTcEvBinds
batterseapower's avatar
batterseapower committed
748
       ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t }
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788

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
batterseapower's avatar
batterseapower committed
789
pprEq ty1 ty2 = pprType $ mkEqPred (ty1,ty2)
790
791

isTouchableMetaTyVar :: TcTyVar -> TcS Bool
792
isTouchableMetaTyVar tv 
793
794
795
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

796
797
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
798
  = case tcTyVarDetails tv of 
799
800
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
801
802
803
804
      MetaTv {}      -> inTouchableRange untch tv 
      _              -> False 


805
806
\end{code}

807

808
809
810
811
812
813
814
815
816
817
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.
818
819


820
\begin{code}
821
822
823
824
825
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
826
827
828

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
829
  = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
830
                            ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
831
832
833
834
                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
       ; traceTcS "New Flatten Skolem Born" $ 
           (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
       ; return tv }
835
836
837
838
839

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

instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
840
841
842
843
instDFunTypes mb_inst_tys 
  = mapM inst_tv mb_inst_tys
  where
    inst_tv :: Either TyVar TcType -> TcS Type
844
    inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
845
    inst_tv (Right ty) = return ty 
846
847
848
849

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

850

851
instFlexiTcS :: TyVar -> TcS TcTyVar 
852
853
854
-- 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] 
855
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
856

857
858
859
860
861
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
862
       ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
863
864
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

865
866
867
868
869
870
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

871
newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
872
873
-- Create new wanted CoVar that constrains the type to have the specified kind. 
newKindConstraint tv knd 
874
  = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
875
       ; let ty_k = mkTyVarTy tv_k
batterseapower's avatar
batterseapower committed
876
877
       ; eqv <- newEqVar (mkTyVarTy tv) ty_k
       ; return eqv }
878

879
880
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper tvname tvkind
881
882
883
884
885
886
  = wrapTcS $ 
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
       ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
887
888
889
890

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

891
892
newEvVar :: TcPredType -> TcS EvVar
newEvVar pty = wrapTcS $ TcM.newEvVar pty
893

894
895
896
newDerivedId :: TcPredType -> TcS EvVar 
newDerivedId pty = wrapTcS $ TcM.newEvVar pty

batterseapower's avatar
batterseapower committed
897
newGivenEqVar :: TcType -> TcType -> Coercion -> TcS EvVar 
898
899
900
901
-- 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 
batterseapower's avatar
batterseapower committed
902
903
904
newGivenEqVar ty1 ty2 co 
  = do { cv <- newEqVar ty1 ty2
       ; setEvBind cv (EvCoercionBox co) 
905
906
       ; return cv } 

batterseapower's avatar
batterseapower committed
907
908
newEqVar :: TcType -> TcType -> TcS EvVar
newEqVar ty1 ty2 = wrapTcS $ TcM.newEq ty1 ty2 
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932

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
933
        ; case lookupInstEnv instEnvs clas tys of {
934
            ([], unifs, _)               -- Nothing matches  
935
936
937
938
939
                -> do { traceTcS "matchClass not matching"
                                 (vcat [ text "dict" <+> ppr pred, 
                                         text "unifs" <+> ppr unifs ]) 
                      ; return MatchInstNo  
                      } ;  
940
	    ([(ispec, inst_tys)], [], _) -- A single match 
941
942
943
944
		-> do	{ let dfun_id = is_dfun ispec
			; traceTcS "matchClass success"
				   (vcat [text "dict" <+> ppr pred, 
				          text "witness" <+> ppr dfun_id
945
                                           <+> ppr (idType dfun_id) ])
946
				  -- Record that this dfun is needed
947
                        ; return $ MatchInstSingle (dfun_id, inst_tys)
948
                        } ;
949
     	    (matches, unifs, _)          -- More than one matches 
950
951
952
953
954
955
956
957
		-> do	{ traceTcS "matchClass multiple matches, deferring choice"
			           (vcat [text "dict" <+> ppr pred,
				   	  text "matches" <+> ppr matches,
				   	  text "unifs" <+> ppr unifs])
                        ; return MatchInstMany 
		        }
	}
        }
958

959
matchFam :: TyCon -> [Type] -> TcS (Maybe (TyCon, [Type]))
960
matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
961
\end{code}