TcSMonad.lhs 64.5 KB
Newer Older
1
\begin{code}
2
{-# OPTIONS -fno-warn-tabs #-}
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
16
    WorkList(..), isEmptyWorkList, emptyWorkList,
    workListFromEq, workListFromNonEq, workListFromCt, 
    extendWorkListEq, extendWorkListNonEq, extendWorkListCt, 
dimitris's avatar
dimitris committed
17
    appendWorkListCt, appendWorkListEqs, unionWorkList, selectWorkItem,
18
    withWorkList,
19

20
    getTcSWorkList, updWorkListTcS, updWorkListTcS_return,
21
22
    
    getTcSImplics, updTcSImplics, emitTcSImplication, 
23

24
    Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, 
25
    emitFrozenError,
26

27
28
    isWanted, isDerived, 
    isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
29

30
    canRewrite, canSolve,
31
    mkGivenLoc, ctWantedLoc,
32

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

dimitris's avatar
dimitris committed
38
    -- Getting and setting the flattening cache
39
    getFlatCache, updFlatCache, addToSolved, addSolvedFunEq, getFlattenSkols,
dimitris's avatar
dimitris committed
40
    
41
    deferTcSForAllEq, 
dimitris's avatar
dimitris committed
42
43
44
    
    setEvBind,
    XEvTerm(..),
45
46
47
    MaybeNew (..), isFresh, freshGoals, getEvTerms,

    xCtFlavor, -- Transform a CtEvidence during a step 
dimitris's avatar
dimitris committed
48
    rewriteCtFlavor,          -- Specialized version of xCtFlavor for coercions
49
    newWantedEvVar, instDFunConstraints,
dimitris's avatar
dimitris committed
50
51
52
    newDerived,
    xCtFlavor_cache, rewriteCtFlavor_cache,
    
53
       -- Creation of evidence variables
54
55
    setWantedTyBind,

56
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
57
    getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
58
    getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
59

60
61

    newFlattenSkolemTy,                         -- Flatten skolems 
62

63
        -- Inerts 
dimitris's avatar
dimitris committed
64
    InertSet(..), InertCans(..), 
65
66
67
68
    getInertEqs, 
    emptyInert, getTcSInerts, lookupInInerts, lookupFlatEqn,
    getInertUnsolved, checkAllSolved, 
    prepareInertsForImplications,
69
    modifyInertTcS,
70
    insertInertItemTcS, partitionCCanMap, partitionEqMap,
71
    getRelevantCts, extractRelevantInerts,
72
73
74
    CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
    PredMap, FamHeadMap,
    partCtFamHeadMap, lookupFamHead,
75
    filterSolved,
76

77
    instDFunType,                              -- Instantiation
78
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
79
    cloneMetaTyVar,
80

81
    compatKind, mkKindErrorCtxtTcS,
82

83
    Untouchables, isTouchableMetaTyVarTcS,
84
85
86
87
88
89

    getDefaultInfo, getDynFlags,

    matchClass, matchFam, MatchInstResult (..), 
    checkWellStagedDFun, 
    warnTcS,
90
    pprEq                                    -- Smaller utils, re-exported from TcM
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
                                             -- 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 
109
       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
110
import {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
111
import Kind
112
113
import TcType
import DynFlags
114
import Type
115

116
import TcEvidence
117
118
import Class
import TyCon
119

120
121
import Name
import Var
122
import VarEnv
123
124
125
import Outputable
import Bag
import MonadUtils
126

127
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
128
import Util
129
import Id 
Ian Lynagh's avatar
Ian Lynagh committed
130
import TcRnTypes
131

132
133
import Unique 
import UniqFM
134
import Maybes ( orElse, catMaybes, firstJust )
135

136
import Control.Monad( unless, when, zipWithM )
Ian Lynagh's avatar
Ian Lynagh committed
137
import Data.IORef
138
import TrieMap
139

140
141
142
143
144
#ifdef DEBUG
import StaticFlags( opt_PprStyle_Debug )
import VarSet
import Digraph
#endif
145
\end{code}
146

147

148
\begin{code}
149
compatKind :: Kind -> Kind -> Bool
Simon Peyton Jones's avatar
Simon Peyton Jones committed
150
compatKind k1 k2 = k1 `tcIsSubKind` k2 || k2 `tcIsSubKind` k1 
151

152
153
154
155
156
157
mkKindErrorCtxtTcS :: Type -> Kind 
                   -> Type -> Kind 
                   -> ErrCtxt
mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
  = (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)

158
159
\end{code}

160
161
162
163
164
165
166
167
%************************************************************************
%*									*
%*                            Worklists                                *
%*  Canonical and non-canonical constraints that the simplifier has to  *
%*  work on. Including their simplification depths.                     *
%*                                                                      *
%*									*
%************************************************************************
168

169
170
171
172
173
Note [WorkList]
~~~~~~~~~~~~~~~
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. 
174

175
176
177
178
179
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. 
180

181
182
183
184
185
186
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. 
187

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

191
192
193
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)
194

195
\begin{code}
196

197
-- See Note [WorkList]
198
199
200
201
data WorkList = WorkList { wl_eqs    :: [Ct]
                         , wl_funeqs :: [Ct]
                         , wl_rest   :: [Ct] 
                         }
202

batterseapower's avatar
batterseapower committed
203

204
205
unionWorkList :: WorkList -> WorkList -> WorkList
unionWorkList new_wl orig_wl = 
dimitris's avatar
dimitris committed
206
207
208
   WorkList { wl_eqs    = wl_eqs new_wl ++ wl_eqs orig_wl
            , wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl
            , wl_rest   = wl_rest new_wl ++ wl_rest orig_wl }
209

210

211
212
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
dimitris's avatar
dimitris committed
213
214
215
216
217
extendWorkListEq ct wl 
  | Just {} <- isCFunEqCan_Maybe ct
  = wl { wl_funeqs = ct : wl_funeqs wl }
  | otherwise
  = wl { wl_eqs = ct : wl_eqs wl }
218

219
220
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
221
222
extendWorkListNonEq ct wl 
  = wl { wl_rest = ct : wl_rest wl }
223

224
225
226
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
dimitris's avatar
dimitris committed
227
 | isEqPred (ctPred ct) = extendWorkListEq ct wl
228
 | otherwise = extendWorkListNonEq ct wl
229

230
231
232
appendWorkListCt :: [Ct] -> WorkList -> WorkList
-- Agnostic
appendWorkListCt cts wl = foldr extendWorkListCt wl cts
233

234
235
236
appendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
appendWorkListEqs cts wl = foldr extendWorkListEq wl cts
237
238

isEmptyWorkList :: WorkList -> Bool
dimitris's avatar
dimitris committed
239
240
isEmptyWorkList wl 
  = null (wl_eqs wl) &&  null (wl_rest wl) && null (wl_funeqs wl)
241
242

emptyWorkList :: WorkList
243
emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = [] }
244

