TcSMonad.lhs 66.8 KB
Newer Older
1
\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
2
{-# OPTIONS -fno-warn-tabs -w #-}
Ian Lynagh's avatar
Ian Lynagh committed
3
4
5
6
7
8
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

9
10
11
-- Type definitions for the constraint solver
module TcSMonad ( 

12
       -- Canonical constraints, definition is now in TcRnTypes
13

14
15
    WorkList(..), isEmptyWorkList, emptyWorkList,
    workListFromEq, workListFromNonEq, workListFromCt, 
16
17
    extendWorkListEq, extendWorkListFunEq, 
    extendWorkListNonEq, extendWorkListCt, 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
18
    extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
19
    withWorkList, workListSize,
20

Simon Peyton Jones's avatar
Simon Peyton Jones committed
21
    updWorkListTcS, updWorkListTcS_return,
22
    
23
    updTcSImplics, 
24

25
    Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, 
26
    emitInsoluble,
27

28
    isWanted, isDerived, 
29
    isGivenCt, isWantedCt, isDerivedCt, 
30

31
    canRewrite, canSolve,
32
    mkGivenLoc, 
33

34
    TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality 
35
    traceFireTcS, bumpStepCountTcS, 
36
    tryTcS, nestTcS, nestImplicTcS, recoverTcS,
37
38
    wrapErrTcS, wrapWarnTcS,

dimitris's avatar
dimitris committed
39
    -- Getting and setting the flattening cache
40
    addSolvedDict, addSolvedFunEq, getFlattenSkols,
41
42
43

    -- Marking stuff as used
    addUsedRdrNamesTcS,
dimitris's avatar
dimitris committed
44
    
45
    deferTcSForAllEq, 
dimitris's avatar
dimitris committed
46
47
48
    
    setEvBind,
    XEvTerm(..),
49
    MaybeNew (..), isFresh, freshGoal, freshGoals, getEvTerm, getEvTerms,
50

51
52
    xCtFlavor,        -- Transform a CtEvidence during a step 
    rewriteCtFlavor,  -- Specialized version of xCtFlavor for coercions
53
    newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
dimitris's avatar
dimitris committed
54
55
    newDerived,
    
56
       -- Creation of evidence variables
57
58
    setWantedTyBind,

59
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
60
    getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
61
    getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
62

63

64
    lookupFlatEqn, newFlattenSkolem,            -- Flatten skolems 
65

Simon Peyton Jones's avatar
Simon Peyton Jones committed
66
67
68
        -- Deque
    Deque(..), insertDeque, emptyDeque,

69
        -- Inerts 
dimitris's avatar
dimitris committed
70
    InertSet(..), InertCans(..), 
71
    getInertEqs, 
72
    emptyInert, getTcSInerts, lookupInInerts, 
73
74
    getInertUnsolved, checkAllSolved, 
    prepareInertsForImplications,
75
    modifyInertTcS,
76
    insertInertItemTcS, partitionCCanMap, partitionEqMap,
77
    getRelevantCts, extractRelevantInerts,
78
    getInertsFunEqTyCon,
79
80
    CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
    PredMap, FamHeadMap,
81
    partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
82
    filterSolved,
83

84
    instDFunType,                              -- Instantiation
85
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
86
    cloneMetaTyVar,
87

88
    Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
89
    zonkTyVarsAndFV,
90

91
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
92

93
    matchFam, matchOpenFam, 
94
    checkWellStagedDFun, 
95
    pprEq                                    -- Smaller utils, re-exported from TcM
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
                                             -- 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 Inst
import InstEnv 
import FamInst 
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM 
114
       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
115
import Kind
116
117
import TcType
import DynFlags
118
import Type
119

120
import TcEvidence
121
122
import Class
import TyCon
123

124
import Name
125
126
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
127
import Var
128
import VarEnv
129
130
131
import Outputable
import Bag
import MonadUtils
132

133
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
134
import Util
135
import Id 
Ian Lynagh's avatar
Ian Lynagh committed
136
import TcRnTypes
137

138
139
import Unique 
import UniqFM
140
import Maybes ( orElse, catMaybes, firstJust )
141
import Pair ( pSnd )
142

143
import Control.Monad( unless, when, zipWithM )
Ian Lynagh's avatar
Ian Lynagh committed
144
import Data.IORef
145
import TrieMap
146

147
148
149
150
151
#ifdef DEBUG
import StaticFlags( opt_PprStyle_Debug )
import VarSet
import Digraph
#endif
152
\end{code}
153

154
155
156
157
158
159
160
161
%************************************************************************
%*									*
%*                            Worklists                                *
%*  Canonical and non-canonical constraints that the simplifier has to  *
%*  work on. Including their simplification depths.                     *
%*                                                                      *
%*									*
%************************************************************************
162

163
164
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
165
166
167
A WorkList contains canonical and non-canonical items (of all flavors). 
Notice that each Ct now has a simplification depth. We may 
consider using this depth for prioritization as well in the future. 
168

169
170
171
172
173
As a simple form of priority queue, our worklist separates out
equalities (wl_eqs) from the rest of the canonical constraints, 
so that it's easier to deal with them first, but the separation 
is not strictly necessary. Notice that non-canonical constraints 
are also parts of the worklist. 
174

175

176
177
178
179
180
181
Note [NonCanonical Semantics]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that canonical constraints involve a CNonCanonical constructor. In the worklist
we use this constructor for constraints that have not yet been canonicalized such as 
   [Int] ~ [a] 
In other words, all constraints start life as NonCanonicals. 
182

183
184
On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
means that we have a ``frozen error''. 
185

186
187
188
NonCanonical constraints never interact directly with other constraints -- but they can
be rewritten by equalities (for instance if a non canonical exists in the inert, we'd 
better rewrite it as much as possible before reporting it as an error to the user)
189

190
\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
191
192
193
194
195
196
197
198
199
200
201
202
data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
                            -- First to remove is at head of LH field

instance Outputable a => Outputable (Deque a) where
  ppr (DQ as bs) = ppr (as ++ reverse bs)   -- Show first one to come out at the start

emptyDeque :: Deque a
emptyDeque = DQ [] []

isEmptyDeque :: Deque a -> Bool
isEmptyDeque (DQ as bs) = null as && null bs

203
204
205
dequeSize :: Deque a -> Int
dequeSize (DQ as bs) = length as + length bs

Simon Peyton Jones's avatar
Simon Peyton Jones committed
206
207
208
209
210
211
212
213
214
215
216
217
insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)

appendDeque :: Deque a -> Deque a -> Deque a
appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2

extractDeque :: Deque a -> Maybe (Deque a, a)
extractDeque (DQ [] [])     = Nothing
extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
extractDeque (DQ [] bs)     = case reverse bs of
                                (a:as) -> Just (DQ as [], a)
                                [] -> panic "extractDeque"
218

219
-- See Note [WorkList priorities]
220
data WorkList = WorkList { wl_eqs    :: [Ct]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
221
                         , wl_funeqs :: Deque Ct
222
223
                         , wl_rest   :: [Ct] 
                         }
224

batterseapower's avatar
batterseapower committed
225

Simon Peyton Jones's avatar
Simon Peyton Jones committed
226
227
228
229
230
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList new_wl orig_wl 
   = WorkList { wl_eqs    = wl_eqs new_wl    ++            wl_eqs orig_wl
              , wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
              , wl_rest   = wl_rest new_wl   ++            wl_rest orig_wl }
231

232

233
234
235
236
workListSize :: WorkList -> Int
workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
  = length eqs + dequeSize funeqs + length rest

237
238
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
dimitris's avatar
dimitris committed
239
240
extendWorkListEq ct wl 
  | Just {} <- isCFunEqCan_Maybe ct
241
  = extendWorkListFunEq ct wl
dimitris's avatar
dimitris committed
242
243
  | otherwise
  = wl { wl_eqs = ct : wl_eqs wl }
244

245
246
247
248
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl 
  = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
249
250
251
252
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
extendWorkListEqs cts wl = foldr extendWorkListEq wl cts

253
254
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
255
256
extendWorkListNonEq ct wl 
  = wl { wl_rest = ct : wl_rest wl }
257

258
259
260
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
dimitris's avatar
dimitris committed
261
 | isEqPred (ctPred ct) = extendWorkListEq ct wl
262
 | otherwise = extendWorkListNonEq ct wl
263

Simon Peyton Jones's avatar
Simon Peyton Jones committed
264
extendWorkListCts :: [Ct] -> WorkList -> WorkList
265
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
266
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
267
268

isEmptyWorkList :: WorkList -> Bool
dimitris's avatar
dimitris committed
269
isEmptyWorkList wl 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
270
  = null (wl_eqs wl) &&  null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
271
272

emptyWorkList :: WorkList
Simon Peyton Jones's avatar
Simon Peyton Jones committed
273
emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = emptyDeque }
274