245
workListFromEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
246
workListFromEq ct = extendWorkListEq ct emptyWorkList
247

248
workListFromNonEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
249
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
250

251
252
workListFromCt :: Ct -> WorkList
-- Agnostic 
dimitris's avatar
dimitris committed
253
254
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct 
                  | otherwise            = workListFromNonEq ct
255

dimitris's avatar
dimitris committed
256
257
258
259
260
261
262
263
264

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 })
      (_,(ct:cts),_)   -> (Just ct, wl { wl_funeqs = cts })
      (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
      (_,_,_)          -> (Nothing,wl)

265
266
267
-- Pretty printing 
instance Outputable WorkList where 
  ppr wl = vcat [ text "WorkList (eqs)   = " <+> ppr (wl_eqs wl)
dimitris's avatar
dimitris committed
268
                , text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
269
270
                , text "WorkList (rest)  = " <+> ppr (wl_rest wl)
                ]
271
272


dimitris's avatar
dimitris committed
273
-- Canonical constraint maps
274
275
276
277
278
279
280
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 }
281
282
283
284
285
286
287
288
289
290
291

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 
292
  = case cc_ev ct of 
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
      Wanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
      Given {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
      Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
  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

312
313
314
315
316
317
318
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))
319

320
321
322
323
324
325
326
327
328
329
     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
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344

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

345
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
346
347
348
349
350
351
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

352
353
354
355
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)
356

dimitris's avatar
dimitris committed
357
-- Maps from PredTypes to Constraints
358
359
360
361
362
363
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
364

365
366
367
368
369
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 [])
370
371
372
373

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

374
375
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
dimitris's avatar
dimitris committed
376

377
378
379
380
381
382
383
384
385
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
386
387
388
389
390
partCtFamHeadMap :: (Ct -> Bool) 
                 -> CtFamHeadMap 
                 -> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
  = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
391
    in (cts, FamHeadMap tymap_final)
dimitris's avatar
dimitris committed
392
  where
393
    tymap_inside = unFamHeadMap ctmap 
dimitris's avatar
dimitris committed
394
    upd_acc ct (cts,acc_map)
395
396
         | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
         | otherwise = (cts,acc_map)
dimitris's avatar
dimitris committed
397
398
399
400
         where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
                      = ty1 
                      | otherwise 
                      = panic "partCtFamHeadMap, encountered non equality!"
401
402
403
404
405

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
406
407
408
409
410
411
412
413
414
415
\end{code}

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

\begin{code}
416
-- All Given (fully known) or Wanted or Derived
dimitris's avatar
dimitris committed
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
442
443
444
-- 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_eq_tvs :: InScopeSet
              -- Superset of the type variables of inert_eqs
       , 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
       }
    
                     
\end{code}

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
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
  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)

  8 Equalities _do_not_ form an idempotent substitution but they are guarranteed 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.

       - In the past we did try to have the inert substituion as 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. 
         
         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. 

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

478
479
480
481
482
483
484
485
486
487
488
489
490
491
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

492
493
494
495
* 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
496

497
498

\begin{code}
dimitris's avatar
dimitris committed
499
500
501
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
502
503
504
              -- Canonical Given, Wanted, Derived (no Solved)
	      -- Sometimes called "the inert set"

dimitris's avatar
dimitris committed
505
506
507
508
       , inert_frozen :: Cts       
              -- Frozen errors (as non-canonicals)
                               
       , inert_flat_cache :: CtFamHeadMap 
509
510
       , inert_fsks :: [TcTyVar]  -- Flatten-skolems allocated in this local scope
                                  -- Subset of inert_flat_cacha
dimitris's avatar
dimitris committed
511
512
              -- All ``flattening equations'' are kept here. 
              -- Always canonical CTyFunEqs (Given or Wanted only!)
513
514
515
              -- Key is by family head. We use this field during flattening only
              -- Not necessarily inert wrt top-level equations (or inert_cans)

516
517
518
519
       , inert_solved_funeqs :: CtFamHeadMap  
              -- Of form co :: F xis ~ xi 
              -- Always the result of using a top-level family axiom F xis ~ tau
              -- No Deriveds 
520

521
       , inert_solved        :: PredMap CtEvidence 
522
523
       	      -- These two fields constitute a cache of solved (only!) constraints
              -- See Note [Solved constraints]
524
       	      -- - Superset of inert_solved_funeqs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
525
       	      -- - Used to avoid creating a new EvVar when we have a new goal that we
526
       	      --   have solvedin the past
Simon Peyton Jones's avatar
Simon Peyton Jones committed
527
       	      -- - Stored not necessarily as fully rewritten 
528
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
529
       }
530
531