275
workListFromEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
276
workListFromEq ct = extendWorkListEq ct emptyWorkList
277

278
workListFromNonEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
279
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
280

281
282
workListFromCt :: Ct -> WorkList
-- Agnostic 
dimitris's avatar
dimitris committed
283
284
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct 
                  | otherwise            = workListFromNonEq ct
285

dimitris's avatar
dimitris committed
286
287
288
289
290

selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
  = case (eqs,feqs,rest) of
      (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
291
292
      (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
                       -> (Just ct, wl { wl_funeqs = fun_eqs' })
dimitris's avatar
dimitris committed
293
294
295
      (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
      (_,_,_)          -> (Nothing,wl)

296
297
298
-- Pretty printing 
instance Outputable WorkList where 
  ppr wl = vcat [ text "WorkList (eqs)   = " <+> ppr (wl_eqs wl)
dimitris's avatar
dimitris committed
299
                , text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
300
301
                , text "WorkList (rest)  = " <+> ppr (wl_rest wl)
                ]
302
303


dimitris's avatar
dimitris committed
304
-- Canonical constraint maps
305
306
307
308
309
310
311
data CCanMap a 
  = CCanMap { cts_given   :: UniqFM Cts   -- All Given
            , cts_derived :: UniqFM Cts   -- All Derived
            , cts_wanted  :: UniqFM Cts } -- All Wanted

keepGivenCMap :: CCanMap a -> CCanMap a
keepGivenCMap cc = emptyCCanMap { cts_given = cts_given cc }
312

313
314
315
instance Outputable (CCanMap a) where
  ppr (CCanMap given derived wanted) = ptext (sLit "CCanMap") <+> (ppr given) <+> (ppr derived) <+> (ppr wanted)

316
317
318
319
320
321
322
323
324
325
cCanMapToBag :: CCanMap a -> Cts 
cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
  where rest_wder = foldUFM unionBags rest_der  (cts_wanted cmap) 
        rest_der  = foldUFM unionBags emptyCts  (cts_derived cmap)

emptyCCanMap :: CCanMap a 
emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM } 

updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a 
updCCanMap (a,ct) cmap 
326
  = case cc_ev ct of 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
327
328
329
      CtWanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
      CtGiven {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
      CtDerived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
  where 
    insert_into m = addToUFM_C unionBags m a (singleCt ct)

getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a) 
-- Gets the relevant constraints and returns the rest of the CCanMap
getRelevantCts a cmap 
    = let relevant = lookup (cts_wanted cmap) `unionBags`
                     lookup (cts_given cmap)  `unionBags`
                     lookup (cts_derived cmap) 
          residual_map = cmap { cts_wanted  = delFromUFM (cts_wanted cmap) a
                              , cts_given   = delFromUFM (cts_given cmap) a
                              , cts_derived = delFromUFM (cts_derived cmap) a }
      in (relevant, residual_map) 
  where
    lookup map = lookupUFM map a `orElse` emptyCts

346
347
348
349
350
351
352
lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence
lookupCCanMap a pick_me map
  = findEvidence pick_me possible_cts
  where
     possible_cts = lookupUFM (cts_given map)   a `plus` (
                    lookupUFM (cts_wanted map)  a `plus` (
                    lookupUFM (cts_derived map) a `plus` emptyCts))
353

354
355
356
357
358
359
360
361
362
363
     plus Nothing     cts2 = cts2
     plus (Just cts1) cts2 = cts1 `unionBags` cts2

findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence
findEvidence pick_me cts
  = foldrBag pick Nothing cts
  where
     pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
     pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
                   | otherwise                             = deflt
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378

partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) 
-- All constraints that /match/ the predicate go in the bag, the rest remain in the map
partitionCCanMap pred cmap
  = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap) 
        (ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap)
        (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap) 
    in (ws `andCts` ds `andCts` gs, cmap { cts_wanted  = ws_map
                                         , cts_given   = gs_map
                                         , cts_derived = ds_map }) 
  where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts)
                                    where new_mp      = addToUFM mp k cts_keep
                                          new_acc_cts = acc_cts `andCts` cts_out
                                          (cts_out, cts_keep) = partitionBag pred this_cts

379
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
380
381
382
383
384
385
partitionEqMap pred isubst 
  = let eqs_out = foldVarEnv extend_if_pred [] isubst
        eqs_in  = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
    in (eqs_out, eqs_in)
  where extend_if_pred (ct,_) cts = if pred ct then ct : cts else cts

386
387
388
389
extractUnsolvedCMap :: CCanMap a -> Cts
-- Gets the wanted or derived constraints
extractUnsolvedCMap cmap = foldUFM unionBags emptyCts (cts_wanted cmap)
              `unionBags`  foldUFM unionBags emptyCts (cts_derived cmap)
390

dimitris's avatar
dimitris committed
391
-- Maps from PredTypes to Constraints
392
393
394
395
396
397
type CtTypeMap    = TypeMap    Ct
type CtPredMap    = PredMap    Ct
type CtFamHeadMap = FamHeadMap Ct

newtype PredMap    a = PredMap    { unPredMap    :: TypeMap a } -- Indexed by TcPredType
newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head
398

399
400
401
402
403
instance Outputable a => Outputable (PredMap a) where
   ppr (PredMap m) = ppr (foldTM (:) m [])

instance Outputable a => Outputable (FamHeadMap a) where
   ppr (FamHeadMap m) = ppr (foldTM (:) m [])
404

405
406
407
sizePredMap :: PredMap a -> Int
sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m

408
409
410
emptyFamHeadMap :: FamHeadMap a
emptyFamHeadMap = FamHeadMap emptyTM

411
412
413
sizeFamHeadMap :: FamHeadMap a -> Int
sizeFamHeadMap (FamHeadMap m) = foldTypeMap (\_ x -> x+1) 0 m

414
415
416
ctTypeMapCts :: TypeMap Ct -> Cts
ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts

417
418
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
dimitris's avatar
dimitris committed
419

420
421
422
423
424
425
426
427
428
insertFamHead :: FamHeadMap a -> TcType -> a -> FamHeadMap a
insertFamHead (FamHeadMap m) key value = FamHeadMap (alterTM key (const (Just value)) m)

delFamHead :: FamHeadMap a -> TcType -> FamHeadMap a
delFamHead (FamHeadMap m) key = FamHeadMap (alterTM key (const Nothing) m)

anyFamHeadMap :: (Ct -> Bool) -> CtFamHeadMap -> Bool
anyFamHeadMap f ctmap = foldTM ((||) . f) (unFamHeadMap ctmap) False

dimitris's avatar
dimitris committed
429
430
431
432
433
partCtFamHeadMap :: (Ct -> Bool) 
                 -> CtFamHeadMap 
                 -> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
  = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
434
    in (cts, FamHeadMap tymap_final)
dimitris's avatar
dimitris committed
435
  where
436
    tymap_inside = unFamHeadMap ctmap 
dimitris's avatar
dimitris committed
437
    upd_acc ct (cts,acc_map)
438
439
         | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
         | otherwise = (cts,acc_map)
dimitris's avatar
dimitris committed
440
441
442
443
         where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
                      = ty1 
                      | otherwise 
                      = panic "partCtFamHeadMap, encountered non equality!"
444
445
446
447
448

filterSolved :: (CtEvidence -> Bool) -> PredMap CtEvidence -> PredMap CtEvidence
filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
  where upd a m = if p a then alterTM (ctEvPred a) (\_ -> Just a) m
                         else m
dimitris's avatar
dimitris committed
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
\end{code}

%************************************************************************
%*									*
%*                            Inert Sets                                *
%*                                                                      *
%*									*
%************************************************************************

Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
  1 All canonical
  2 All Given or Wanted or Derived. No (partially) Solved
  3 No two dictionaries with the same head
464
465
466
467
468
469
470
  4 No two family equations with the same head 
      NB: This is enforced by construction since we use a CtFamHeadMap for inert_funeqs
  5 Family equations inert wrt top-level family axioms
  6 Dictionaries have no matching top-level instance 
  
  7 Non-equality constraints are fully rewritten with respect to the equalities (CTyEqCan)

471
472
473
474
475
476
477
478
479
480
  8 Equalities _do_not_ form an idempotent substitution, but they are
    guaranteed to not have any occurs errors. Additional notes: 

       - The lack of idempotence of the inert substitution implies
         that we must make sure that when we rewrite a constraint we
         apply the substitution /recursively/ to the types
         involved. Currently the one AND ONLY way in the whole
         constraint solver that we rewrite types and constraints wrt
         to the inert substitution is TcCanonical/flattenTyVar.

Gabor Greif's avatar
typos    
Gabor Greif committed
481
       - In the past we did try to have the inert substitution as
482
483
484
485
486
487
488
489
490
491
492
493
494
         idempotent as possible but this would only be true for
         constraints of the same flavor, so in total the inert
         substitution could not be idempotent, due to flavor-related
         issued.  Note [Non-idempotent inert substitution] explains
         what is going on.

       - Whenever a constraint ends up in the worklist we do
         recursively apply exhaustively the inert substitution to it
         to check for occurs errors.  But if an equality is already in
         the inert set and we can guarantee that adding a new equality
         will not cause the first equality to have an occurs check
         then we do not rewrite the inert equality.  This happens in
         TcInteract, rewriteInertEqsFromInertEq.
495
         
496
497
498
         See Note [Delicate equality kick-out] to see which inert
         equalities can safely stay in the inert set and which must be
         kicked out to be rewritten and re-checked for occurs errors.
499

dimitris's avatar
dimitris committed
500
501
  9 Given family or dictionary constraints don't mention touchable unification variables

502
503
504
505
506
507
508
509
510
511
512
513
514
515
Note [Solved constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~
When we take a step to simplify a constraint 'c', we call the original constraint "solved".
For example:   Wanted:    ev  :: [s] ~ [t]
               New goal:  ev1 :: s ~ t
               Then 'ev' is now "solved".

The reason for all this is simply to avoid re-solving goals we have solved already.

* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
  use it to rewrite a Given; in that sense the solved goal is still a Wanted

* A solved Given is just given

516
517
518
519
* A solved Derived in inert_solved is possible; purpose is to avoid
  creating tons of identical Derived goals.

  But there are no solved Deriveds in inert_solved_funeqs
dimitris's avatar
dimitris committed
520

521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, of form (ev : F tys ~ ty), live in four places

  * The work-list, of course

  * The inert_flat_cache.  This is used when flattening, to get maximal
    sharing.  It contains lots of things that are still in the work-list.
    E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
        work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
        list.  Now if we flatten w2 before we get to w3, we still want to 
        share that (G a).

    Because it contains work-list things, DO NOT use the flat cache to solve
    a top-level goal.  Eg in the above example we don't want to solve w3 
    using w3 itself!  

  * The inert_solved_funeqs.  These are all "solved" goals (see Note [Solved constraints]),
    the result of using a top-level type-family instance.

  * THe inert_funeqs are un-solved but fully processed and in the InertCans.

543
544

\begin{code}
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
data InertCans 
  = IC { inert_eqs :: TyVarEnv Ct
              -- Must all be CTyEqCans! If an entry exists of the form: 
              --   a |-> ct,co
              -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
              -- And  co : a ~ xi
       , inert_dicts :: CCanMap Class
              -- Dictionaries only, index is the class
              -- NB: index is /not/ the whole type because FD reactions 
              -- need to match the class but not necessarily the whole type.
       , inert_funeqs :: CtFamHeadMap
              -- Family equations, index is the whole family head type.
       , inert_irreds :: Cts       
              -- Irreducible predicates

       , inert_insols :: Cts       
              -- Frozen errors (as non-canonicals)
       }
    
                     
dimitris's avatar
dimitris committed
567
568
569
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
570
571
572
              -- Canonical Given, Wanted, Derived (no Solved)
	      -- Sometimes called "the inert set"

573
574
575
576
577
578
579
       , inert_flat_cache :: FamHeadMap (CtEvidence, TcType)
              -- See Note [Type family equations]
              -- Just a hash-cons cache for use when flattening only
              -- These include entirely un-processed goals, so don't use
              -- them to solve a top-level goal, else you may end up solving
              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
              -- when allocating a new flatten-skolem.
580
              -- Not necessarily inert wrt top-level equations (or inert_cans)
581
582
583
 
       , inert_fsks :: [TcTyVar]  -- Rigid flatten-skolems (arising from givens)
                                  -- allocated in this local scope
584

585
586
       , inert_solved_funeqs :: FamHeadMap (CtEvidence, TcType)
              -- See Note [Type family equations]
587
588
589
              -- Of form co :: F xis ~ xi 
              -- Always the result of using a top-level family axiom F xis ~ tau
              -- No Deriveds 
590
              -- Not necessarily fully rewritten (by type substitutions)
591

592
593
594
       , inert_solved_dicts   :: PredMap CtEvidence 
       	      -- Of form ev :: C t1 .. tn
              -- Always the result of using a top-level instance declaration
595
              -- See Note [Solved constraints]
596
597
       	      -- - Used to avoid creating a new EvVar when we have a new goal 
       	      --   that we have solved in the past
Simon Peyton Jones's avatar
Simon Peyton Jones committed
598
       	      -- - Stored not necessarily as fully rewritten 
599
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
600
       }
601
602


dimitris's avatar
dimitris committed
603
instance Outputable InertCans where 
604
605
606
607
  ppr ics = vcat [ ptext (sLit "Equalities:") 
                   <+> vcat (map ppr (varEnvElts (inert_eqs ics)))
                 , ptext (sLit "Type-function equalities:")
                   <+> vcat (map ppr (Bag.bagToList $ 
608
                                  ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
609
610
611
612
                 , ptext (sLit "Dictionaries:")
                   <+> vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
                 , ptext (sLit "Irreds:")
                   <+> vcat (map ppr (Bag.bagToList $ inert_irreds ics))
613
614
                 , text "Insolubles =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
dimitris's avatar
dimitris committed
615
616
617
618
                 ]
            
instance Outputable InertSet where 
  ppr is = vcat [ ppr $ inert_cans is
619
620
                , text "Solved dicts"  <+> int (sizePredMap (inert_solved_dicts is))
                , text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
621

dimitris's avatar
dimitris committed
622
623
624
625
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                         , inert_dicts  = emptyCCanMap
626
                         , inert_funeqs = emptyFamHeadMap
627
628
                         , inert_irreds = emptyCts
                         , inert_insols = emptyCts }
629
       , inert_fsks          = []
630
       , inert_flat_cache    = emptyFamHeadMap
631
       , inert_solved_dicts  = PredMap emptyTM 
632
       , inert_solved_funeqs = emptyFamHeadMap }
633

634
insertInertItem :: Ct -> InertSet -> InertSet 
635
-- Add a new inert element to the inert set. 
636
insertInertItem item is
637
638
  = -- A canonical Given, Wanted, or Derived
    is { inert_cans = upd_inert_cans (inert_cans is) item }
dimitris's avatar
dimitris committed
639
  
640
  where upd_inert_cans :: InertCans -> Ct -> InertCans
dimitris's avatar
dimitris committed
641
642
643
        -- Precondition: item /is/ canonical
        upd_inert_cans ics item
          | isCTyEqCan item                     
644
          = let upd_err a b = pprPanic "insertInertItem" $
dimitris's avatar
dimitris committed
645
646
647
648
649
650
                              vcat [ text "Multiple inert equalities:"
                                   , text "Old (already inert):" <+> ppr a
                                   , text "Trying to insert   :" <+> ppr b ]
        
                eqs'     = extendVarEnv_C upd_err (inert_eqs ics) 
                                                  (cc_tyvar item) item        
651
652

            in ics { inert_eqs = eqs' }
dimitris's avatar
dimitris committed
653
654
655
656
657
658
659
660
661
662
663

          | isCIrredEvCan item                  -- Presently-irreducible evidence
          = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }

          | Just cls <- isCDictCan_Maybe item   -- Dictionary 
          = ics { inert_dicts = updCCanMap (cls,item) (inert_dicts ics) }

          | Just _tc <- isCFunEqCan_Maybe item  -- Function equality
          = let fam_head = mkTyConApp (cc_fun item) (cc_tyargs item)
                upd_funeqs Nothing = Just item
                upd_funeqs (Just _already_there) 
664
                  = panic "insertInertItem: item already there!"
665
            in ics { inert_funeqs = FamHeadMap 
dimitris's avatar
dimitris committed
666
                                      (alterTM fam_head upd_funeqs $ 
667
                                         (unFamHeadMap $ inert_funeqs ics)) }
dimitris's avatar
dimitris committed
668
669
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
670
671
672
            ppr item   -- Can't be CNonCanonical, CHoleCan, 
                       -- because they only land in inert_insols

673

674
insertInertItemTcS :: Ct -> TcS ()
675
-- Add a new item in the inerts of the monad
676
677
insertInertItemTcS item
  = do { traceTcS "insertInertItemTcS {" $ 
678
679
         text "Trying to insert new inert item:" <+> ppr item

680
       ; updInertTcS (insertInertItem item) 
681
                        
682
       ; traceTcS "insertInertItemTcS }" $ empty }
683

684
addSolvedDict :: CtEvidence -> TcS ()
685
-- Add a new item in the solved set of the monad
686
addSolvedDict item
687
688
689
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
  = return () 
  | otherwise
690
691
692
693
694
695
696
697
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
       ; updInertTcS upd_solved_dicts }
  where
    upd_solved_dicts is 
      = is { inert_solved_dicts = PredMap $ alterTM pred upd_solved $ 
                                  unPredMap $ inert_solved_dicts is }
    pred = ctEvPred item
    upd_solved _ = Just item
698

699
700
701
702
703
addSolvedFunEq :: TcType -> CtEvidence -> TcType -> TcS ()
addSolvedFunEq fam_ty ev rhs_ty
  = updInertTcS $ \ inert -> 
    inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) 
                                                fam_ty (ev, rhs_ty) }