dimitris's avatar
dimitris committed
532
instance Outputable InertCans where 
533
534
535
536
  ppr ics = vcat [ ptext (sLit "Equalities:") 
                   <+> vcat (map ppr (varEnvElts (inert_eqs ics)))
                 , ptext (sLit "Type-function equalities:")
                   <+> vcat (map ppr (Bag.bagToList $ 
537
                                  ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
538
539
540
541
                 , ptext (sLit "Dictionaries:")
                   <+> vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
                 , ptext (sLit "Irreds:")
                   <+> vcat (map ppr (Bag.bagToList $ inert_irreds ics))
dimitris's avatar
dimitris committed
542
543
544
545
                 ]
            
instance Outputable InertSet where 
  ppr is = vcat [ ppr $ inert_cans is
546
547
                , text "Frozen errors =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
dimitris's avatar
dimitris committed
548
549
                , text "Solved and cached" <+>
                    int (foldTypeMap (\_ x -> x+1) 0 
550
                             (unPredMap $ inert_solved is)) <+> 
dimitris's avatar
dimitris committed
551
                    text "more constraints" ]
552

dimitris's avatar
dimitris committed
553
554
555
556
557
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                         , inert_eq_tvs = emptyInScopeSet
                         , inert_dicts  = emptyCCanMap
558
                         , inert_funeqs = FamHeadMap emptyTM 
dimitris's avatar
dimitris committed
559
560
                         , inert_irreds = emptyCts }
       , inert_frozen        = emptyCts
561
       , inert_flat_cache    = FamHeadMap emptyTM
562
       , inert_fsks          = []
563
564
       , inert_solved        = PredMap emptyTM 
       , inert_solved_funeqs = FamHeadMap emptyTM }
565

566
567
updSolvedSet :: CtEvidence -> InertSet -> InertSet 
updSolvedSet item is
568
  = let pty = ctEvPred item
dimitris's avatar
dimitris committed
569
570
571
572
        upd_solved Nothing = Just item
        upd_solved (Just _existing_solved) = Just item 
               -- .. or Just existing_solved? Is this even possible to happen?
    in is { inert_solved = 
573
574
575
               PredMap $ 
               alterTM pty upd_solved (unPredMap $ inert_solved is) }

dimitris's avatar
dimitris committed
576

577
insertInertItem :: Ct -> InertSet -> InertSet 
578
-- Add a new inert element to the inert set. 
579
insertInertItem item is
dimitris's avatar
dimitris committed
580
581
582
  | isCNonCanonical item 
    -- NB: this may happen if we decide to kick some frozen error 
    -- out to rewrite him. Frozen errors are just NonCanonicals
583
  = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
dimitris's avatar
dimitris committed
584
585
586
587
588
    
  | otherwise  
    -- A canonical Given, Wanted, or Derived
  = is { inert_cans = upd_inert_cans (inert_cans is) item }
  
589
  where upd_inert_cans :: InertCans -> Ct -> InertCans
dimitris's avatar
dimitris committed
590
591
592
        -- Precondition: item /is/ canonical
        upd_inert_cans ics item
          | isCTyEqCan item                     
593
          = let upd_err a b = pprPanic "insertInertItem" $
dimitris's avatar
dimitris committed
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
                              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        
                inscope' = extendInScopeSetSet (inert_eq_tvs ics)
                                               (tyVarsOfCt item)
                
            in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }

          | 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) 
615
                  = panic "insertInertItem: item already there!"
616
            in ics { inert_funeqs = FamHeadMap 
dimitris's avatar
dimitris committed
617
                                      (alterTM fam_head upd_funeqs $ 
618
                                         (unFamHeadMap $ inert_funeqs ics)) }
dimitris's avatar
dimitris committed
619
620
621
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
            ppr item 
622

623
insertInertItemTcS :: Ct -> TcS ()
624
-- Add a new item in the inerts of the monad
625
626
insertInertItemTcS item
  = do { traceTcS "insertInertItemTcS {" $ 
627
628
         text "Trying to insert new inert item:" <+> ppr item

629
       ; updInertTcS (insertInertItem item) 
630
                        
631
       ; traceTcS "insertInertItemTcS }" $ empty }
632

633
634
635
636
637
638
639
640
641
addToSolved :: CtEvidence -> TcS ()
-- Add a new item in the solved set of the monad
addToSolved item
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
  = return () 
  | otherwise
  = do { traceTcS "updSolvedSetTcs {" $ 
         text "Trying to insert new solved item:" <+> ppr item

642
       ; updInertTcS (updSolvedSet item)
643
644
645
                        
       ; traceTcS "updSolvedSetTcs }" $ empty }

646
647
648
649
650
addSolvedFunEq :: Ct -> TcType -> TcS ()
addSolvedFunEq fun_eq fam_ty
  = updInertTcS (upd_solved_funeqs . upd_solved)
    -- Update both inert_solved and inert_solved_funeqs
    -- The former is a superset of the latter
651
  where 
652
653
654
    upd_solved = updSolvedSet (cc_ev fun_eq)  
    upd_solved_funeqs inert 
      = inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) fam_ty fun_eq }
655

656
657
658
659
660
661
662
663
664
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 }

665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
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
  = is { inert_cans = getGivens (inert_cans is)
       , inert_fsks = []
       , inert_frozen = emptyCts }
  where
    getGivens (IC { inert_eq_tvs = eq_tvs
                  , inert_eqs    = eqs
                  , inert_irreds = irreds
                  , inert_funeqs = FamHeadMap funeqs
                  , inert_dicts  = dicts })
      = IC { inert_eq_tvs = eq_tvs
           , inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
           , inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
           , inert_irreds = Bag.filterBag isGivenCt irreds
           , inert_dicts  = keepGivenCMap dicts }

    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
        given_ev = Given { ctev_gloc = setCtLocOrigin (ctev_wloc ev) UnkSkol
                         , ctev_evtm = EvId (ctev_evar ev)
                         , ctev_pred = ctev_pred ev }
\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
707

708
709
710
711
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
712

713
714
715
716
717
718
719
720
721
722
   [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.  
723

724
725
Turning type-function equalities into Givens is easy becase they 
*stay inert*.  No need to re-process them.
726

727
We don't try to turn any *other* Wanteds into Givens:
728

729
730
731
  * 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.
732

733
734
There might be cases where interactions between wanteds can help
to solve a constraint. For example
735

736
737
  	class C a b | a -> b
  	(C Int alpha), (forall d. C d blah => C Int a)
738

739
740
741
742
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.
743
744


745
746
747
748
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
789
\begin{code}
getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
getInertEqs = do { inert <- getTcSInerts
                 ; let ics = inert_cans inert
                 ; return (inert_eqs ics, inert_eq_tvs ics) }

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

      ; return (unsolved_flats, inert_frozen is) }
  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
                     || not (isEmptyBag (inert_frozen is)))) }

790
791
792
793
794
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
795
796
797
798
799
800
801
802
  = modifyInertTcS (extract_relevants wi)
  where extract_relevants wi is 
          = let (cts,ics') = extract_ics_relevants wi (inert_cans is)
            in (cts, is { inert_cans = ics' }) 
            
        extract_ics_relevants (CDictCan {cc_class = cl}) ics = 
            let (cts,dict_map) = getRelevantCts cl (inert_dicts ics) 
            in (cts, ics { inert_dicts = dict_map })
803
804
805
806
807
808
809
810
811

        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)

dimitris's avatar
dimitris committed
812
813
814
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
815

dimitris's avatar
dimitris committed
816
817
818
        extract_ics_relevants _ ics = (emptyCts,ics)
        

819
820
821
822
823
824
825
826
827
828
lookupFlatEqn :: TcType -> TcS (Maybe Ct)
lookupFlatEqn fam_ty 
  = do { IS { inert_solved_funeqs = solved_funeqs
            , inert_flat_cache = flat_cache
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
       ; return (lookupFamHead solved_funeqs fam_ty `firstJust`
                 lookupFamHead inert_funeqs fam_ty  `firstJust`
                 lookupFamHead flat_cache   fam_ty) }

lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
dimitris's avatar
dimitris committed
829
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
830
831
832
833
834
lookupInInerts pty
  = do { IS { inert_solved = solved, inert_cans = ics } <- getTcSInerts
       ; case lookupInSolved solved pty of
           Just ctev -> return (Just ctev)
           Nothing   -> return (lookupInInertCans ics pty) }
dimitris's avatar
dimitris committed
835

836
lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
837
-- Returns just if exactly this predicate type exists in the solved.
838
lookupInSolved tm pty = lookupTM pty $ unPredMap tm
dimitris's avatar
dimitris committed
839

840
lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
841
842
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans ics pty
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
  = 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)
    
      _other -> Nothing -- NB: No caching for IPs
863
864
\end{code}

865

dimitris's avatar
dimitris committed
866
867


868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
%************************************************************************
%*									*
%*		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 { 
890
      tcs_ev_binds    :: EvBindsVar,
dimitris's avatar
dimitris committed
891
      
892
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
893
          -- Global type bindings
894
                     
dimitris's avatar
dimitris committed
895
896
897
      tcs_ic_depth   :: Int,       -- Implication nesting depth
      tcs_count      :: IORef Int, -- Global step count

898
      tcs_inerts   :: IORef InertSet, -- Current inert set
899
900
901
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
902
903
904
      -- 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)
905
      tcs_implics  :: IORef (Bag Implication)
906
    }
907
908
909
\end{code}

\begin{code}
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944

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

947
948
949
950
951
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

952
traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
953
954
955
956
957
958
959
960
961
-- 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 }
962