704

705
706
707
708
709
710
711
712
713
modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a 
-- Modify the inert set with the supplied function
modifyInertTcS upd 
  = do { is_var <- getTcSInertsRef
       ; curr_inert <- wrapTcS (TcM.readTcRef is_var)
       ; let (a, new_inert) = upd curr_inert
       ; wrapTcS (TcM.writeTcRef is_var new_inert)
       ; return a }

714
715
716
717
718
719
720
721
722
723
724
updInertTcS :: (InertSet -> InertSet) -> TcS () 
-- Modify the inert set with the supplied function
updInertTcS upd 
  = do { is_var <- getTcSInertsRef
       ; curr_inert <- wrapTcS (TcM.readTcRef is_var)
       ; let new_inert = upd curr_inert
       ; wrapTcS (TcM.writeTcRef is_var new_inert) }

prepareInertsForImplications :: InertSet -> InertSet
-- See Note [Preparing inert set for implications]
prepareInertsForImplications is
725
  = is { inert_cans   = getGivens (inert_cans is)
726
727
       , inert_fsks   = []
       , inert_flat_cache = emptyFamHeadMap }
728
  where
729
    getGivens (IC { inert_eqs    = eqs
730
731
732
                  , inert_irreds = irreds
                  , inert_funeqs = FamHeadMap funeqs
                  , inert_dicts  = dicts })