963
964
965
966
967
968
969
970
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) }

971
972
973
974
runTcSWithEvBinds :: EvBindsVar
                  -> TcS a 
                  -> TcM a
runTcSWithEvBinds ev_binds_var tcs
975
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
976
       ; step_count <- TcM.newTcRef 0
977
978
       ; inert_var <- TcM.newTcRef is 

979
980
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
981
982
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
983
                          , tcs_inerts   = inert_var
984
985
986
                          , tcs_worklist    = panic "runTcS: worklist"
                          , tcs_implics     = panic "runTcS: implics" }
                               -- NB: Both these are initialised by withWorkList
987
988

	     -- Run the computation
989
       ; res <- unTcS tcs env
990
991
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
992
       ; mapM_ do_unification (varEnvElts ty_binds)
993

994
995
996
997
998
#ifdef DEBUG
       ; count <- TcM.readTcRef step_count
       ; when (opt_PprStyle_Debug && count > 0) $
         TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count )

999
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1000
       ; checkForCyclicBinds ev_binds
1001
1002
#endif

1003
       ; return res }
1004
1005
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
1006
1007
    is = emptyInert
    
1008
#ifdef DEBUG
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
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       
1027

1028
1029
nestImplicTcS :: EvBindsVar -> Untouchables -> InertSet -> TcS a -> TcS a 
nestImplicTcS ref inner_untch inerts (TcS thing_inside) 
1030
1031
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
                   , tcs_count = count
1032
1033
                   , tcs_ic_depth = idepth } -> 
    do { new_inert_var <- TcM.newTcRef inerts
1034
1035
1036
1037
1038
       ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                               , tcs_ty_binds    = ty_binds
                               , tcs_count       = count
                               , tcs_ic_depth    = idepth+1
                               , tcs_inerts      = new_inert_var
1039
1040
1041
                               , tcs_worklist    = panic "nextImplicTcS: worklist"
                               , tcs_implics     = panic "nextImplicTcS: implics"
                               -- NB: Both these are initialised by withWorkList
1042
                               }
1043
1044
       ; res <- TcM.setUntouchables inner_untch $
                thing_inside nest_env
1045
                
1046
#ifdef DEBUG
1047
1048
1049
       -- Perform a check that the thing_inside did not cause cycles
       ; ev_binds <- TcM.getTcEvBinds ref
       ; checkForCyclicBinds ev_binds
1050
#endif
1051
1052
         
       ; return res }
1053

1054
1055
1056
1057
1058
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

1059
tryTcS :: TcS a -> TcS a
1060
1061
1062
-- 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. 
dimitris's avatar
dimitris committed
1063
tryTcS tcs
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
  = TcS (\env -> 
             do { wl_var <- TcM.newTcRef emptyWorkList
                ; is_var <- TcM.newTcRef emptyInert

                ; ty_binds_var <- TcM.newTcRef emptyVarEnv
                ; ev_binds_var <- TcM.newTcEvBinds

                ; let env1 = env { tcs_ev_binds = ev_binds_var
                                 , tcs_ty_binds = ty_binds_var
                                 , tcs_inerts   = is_var
                                 , tcs_worklist = wl_var } 
                ; unTcS tcs env1 })

-- Getters and setters of TcEnv fields
1078
1079
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1080
1081
1082
1083
1084
1085
1086
1087
1088
-- Getter of inerts and worklist
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = TcS (return . tcs_inerts)

getTcSWorkListRef :: TcS (IORef WorkList) 
getTcSWorkListRef = TcS (return . tcs_worklist) 
getTcSInerts :: TcS InertSet 
getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) 

1089
1090
1091
1092
1093
1094
1095

getTcSImplicsRef :: TcS (IORef (Bag Implication))
getTcSImplicsRef = TcS (return . tcs_implics) 

getTcSImplics :: TcS (Bag Implication)
getTcSImplics = getTcSImplicsRef >>= wrapTcS . (TcM.readTcRef)

1096
1097
1098
1099
1100
getTcSWorkList :: TcS WorkList
getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 

updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
updWorkListTcS f 
1101
1102
1103
1104
  = do { wl_var <- getTcSWorkListRef
       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
       ; let new_work = f wl_curr
       ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1105
1106

updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1107
1108
-- Process the work list, returning a depleted work list,
-- plus a value extracted from it (typically a work item removed from it)
1109
1110
1111
1112
1113
1114
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 }
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131

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 }
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142

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

emitTcSImplication :: Implication -> TcS ()
emitTcSImplication imp = updTcSImplics (consBag imp)

1143

1144
emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
1145
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
dimitris's avatar
dimitris committed
1146
emitFrozenError fl depth 
1147
  = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
1148
       ; inert_ref <- getTcSInertsRef 
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
       ; wrapTcS $ do
       { inerts <- TcM.readTcRef inert_ref
       ; let old_insols = inert_frozen inerts
             ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
             inerts_new = inerts { inert_frozen = extendCts old_insols ct } 
             this_pred = ctEvPred fl
             already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
	     -- See Note [Do not add duplicate derived insolubles]
       ; unless already_there $
         TcM.writeTcRef inert_ref inerts_new } }
1159

1160
instance HasDynFlags TcS where
1161
    getDynFlags = wrapTcS getDynFlags
1162
1163
1164
1165
1166


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

dimitris's avatar
dimitris committed
1167
getFlatCache :: TcS CtTypeMap 
1168
getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
dimitris's avatar
dimitris committed
1169
1170
1171

updFlatCache :: Ct -> TcS ()
-- Pre: constraint is a flat family equation (equal to a flatten skolem)
1172
updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis })
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
  = updInertTcS upd_inert_cache
  where 
    upd_inert_cache is = is { inert_flat_cache = FamHeadMap new_fc }
                       where new_fc = alterTM pred_key upd_cache fc
                             fc = unFamHeadMap $ inert_flat_cache is
    pred_key = mkTyConApp tc xis
    upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct 
    upd_cache (Just _ct) = Just flat_eq 
    upd_cache Nothing    = Just flat_eq

dimitris's avatar
dimitris committed
1183
1184
1185
updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
                        ppr other_ct
                        
1186
1187
getUntouchables :: TcS Untouchables
getUntouchables = wrapTcS TcM.getUntouchables
1188

1189
1190
getFlattenSkols :: TcS [TcTyVar]
getFlattenSkols = do { is <- getTcSInerts; return (inert_fsks is) }
1191

1192
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1193
1194
getTcSTyBinds = TcS (return . tcs_ty_binds)

1195
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1196
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1197