733
      = IC { inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
734
735
           , inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
           , inert_irreds = Bag.filterBag isGivenCt irreds
736
737
           , inert_dicts  = keepGivenCMap dicts
           , inert_insols = emptyCts }
738
739
740
741
742
743
744

    given_from_wanted funeq   -- This is where the magic processing happens 
      | isGiven ev = funeq    -- for type-function equalities
                              -- See Note [Preparing inert set for implications]
      | otherwise  = funeq { cc_ev = given_ev }
      where
        ev = ctEvidence funeq
745
        given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
746
                           , ctev_pred = ctev_pred ev }
747
748
749
750
751
752
753
\end{code}

Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we trim the inert set,
retaining only Givens.  These givens can be used when solving 
the inner implications.
dimitris's avatar
dimitris committed
754

755
756
757
758
With one wrinkle!  We take all *wanted* *funeqs*, and turn them into givens.
Consider (Trac #4935)
   type instance F True a b = a 
   type instance F False a b = b
759

760
761
762
763
764
765
766
767
768
769
   [w] F c a b ~ gamma 
   (c ~ True) => a ~ gamma 
   (c ~ False) => b ~ gamma

Obviously this is soluble with gamma := F c a b.  But
Since solveCTyFunEqs happens at the very end of solving, the only way
to solve the two implications is temporarily consider (F c a b ~ gamma)
as Given and push it inside the implications. Now, when we come
out again at the end, having solved the implications solveCTyFunEqs
will solve this equality.  
770

771
772
Turning type-function equalities into Givens is easy becase they 
*stay inert*.  No need to re-process them.
773

774
We don't try to turn any *other* Wanteds into Givens:
775

776
777
778
  * For example, we should not push given dictionaries in because
    of example LongWayOverlapping.hs, where we might get strange
    overlap errors between far-away constraints in the program.
779

780
781
There might be cases where interactions between wanteds can help
to solve a constraint. For example
782

783
784
  	class C a b | a -> b
  	(C Int alpha), (forall d. C d blah => C Int a)
785

786
787
788
789
If we push the (C Int alpha) inwards, as a given, it can produce a
fundep (alpha~a) and this can float out again and be used to fix
alpha.  (In general we can't float class constraints out just in case
(C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
790
791


792
\begin{code}
793
getInertEqs :: TcS (TyVarEnv Ct)
794
getInertEqs = do { inert <- getTcSInerts
795
                 ; return (inert_eqs (inert_cans inert)) }
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811

getInertUnsolved :: TcS (Cts, Cts)
-- Return (unsolved-wanteds, insolubles)
-- Both consist of a mixture of Wanted and Derived
getInertUnsolved
 = do { is <- getTcSInerts

      ; let icans = inert_cans is
            unsolved_irreds = Bag.filterBag is_unsolved (inert_irreds icans)
            unsolved_dicts  = extractUnsolvedCMap (inert_dicts icans)
            (unsolved_funeqs,_) = partCtFamHeadMap is_unsolved (inert_funeqs icans)
            unsolved_eqs = foldVarEnv add_if_unsolved emptyCts (inert_eqs icans)

            unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags` 
                             unsolved_dicts `unionBags` unsolved_funeqs

812
      ; return (unsolved_flats, inert_insols icans) }
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
  where
    add_if_unsolved ct cts
      | is_unsolved ct = cts `extendCts` ct
      | otherwise      = cts

    is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived

checkAllSolved :: TcS Bool
-- True if there are no unsolved wanteds
-- Ignore Derived for this purpose, unless in insolubles
checkAllSolved
 = do { is <- getTcSInerts

      ; let icans = inert_cans is
            unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
            unsolved_dicts  = not (isNullUFM (cts_wanted (inert_dicts icans)))
            unsolved_funeqs = anyFamHeadMap isWantedCt (inert_funeqs icans)
            unsolved_eqs    = foldVarEnv ((||) . isWantedCt) False (inert_eqs icans)

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
834
                     || not (isEmptyBag (inert_insols icans)))) }
835

836
837
838
839
840
841
842
843
844
845
846
847

{- Get inert function equation constraints that have the given tycon
in their head.  Not that the constraints remain in the inert set.
We use this to check for derived interactions with built-in type-function
constructors. -}
getInertsFunEqTyCon :: TyCon -> TcS [Ct]
getInertsFunEqTyCon tc =
  do is <- getTcSInerts
     let mp = unFamHeadMap $ inert_funeqs $ inert_cans is
     return $ lookupTypeMapTyCon mp tc


848
849
850
851
852
extractRelevantInerts :: Ct -> TcS Cts
-- Returns the constraints from the inert set that are 'relevant' to react with 
-- this constraint. The monad is left with the 'thinner' inerts. 
-- NB: This function contains logic specific to the constraint solver, maybe move there?
extractRelevantInerts wi 
dimitris's avatar
dimitris committed
853
  = modifyInertTcS (extract_relevants wi)
854
855
856
  where 
        extract_relevants :: Ct -> InertSet -> (Cts,InertSet)
        extract_relevants wi is 
dimitris's avatar
dimitris committed
857
858
859
          = let (cts,ics') = extract_ics_relevants wi (inert_cans is)
            in (cts, is { inert_cans = ics' }) 
            
860
        extract_ics_relevants :: Ct -> InertCans -> (Cts, InertCans)
dimitris's avatar
dimitris committed
861
862
863
        extract_ics_relevants (CDictCan {cc_class = cl}) ics = 
            let (cts,dict_map) = getRelevantCts cl (inert_dicts ics) 
            in (cts, ics { inert_dicts = dict_map })
864
865
866
867
868
869
870
871
872

        extract_ics_relevants ct@(CFunEqCan {}) ics@(IC { inert_funeqs = funeq_map })
            | Just ct <- lookupFamHead funeq_map fam_head
            = (singleCt ct, ics { inert_funeqs = delFamHead funeq_map fam_head })
            | otherwise
            = (emptyCts, ics)
            where
              fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)

873
874
875
876
        extract_ics_relevants (CHoleCan {}) ics
            = pprPanic "extractRelevantInerts" (ppr wi)
              -- Holes are put straight into inert_frozen, so never get here

dimitris's avatar
dimitris committed
877
878
879
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
880

dimitris's avatar
dimitris committed
881
882
883
        extract_ics_relevants _ ics = (emptyCts,ics)
        

884
lookupFlatEqn :: TcType -> TcS (Maybe (CtEvidence, TcType))
885
886
lookupFlatEqn fam_ty 
  = do { IS { inert_solved_funeqs = solved_funeqs
887
            , inert_flat_cache = flat_cache
888
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
889
       ; return (lookupFamHead solved_funeqs fam_ty `firstJust` 
890
891
                 lookup_in_inerts inert_funeqs    `firstJust`
                 lookupFamHead flat_cache fam_ty) }
892
893
894
895
896
  where
    lookup_in_inerts inert_funeqs 
        = case lookupFamHead inert_funeqs fam_ty of
            Nothing -> Nothing
            Just ct -> Just (ctEvidence ct, cc_rhs ct)
897
898

lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
dimitris's avatar
dimitris committed
899
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
900
lookupInInerts pty
901
902
  = do { inerts <- getTcSInerts
       ; case lookupSolvedDict inerts pty of
903
           Just ctev -> return (Just ctev)
904
           Nothing   -> return (lookupInInertCans inerts pty) }
dimitris's avatar
dimitris committed
905

906
lookupSolvedDict :: InertSet -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
907
-- Returns just if exactly this predicate type exists in the solved.
908
909
lookupSolvedDict (IS { inert_solved_dicts = solved }) pty 
  = lookupTM pty (unPredMap solved)
dimitris's avatar
dimitris committed
910

911
lookupInInertCans :: InertSet -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
912
-- Returns Just if exactly this pred type exists in the inert canonicals
913
lookupInInertCans (IS { inert_cans = ics }) pty
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
  = case (classifyPredType pty) of
      ClassPred cls _ 
         -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)

      EqPred ty1 _ty2 
         | Just tv <- getTyVar_maybe ty1      -- Tyvar equation
         , Just ct <- lookupVarEnv (inert_eqs ics) tv
      	 , let ctev = ctEvidence ct
      	 , ctEvPred ctev `eqType` pty
      	 -> Just ctev

      	 | Just _ <- splitTyConApp_maybe ty1  -- Family equation
      	 , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
      	 , let ctev = ctEvidence ct
      	 , ctEvPred ctev `eqType` pty
      	 -> Just ctev

      IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
    
933
      _other -> Nothing -- NB: No caching for IPs or holes
934
935
\end{code}

936

dimitris's avatar
dimitris committed
937
938


939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
%************************************************************************
%*									*
%*		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 { 
961
      tcs_ev_binds    :: EvBindsVar,
dimitris's avatar
dimitris committed
962
      
963
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
964
          -- Global type bindings
965
                     
dimitris's avatar
dimitris committed
966
967
      tcs_count      :: IORef Int, -- Global step count

968
      tcs_inerts   :: IORef InertSet, -- Current inert set
969
970
971
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
972
973
974
      -- while solving or canonicalising the current worklist.
      -- Specifically, when canonicalising (forall a. t1 ~ forall a. t2)
      -- from which we get the implication (forall a. t1 ~ t2)
975
      tcs_implics  :: IORef (Bag Implication)
976
    }
977
978
979
\end{code}

\begin{code}
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014

---------------
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 ()
1015
traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
1016

1017
1018
1019
instance HasDynFlags TcS where
    getDynFlags = wrapTcS getDynFlags

1020
1021
1022
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv

1023
1024
1025
1026
1027
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

1028
traceFireTcS :: Ct -> SDoc -> TcS ()
1029
-- Dump a rule-firing trace
1030
traceFireTcS ct doc 
1031
  = TcS $ \env -> 
1032
    TcM.whenDOptM Opt_D_dump_cs_trace $ 
1033
    do { n <- TcM.readTcRef (tcs_count env)
1034
       ; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
1035
       ; TcM.dumpTcRn msg }
1036

1037
1038
1039
1040
1041
1042
1043
1044
runTcS :: TcS a		       -- What to run
       -> TcM (a, Bag EvBind)
runTcS tcs
  = do { ev_binds_var <- TcM.newTcEvBinds
       ; res <- runTcSWithEvBinds ev_binds_var tcs
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
       ; return (res, ev_binds) }

1045
1046
1047
1048
runTcSWithEvBinds :: EvBindsVar
                  -> TcS a 
                  -> TcM a
runTcSWithEvBinds ev_binds_var tcs
1049
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
1050
       ; step_count <- TcM.newTcRef 0
1051
1052
       ; inert_var <- TcM.newTcRef is 

1053
1054
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
1055
			  , tcs_count    = step_count
1056
                          , tcs_inerts   = inert_var
1057
1058
1059
                          , tcs_worklist    = panic "runTcS: worklist"
                          , tcs_implics     = panic "runTcS: implics" }
                               -- NB: Both these are initialised by withWorkList
1060
1061

	     -- Run the computation
1062
       ; res <- unTcS tcs env
1063
1064
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
1065
       ; mapM_ do_unification (varEnvElts ty_binds)
1066

1067
1068
1069
1070
1071
#ifdef DEBUG
       ; count <- TcM.readTcRef step_count
       ; when (opt_PprStyle_Debug && count > 0) $
         TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count )

1072
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1073
       ; checkForCyclicBinds ev_binds
1074
1075
#endif

1076
       ; return res }
1077
1078
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
1079
1080
    is = emptyInert
    
1081
#ifdef DEBUG
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
checkForCyclicBinds :: Bag EvBind -> TcM ()
checkForCyclicBinds ev_binds
  | null cycles 
  = return ()
  | null coercion_cycles
  = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
  | otherwise
  = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
  where
    cycles :: [[EvBind]]
    cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]

    coercion_cycles = [c | c <- cycles, any is_co_bind c]
    is_co_bind (EvBind b _) = isEqVar b

    edges :: [(EvBind, EvVar, [EvVar])]
    edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
#endif       
1100

1101
1102
nestImplicTcS :: EvBindsVar -> Untouchables -> InertSet -> TcS a -> TcS a 
nestImplicTcS ref inner_untch inerts (TcS thing_inside) 
1103
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
1104
                   , tcs_count = count } -> 
1105
    do { new_inert_var <- TcM.newTcRef inerts
1106
1107
1108
1109
       ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                               , tcs_ty_binds    = ty_binds
                               , tcs_count       = count
                               , tcs_inerts      = new_inert_var
1110
1111
1112
                               , tcs_worklist    = panic "nextImplicTcS: worklist"
                               , tcs_implics     = panic "nextImplicTcS: implics"
                               -- NB: Both these are initialised by withWorkList
1113
                               }
1114
1115
       ; res <- TcM.setUntouchables inner_untch $
                thing_inside nest_env
1116
                
1117
#ifdef DEBUG
1118
1119
1120
       -- Perform a check that the thing_inside did not cause cycles
       ; ev_binds <- TcM.getTcEvBinds ref
       ; checkForCyclicBinds ev_binds
1121
#endif
1122
1123
         
       ; return res }
1124

1125
1126
1127
1128
1129
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
nestTcS ::  TcS a -> TcS a 
-- Use the current untouchables, augmenting the current
-- evidence bindings, ty_binds, and solved caches
-- But have no effect on the InertCans or insolubles
nestTcS (TcS thing_inside) 
  = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
    do { inerts <- TcM.readTcRef inerts_var
       ; new_inert_var <- TcM.newTcRef inerts
       ; let nest_env = env { tcs_inerts   = new_inert_var
                            , tcs_worklist = panic "nextImplicTcS: worklist"
                            , tcs_implics  = panic "nextImplicTcS: implics" }
       ; thing_inside nest_env }

1143
tryTcS :: TcS a -> TcS a
1144
1145
1146
-- Like runTcS, but from within the TcS monad 
-- Completely afresh inerts and worklist, be careful! 
-- Moreover, we will simply throw away all the evidence generated. 
1147
1148
1149
1150
1151
tryTcS (TcS thing_inside)
  = TcS $ \env -> 
    do { is_var <- TcM.newTcRef emptyInert
       ; ty_binds_var <- TcM.newTcRef emptyVarEnv
       ; ev_binds_var <- TcM.newTcEvBinds
1152

1153
1154
1155
1156
1157
1158
       ; let nest_env = env { tcs_ev_binds = ev_binds_var
                            , tcs_ty_binds = ty_binds_var
                            , tcs_inerts   = is_var
                            , tcs_worklist = panic "nextImplicTcS: worklist"
                            , tcs_implics  = panic "nextImplicTcS: implics" }
       ; thing_inside nest_env }
1159
1160

-- Getters and setters of TcEnv fields
1161
1162
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1163
1164
1165
1166
1167
1168
-- Getter of inerts and worklist
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = TcS (return . tcs_inerts)

getTcSWorkListRef :: TcS (IORef WorkList) 
getTcSWorkListRef = TcS (return . tcs_worklist) 
1169

1170
1171
1172
1173
1174
getTcSInerts :: TcS InertSet 
getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) 

updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
updWorkListTcS f 
1175
1176
1177
1178
  = do { wl_var <- getTcSWorkListRef
       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
       ; let new_work = f wl_curr
       ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1179
1180

updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1181
1182
-- Process the work list, returning a depleted work list,
-- plus a value extracted from it (typically a work item removed from it)
1183
1184
1185
1186
1187
1188
updWorkListTcS_return f
  = do { wl_var <- getTcSWorkListRef
       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
       ; let (res,new_work) = f wl_curr
       ; wrapTcS (TcM.writeTcRef wl_var new_work)
       ; return res }
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205

withWorkList :: Cts -> TcS () -> TcS (Bag Implication)
-- Use 'thing_inside' to solve 'work_items', extending the
-- ambient InertSet, and returning any residual implications
-- (arising from polytype equalities)
-- We do this with fresh work list and residual-implications variables
withWorkList work_items (TcS thing_inside)
  = TcS $ \ tcs_env ->
    do { let init_work_list = foldrBag extendWorkListCt emptyWorkList work_items
       ; new_wl_var <- TcM.newTcRef init_work_list
       ; new_implics_var <- TcM.newTcRef emptyBag
       ; thing_inside (tcs_env { tcs_worklist = new_wl_var
                               , tcs_implics = new_implics_var })
       ; final_wl <- TcM.readTcRef new_wl_var
       ; implics  <- TcM.readTcRef new_implics_var
       ; ASSERT( isEmptyWorkList final_wl )
         return implics }
1206
1207
1208
1209

updTcSImplics :: (Bag Implication -> Bag Implication) -> TcS ()
updTcSImplics f 
 = do { impl_ref <- getTcSImplicsRef
1210
1211
      ; wrapTcS $ do { implics <- TcM.readTcRef impl_ref
                     ; TcM.writeTcRef impl_ref (f implics) } }
1212

1213
emitInsoluble :: Ct -> TcS ()
1214
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
1215
1216
emitInsoluble ct
  = do { traceTcS "Emit insoluble" (ppr ct)
1217
1218
       ; updInertTcS add_insol }
  where
1219
    this_pred = ctPred ct
1220
1221
    add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
      | already_there = is