1198
1199
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
1200
1201
1202
1203
1204
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
1205
-- We never do this twice!
1206
1207
1208
1209
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
Ian Lynagh's avatar
Ian Lynagh committed
1210
1211
1212
1213
1214
            ; when debugIsOn $
                  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)]
1215
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1216
1217
1218
\end{code}

\begin{code}
1219
1220
1221
1222
1223
warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
warnTcS loc warn_if doc 
  | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
  | otherwise = return ()

1224
1225
getDefaultInfo ::  TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254

-- 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
1255
pprEq ty1 ty2 = pprType $ mkEqPred ty1 ty2
1256

1257
1258
isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
isTouchableMetaTyVarTcS tv 
1259
  = do { untch <- getUntouchables
1260
       ; return $ isTouchableMetaTyVar untch tv } 
1261
1262
\end{code}

1263
1264
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1265
In general we *do* want to add an insoluble (Int ~ Bool) even if there is one
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
such there already, because they may come from distinct call sites.  But for
*derived* insolubles, we only want to report each one once.  Why?

(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
    equality many times, as the original constraint is sucessively rewritten.

(b) Ditto the successive iterations of the main solver itself, as it traverses
    the constraint tree. See example below.

Also for *given* insolubles we may get repeated errors, as we
repeatedly traverse the constraint tree.  These are relatively rare
anyway, so removing duplicates seems ok.  (Alternatively we could take
the SrcLoc into account.)

Note that the test does not need to be particularly efficient because
it is only used if the program has a type error anyway.

Example of (b): assume a top-level class and instance declaration:

  class D a b | a -> b 
  instance D [a] [a] 

Assume we have started with an implication:

  forall c. Eq c => { wc_flat = D [c] c [W] }

which we have simplified to:

  forall c. Eq c => { wc_flat = D [c] c [W]
                    , wc_insols = (c ~ [c]) [D] }

For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
1299
dropDerivedWC, then we will end up trying to solve the following
1300
1301
1302
1303
1304
1305
1306
1307
1308
constraints the second time:

  (D [c] c) [W]
  (c ~ [c]) [D]

which will result in two Deriveds to end up in the insoluble set:

  wc_flat   = D [c] c [W]
  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
1309

1310
1311


1312
\begin{code}
1313
1314
1315
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newFlattenSkolemTy :: TcType -> TcS TcType
1316
newFlattenSkolemTy fam_ty
dimitris's avatar
dimitris committed
1317
1318
1319
  = do { tv <- wrapTcS $ 
               do { uniq <- TcM.newUnique
                  ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
1320
                  ; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) } 
dimitris's avatar
dimitris committed
1321
       ; traceTcS "New Flatten Skolem Born" $
1322
1323
1324
1325
1326
1327
         ppr tv <+> text "[:= " <+> ppr fam_ty <+> text "]"
       ; updInertTcS (add_fsk tv)
       ; return (mkTyVarTy tv) }
  where
    add_fsk :: TcTyVar -> InertSet -> InertSet
    add_fsk tv is = is { inert_fsks = tv : inert_fsks is }
1328
1329
1330
1331

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

1332
1333
1334
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
instDFunType dfun_id mb_inst_tys 
  = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
1335
  where
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
    (dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)

    go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
    go [] [] subst = return ([], substTy subst dfun_phi)
    go (tv:tvs) (Just ty : mb_tys) subst
      = do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
           ; return (ty : tys, phi) }
    go (tv:tvs) (Nothing : mb_tys) subst
      = do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
                         -- Don't forget to instantiate the kind!
                         -- cf TcMType.tcInstTyVarX
           ; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
           ; return (ty : tys, phi) }
    go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)

1351
1352
1353
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)

1354
1355
1356
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)

1357
1358
1359
instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
  where
1360
1361
1362
1363
     inst_one subst tv 
         = do { ty' <- instFlexiTcSHelper (tyVarName tv) 
                                          (substTy subst (tyVarKind tv))
              ; return (extendTvSubst subst tv ty', ty') }