TcSMonad.lhs 66.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

19
    getTcSWorkList, updWorkListTcS, updWorkListTcS_return, keepWanted,
20
    getTcSWorkListTvs, 
21
22
    
    getTcSImplics, updTcSImplics, emitTcSImplication, 
23
24
25

    Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, 
    emitFrozenError,
26

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

30
31
    isFlexiTcsTv,

32
    canRewrite, canSolve,
33
    mkGivenLoc, ctWantedLoc,
34

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

40
    SimplContext(..), isInteractive, performDefaulting,
41

dimitris's avatar
dimitris committed
42
    -- Getting and setting the flattening cache
43
    getFlatCache, updFlatCache, addToSolved, addSolvedFunEq,
dimitris's avatar
dimitris committed
44
    
45
    deferTcSForAllEq, 
dimitris's avatar
dimitris committed
46
47
48
    
    setEvBind,
    XEvTerm(..),
49
50
51
    MaybeNew (..), isFresh, freshGoals, getEvTerms,

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

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

64
65

    newFlattenSkolemTy,                         -- Flatten skolems 
66

67
        -- Inerts 
dimitris's avatar
dimitris committed
68
    InertSet(..), InertCans(..), 
69
    getInertEqs, getCtCoercion,
70
71
    emptyInert, getTcSInerts, lookupInInerts, 
    extractUnsolved,
72
73
74
    extractUnsolvedTcS, modifyInertTcS,
    updInertSetTcS, partitionCCanMap, partitionEqMap,
    getRelevantCts, extractRelevantInerts,
75
76
77
    CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
    PredMap, FamHeadMap,
    partCtFamHeadMap, lookupFamHead,
78

79

80
    instDFunType,                              -- Instantiation
81
    newFlexiTcSTy, instFlexiTcS,
82

83
    compatKind, mkKindErrorCtxtTcS,
84

85
    TcsUntouchables,
86
    isTouchableMetaTyVar,
87
    isTouchableMetaTyVar_InRange, 
88
89
90
91
92
93

    getDefaultInfo, getDynFlags,

    matchClass, matchFam, MatchInstResult (..), 
    checkWellStagedDFun, 
    warnTcS,
94
    pprEq                                    -- Smaller utils, re-exported from TcM
95
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 BasicTypes 

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 {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
116
import Kind
117
118
import TcType
import DynFlags
119
import Type
120

121
import TcEvidence
122
123
import Class
import TyCon
124

125
126
import Name
import Var
127
import VarEnv
128
129
130
131
import Outputable
import Bag
import MonadUtils
import VarSet
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 )
141

142

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

148
\end{code}
149

150

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

155
156
157
158
159
160
mkKindErrorCtxtTcS :: Type -> Kind 
                   -> Type -> Kind 
                   -> ErrCtxt
mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
  = (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)

161
162
\end{code}

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

172
173
Note [WorkList]
~~~~~~~~~~~~~~~
174

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

179
180
181
182
183
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. 
184

185
186
187
188
189
190
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. 
191

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

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

199
\begin{code}
200

201
-- See Note [WorkList]
202
203
204
205
data WorkList = WorkList { wl_eqs    :: [Ct]
                         , wl_funeqs :: [Ct]
                         , wl_rest   :: [Ct] 
                         }
206

batterseapower's avatar
batterseapower committed
207

208
209
unionWorkList :: WorkList -> WorkList -> WorkList
unionWorkList new_wl orig_wl = 
dimitris's avatar
dimitris committed
210
211
212
   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 }
213

214

215
216
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
dimitris's avatar
dimitris committed
217
218
219
220
221
extendWorkListEq ct wl 
  | Just {} <- isCFunEqCan_Maybe ct
  = wl { wl_funeqs = ct : wl_funeqs wl }
  | otherwise
  = wl { wl_eqs = ct : wl_eqs wl }
222

223
224
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
225
226
extendWorkListNonEq ct wl 
  = wl { wl_rest = ct : wl_rest wl }
227

228
229
230
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
dimitris's avatar
dimitris committed
231
 | isEqPred (ctPred ct) = extendWorkListEq ct wl
232
 | otherwise = extendWorkListNonEq ct wl
233

234
235
236
appendWorkListCt :: [Ct] -> WorkList -> WorkList
-- Agnostic
appendWorkListCt cts wl = foldr extendWorkListCt wl cts
237

238
239
240
appendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
appendWorkListEqs cts wl = foldr extendWorkListEq wl cts
241
242

isEmptyWorkList :: WorkList -> Bool
dimitris's avatar
dimitris committed
243
244
isEmptyWorkList wl 
  = null (wl_eqs wl) &&  null (wl_rest wl) && null (wl_funeqs wl)
245
246

emptyWorkList :: WorkList
247
emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = [] }
248

249
workListFromEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
250
workListFromEq ct = extendWorkListEq ct emptyWorkList
251

252
workListFromNonEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
253
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
254

255
256
workListFromCt :: Ct -> WorkList
-- Agnostic 
dimitris's avatar
dimitris committed
257
258
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct 
                  | otherwise            = workListFromNonEq ct
259

dimitris's avatar
dimitris committed
260
261
262
263
264
265
266
267
268

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)

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

276
277
278
279
280
keepWanted :: Cts -> Cts
keepWanted = filterBag isWantedCt
    -- DV: there used to be a note here that read: 
    -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' 
    -- DV: Is this still relevant? 
281

dimitris's avatar
dimitris committed
282
-- Canonical constraint maps
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
data CCanMap a = CCanMap { cts_given   :: UniqFM Cts
                                          -- Invariant: all Given
                         , cts_derived :: UniqFM Cts 
                                          -- Invariant: all Derived
                         , cts_wanted  :: UniqFM Cts } 
                                          -- Invariant: all Wanted

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 
300
  = case cc_ev ct of 
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
      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

320
321
322
323
324
325
326
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))
327

328
329
330
331
332
333
334
335
336
337
     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
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352

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

353
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
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


extractUnsolvedCMap :: CCanMap a -> (Cts, CCanMap a)
-- Gets the wanted or derived constraints and returns a residual
-- CCanMap with only givens.
extractUnsolvedCMap cmap =
  let wntd = foldUFM unionBags emptyCts (cts_wanted cmap)
      derd = foldUFM unionBags emptyCts (cts_derived cmap)
  in (wntd `unionBags` derd, 
      cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM })


dimitris's avatar
dimitris committed
371
-- Maps from PredTypes to Constraints
372
373
374
375
376
377
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
378

379
380
381
382
383
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 [])
384
385
386
387

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

388
389
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
dimitris's avatar
dimitris committed
390
391
392
393
394
395

partCtFamHeadMap :: (Ct -> Bool) 
                 -> CtFamHeadMap 
                 -> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
  = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
396
    in (cts, FamHeadMap tymap_final)
dimitris's avatar
dimitris committed
397
  where
398
    tymap_inside = unFamHeadMap ctmap 
dimitris's avatar
dimitris committed
399
    upd_acc ct (cts,acc_map)
400
401
         | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
         | otherwise = (cts,acc_map)
dimitris's avatar
dimitris committed
402
403
404
405
406
407
408
409
410
411
412
413
414
415
         where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
                      = ty1 
                      | otherwise 
                      = panic "partCtFamHeadMap, encountered non equality!"
\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
445
446
447
448
-- 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_ips :: CCanMap (IPName Name)
              -- Implicit parameters, index is the name
              -- NB: index is /not/ the whole type because IP reactions need 
              -- to match the ip name 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
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
476
477
478
479
  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
480
481
  9 Given family or dictionary constraints don't mention touchable unification variables

482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
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

* A solved Derived is possible; purpose is to avoid creating tons of identical
  Derived goals.
dimitris's avatar
dimitris committed
498

499
500

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

dimitris's avatar
dimitris committed
507
508
509
510
511
512
       , inert_frozen :: Cts       
              -- Frozen errors (as non-canonicals)
                               
       , inert_flat_cache :: CtFamHeadMap 
              -- All ``flattening equations'' are kept here. 
              -- Always canonical CTyFunEqs (Given or Wanted only!)
513
514
515
516
517
518
519
              -- Key is by family head. We use this field during flattening only
              -- Not necessarily inert wrt top-level equations (or inert_cans)

       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi
       , inert_solved        :: PredMap    CtEvidence  -- All others
       	      -- These two fields constitute a cache of solved (only!) constraints
              -- See Note [Solved constraints]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
520
       	      -- - Constraints of form (F xis ~ xi) live in inert_solved_funeqs, 
521
       	      --   all the others are in inert_solved
Simon Peyton Jones's avatar
Simon Peyton Jones committed
522
       	      -- - Used to avoid creating a new EvVar when we have a new goal that we
523
       	      --   have solvedin the past
Simon Peyton Jones's avatar
Simon Peyton Jones committed
524
       	      -- - Stored not necessarily as fully rewritten 
525
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
526
       }
527
528


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

dimitris's avatar
dimitris committed
547
548
549
550
551
552
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                         , inert_eq_tvs = emptyInScopeSet
                         , inert_dicts  = emptyCCanMap
                         , inert_ips    = emptyCCanMap
553
                         , inert_funeqs = FamHeadMap emptyTM 
dimitris's avatar
dimitris committed
554
555
                         , inert_irreds = emptyCts }
       , inert_frozen        = emptyCts
556
557
558
       , inert_flat_cache    = FamHeadMap emptyTM
       , inert_solved        = PredMap emptyTM 
       , inert_solved_funeqs = FamHeadMap emptyTM }
559

560
561
562
updSolvedSet :: InertSet -> CtEvidence -> InertSet 
updSolvedSet is item 
  = let pty = ctEvPred item
dimitris's avatar
dimitris committed
563
564
565
566
        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 = 
567
568
569
               PredMap $ 
               alterTM pty upd_solved (unPredMap $ inert_solved is) }

dimitris's avatar
dimitris committed
570

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

          | Just x  <- isCIPCan_Maybe item      -- IP 
          = ics { inert_ips   = updCCanMap (x,item) (inert_ips ics) }  
            
          | 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) 
                  = panic "updInertSet: item already there!"
613
            in ics { inert_funeqs = FamHeadMap 
dimitris's avatar
dimitris committed
614
                                      (alterTM fam_head upd_funeqs $ 
615
                                         (unFamHeadMap $ inert_funeqs ics)) }
dimitris's avatar
dimitris committed
616
617
618
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
            ppr item 
619

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

       ; modifyInertTcS (\is -> ((), updInertSet is item)) 
                        
       ; traceTcS "updInertSetTcs }" $ empty }


631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
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

       ; modifyInertTcS (\is -> ((), updSolvedSet is item)) 
                        
       ; traceTcS "updSolvedSetTcs }" $ empty }

addSolvedFunEq :: CtEvidence -> TcS ()
addSolvedFunEq fun_eq
  = modifyInertTcS $ \inert -> ((), upd_inert inert)
  where 
    upd_inert inert 
      = let slvd = unFamHeadMap (inert_solved_funeqs inert)
        in inert { inert_solved_funeqs =
                      FamHeadMap (alterTM key upd_funeqs slvd) }       
    upd_funeqs Nothing    = Just fun_eq
    upd_funeqs (Just _ct) = Just fun_eq 
         -- Or _ct? depends on which caches more steps of computation
    key = ctEvPred fun_eq

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

dimitris's avatar
dimitris committed
666

667
668
669
extractUnsolvedTcS :: TcS (Cts,Cts) 
-- Extracts frozen errors and remaining unsolved and sets the 
-- inert set to be the remaining! 
670
extractUnsolvedTcS = modifyInertTcS extractUnsolved 
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686

extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
-- Postcondition
-- -------------
-- When: 
--   ((frozen,cts),is_solved) <- extractUnsolved inert
-- Then: 
-- -----------------------------------------------------------------------------
--  cts       |  The unsolved (Derived or Wanted only) residual 
--            |  canonical constraints, that is, no CNonCanonicals.
-- -----------|-----------------------------------------------------------------
--  frozen    | The CNonCanonicals of the original inert (frozen errors), 
--            | of all flavors
-- -----------|-----------------------------------------------------------------
--  is_solved | Whatever remains from the inert after removing the previous two. 
-- -----------------------------------------------------------------------------
dimitris's avatar
dimitris committed
687
688
689
690
691
692
693
694
extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
                                      , inert_eq_tvs = eq_tvs
                                      , inert_irreds = irreds
                                      , inert_ips    = ips
                                      , inert_funeqs = funeqs
                                      , inert_dicts  = dicts
                                      }
                    , inert_frozen = frozen
695
696
697
698
                    , inert_solved = solved
                    , inert_flat_cache = flat_cache 
                    , inert_solved_funeqs = funeq_cache
                    })
dimitris's avatar
dimitris committed
699
700
701
702
703
704
705
706
707
  
  = let is_solved  = IS { inert_cans = IC { inert_eqs    = solved_eqs
                                          , inert_eq_tvs = eq_tvs
                                          , inert_dicts  = solved_dicts
                                          , inert_ips    = solved_ips
                                          , inert_irreds = solved_irreds
                                          , inert_funeqs = solved_funeqs }
                        , inert_frozen = emptyCts -- All out
                                         
708
709
710
                              -- At some point, I used to flush all the solved, in 
                              -- fear of evidence loops. But I think we are safe, 
                              -- flushing is why T3064 had become slower
711
712
713
                        , inert_solved        = solved      -- PredMap emptyTM
                        , inert_flat_cache    = flat_cache  -- FamHeadMap emptyTM
                        , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
714
                        }
dimitris's avatar
dimitris committed
715
    in ((frozen, unsolved), is_solved)
716

717
  where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
dimitris's avatar
dimitris committed
718
        unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
719
720
                       eqs `minusVarEnv` solved_eqs

721
        (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
dimitris's avatar
dimitris committed
722
723
        (unsolved_ips, solved_ips)       = extractUnsolvedCMap ips
        (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap dicts
724
        (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
725
726
727
728
729
730
731
732
733
734
735

        unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
                   unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs



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
736
737
738
739
740
741
742
743
744
745
  = 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 })
        extract_ics_relevants ct@(CFunEqCan {}) ics = 
            let (cts,feqs_map)  = 
746
                  let funeq_map = unFamHeadMap $ inert_funeqs ics
dimitris's avatar
dimitris committed
747
748
749
750
751
752
753
754
                      fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
                      lkp = lookupTM fam_head funeq_map
                      new_funeq_map = alterTM fam_head xtm funeq_map
                      xtm Nothing    = Nothing
                      xtm (Just _ct) = Nothing
                  in case lkp of 
                    Nothing -> (emptyCts, funeq_map)
                    Just ct -> (singleCt ct, new_funeq_map)
755
            in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
dimitris's avatar
dimitris committed
756
757
758
759
760
761
762
763
764
        extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics = 
            let (cts, ips_map) = getRelevantCts nm (inert_ips ics) 
            in (cts, ics { inert_ips = ips_map })
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
        extract_ics_relevants _ ics = (emptyCts,ics)
        

765
lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
766
767
768
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
  = case lookupInSolved solved pty of
769
770
      Just ctev -> return ctev
      Nothing   -> lookupInInertCans ics pty
dimitris's avatar
dimitris committed
771

772
lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
773
-- Returns just if exactly this predicate type exists in the solved.
774
lookupInSolved tm pty = lookupTM pty $ unPredMap tm
dimitris's avatar
dimitris committed
775

776
lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
777
778
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans ics pty
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
  = 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
799
800
\end{code}

801

dimitris's avatar
dimitris committed
802
803


804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
%************************************************************************
%*									*
%*		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 { 
826
      tcs_ev_binds    :: EvBindsVar,
dimitris's avatar
dimitris committed
827
      
828
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
829
830
          -- Global type bindings

831
      tcs_context :: SimplContext,
832
                     
833
834
      tcs_untch :: TcsUntouchables,

dimitris's avatar
dimitris committed
835
836
837
      tcs_ic_depth   :: Int,       -- Implication nesting depth
      tcs_count      :: IORef Int, -- Global step count

838
      tcs_inerts   :: IORef InertSet, -- Current inert set
839
840
841
842
843
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
      -- while solving the current worklist.
      tcs_implics  :: IORef (Bag Implication)
844
    }
dimitris's avatar
dimitris committed
845

846
847
848
849
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify
850
851
852
\end{code}

\begin{code}
853
data SimplContext
854
855
856
  = SimplInfer SDoc	   -- Inferring type of a let-bound thing
  | SimplInteractive	   -- Inferring type at GHCi prompt
  | SimplCheck SDoc	   -- Checking a type signature or RULE rhs
857
858

instance Outputable SimplContext where
859
860
  ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
  ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
861
862
863
864
865
866
867
  ppr SimplInteractive = ptext (sLit "SimplInteractive")

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

performDefaulting :: SimplContext -> Bool
868
869
870
performDefaulting (SimplInfer {})   = False
performDefaulting SimplInteractive  = True
performDefaulting (SimplCheck {})   = True
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905

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

908
909
910
911
912
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

913
traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
914
915
916
917
918
919
920
921
922
-- 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 }
923
924

runTcS :: SimplContext
925
       -> Untouchables 	       -- Untouchables
926
927
       -> InertSet             -- Initial inert set
       -> WorkList             -- Initial work list
928
       -> TcS a		       -- What to run
929
       -> TcM (a, Bag EvBind)
930
runTcS context untouch is wl tcs 
931
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
932
       ; ev_binds_var <- TcM.newTcEvBinds
933
       ; impl_var <- TcM.newTcRef emptyBag
934
       ; step_count <- TcM.newTcRef 0
935
936
937
938

       ; inert_var <- TcM.newTcRef is 
       ; wl_var <- TcM.newTcRef wl

939
940
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
941
                          , tcs_context  = context
942
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
943
944
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
945
                          , tcs_inerts   = inert_var
946
947
                          , tcs_worklist = wl_var 
                          , tcs_implics  = impl_var }
948
949

	     -- Run the computation
950
       ; res <- unTcS tcs env
951
952
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
953
       ; mapM_ do_unification (varEnvElts ty_binds)
954

Ian Lynagh's avatar
Ian Lynagh committed
955
956
957
958
959
960
       ; when debugIsOn $ do {
             count <- TcM.readTcRef step_count
           ; when (opt_PprStyle_Debug && count > 0) $
             TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") 
                                <+> int count <+> ppr context)
         }
961
             -- And return
962
963
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
       ; return (res, ev_binds) }
964
965
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
966

967
968
969
970

doWithInert :: InertSet -> TcS a -> TcS a 
doWithInert inert (TcS action)
  = TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert
dimitris's avatar
dimitris committed
971
                     ; action (env { tcs_inerts = new_inert_var }) }
972
973
974
975
976
977
978
979
980

nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a 
nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) 
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
                   , tcs_untch = (_outer_range, outer_tcs)
                   , tcs_count = count
                   , tcs_ic_depth = idepth
                   , tcs_context = ctxt
                   , tcs_inerts = inert_var
981
982
                   , tcs_worklist = wl_var 
                   , tcs_implics = _impl_var } -> 
dimitris's avatar
dimitris committed
983
    do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
984
985
986
987
       		   -- The inner_range should be narrower than the outer one
		   -- (thus increasing the set of untouchables) but 
		   -- the inner Tcs-untouchables must be unioned with the
		   -- outer ones!
dimitris's avatar
dimitris committed
988

989
990
991
         -- Inherit the inerts from the outer scope
       ; orig_inerts <- TcM.readTcRef inert_var
       ; new_inert_var <- TcM.newTcRef orig_inerts
992
993
994
995
         -- Inherit residual implications from outer scope (?) or create
         -- fresh var?                 
--     ; orig_implics <- TcM.readTcRef impl_var                   
       ; new_implics_var <- TcM.newTcRef emptyBag
dimitris's avatar
dimitris committed
996
                           
997
998
999
1000
1001
       ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                               , tcs_ty_binds    = ty_binds
                               , tcs_untch       = inner_untch
                               , tcs_count       = count
                               , tcs_ic_depth    = idepth+1
1002
                               , tcs_context     = ctxt 
1003
1004
1005
1006
                               , tcs_inerts      = new_inert_var
                               , tcs_worklist    = wl_var 
                               -- NB: worklist is going to be empty anyway, 
                               -- so reuse the same ref cell
1007
                               , tcs_implics     = new_implics_var
1008
1009
                               }
       ; thing_inside nest_env } 
1010

1011
1012
1013
1014
1015
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

1016
tryTcS :: TcS a -> TcS a
1017
1018
1019
-- 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
1020
tryTcS tcs
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
  = 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
1035
1036
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
-- 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) 

1047
1048
1049
1050
1051
1052
1053

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

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

1054
1055
1056
getTcSWorkList :: TcS WorkList
getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 

1057
1058
1059
1060
1061
1062
1063
1064
1065
1066

getTcSWorkListTvs :: TcS TyVarSet
-- Return the variables of the worklist
getTcSWorkListTvs 
  = do { wl <- getTcSWorkList
       ; return $
         cts_tvs (wl_eqs wl) `unionVarSet` cts_tvs (wl_funeqs wl) `unionVarSet` cts_tvs (wl_rest wl) }
  where cts_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet 


1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
updWorkListTcS f 
  = updWorkListTcS_return (\w -> ((),f w))

updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
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 }
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
    

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)

1090

1091
emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
1092
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
dimitris's avatar
dimitris committed
1093
emitFrozenError fl depth 
1094
  = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
1095
1096
       ; inert_ref <- getTcSInertsRef 
       ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
1097
       ; let ct = CNonCanonical { cc_ev = fl
1098
1099
1100
1101
                                , cc_depth = depth } 
             inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
       ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }

1102
instance HasDynFlags TcS where
1103
    getDynFlags = wrapTcS getDynFlags
1104
1105
1106
1107
1108
1109
1110

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

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

dimitris's avatar
dimitris committed
1111
getFlatCache :: TcS CtTypeMap 
1112
getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
dimitris's avatar
dimitris committed
1113
1114
1115

updFlatCache :: Ct -> TcS ()
-- Pre: constraint is a flat family equation (equal to a flatten skolem)
1116
updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis })
dimitris's avatar
dimitris committed
1117
  = modifyInertTcS upd_inert_cache
1118
  where upd_inert_cache is = ((), is { inert_flat_cache = FamHeadMap new_fc })
dimitris's avatar
dimitris committed
1119
                           where new_fc = alterTM pred_key upd_cache fc
1120
                                 fc = unFamHeadMap $ inert_flat_cache is
dimitris's avatar
dimitris committed
1121
        pred_key = mkTyConApp tc xis
1122
        upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct 
dimitris's avatar
dimitris committed
1123
1124
1125
1126
1127
        upd_cache (Just _ct) = Just flat_eq 
        upd_cache Nothing    = Just flat_eq
updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
                        ppr other_ct
                        
1128

1129
getUntouchables :: TcS TcsUntouchables
1130
1131
getUntouchables = TcS (return . tcs_untch)

1132
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1133
1134
getTcSTyBinds = TcS (return . tcs_ty_binds)

1135
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1136
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1137

1138
1139
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
1140
1141
1142
1143
1144
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
1145
-- We never do this twice!
1146
1147
1148
1149
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
Ian Lynagh's avatar
Ian Lynagh committed
1150
1151
1152
1153
1154
            ; 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)]
1155
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1156
1157


1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
\end{code}
Note [Optimizing Spontaneously Solved Coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

Spontaneously solved coercions such as alpha := tau used to be bound as everything else
in the evidence binds. Subsequently they were used for rewriting other wanted or solved
goals. For instance: 

WorkItem = [S] g1 : a ~ tau
Inerts   = [S] g2 : b ~ [a]
           [S] g3 : c ~ [(a,a)]

Would result, eventually, after the workitem rewrites the inerts, in the
following evidence bindings:

        g1 = ReflCo tau
        g2 = ReflCo [a]
        g3 = ReflCo [(a,a)]
        g2' = g2 ; [g1] 
        g3' = g3 ; [(g1,g1)]

This ia annoying because it puts way too much stress to the zonker and
desugarer, since we /know/ at the generation time (spontaneously
solving) that the evidence for a particular evidence variable is the
identity.

For this reason, our solution is to cache inside the GivenSolved
flavor of a constraint the term which is actually solving this
constraint. Whenever we perform a setEvBind, a new flavor is returned
so that if it was a GivenSolved to start with, it remains a
GivenSolved with a new evidence term inside. Then, when we use solved
goals to rewrite other constraints we simply use whatever is in the
GivenSolved flavor and not the constraint cc_id.

In our particular case we'd get the following evidence bindings, eventually: 

       g1 = ReflCo tau
       g2 = ReflCo [a]
       g3 = ReflCo [(a,a)]
       g2'= ReflCo [a]
       g3'= ReflCo [(a,a)]

Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.

\begin{code}
1203

1204
1205
1206
1207
1208
1209
1210
1211
1212

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

getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
getDefaultInfo 
  = do { ctxt <- getTcSContext
1213
       ; (tys, flags) <- wrapTcS TcM.tcGetDefaultTys
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
       ; return (ctxt, tys, flags) }

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

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

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

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

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

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

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

pprEq :: TcType -> TcType -> SDoc
1244
pprEq ty1 ty2 = pprType $ mkEqPred ty1 ty2
1245
1246

isTouchableMetaTyVar :: TcTyVar -> TcS Bool
1247
isTouchableMetaTyVar tv 
1248
1249
1250
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

1251
1252
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
1253
1254
  = ASSERT2 ( isTcTyVar tv, ppr tv )
    case tcTyVarDetails tv of 
1255
1256
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
1257
1258
1259
1260
      MetaTv {}      -> inTouchableRange untch tv 
      _              -> False 


1261
1262
\end{code}

1263

1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
Note [Touchable meta type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Meta type variables allocated *by the constraint solver itself* are always
touchable.  Example: 
   instance C a b => D [a] where...
if we use this instance declaration we "make up" a fresh meta type
variable for 'b', which we must later guess.  (Perhaps C has a
functional dependency.)  But since we aren't in the constraint *generator*
we can't allocate a Unique in the touchable range for this implication
constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
1274
1275


1276
\begin{code}
1277
1278
1279
1280
1281
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
1282
1283
1284

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
dimitris's avatar
dimitris committed
1285
1286
1287
1288
1289
1290
  = do { tv <- wrapTcS $ 
               do { uniq <- TcM.newUnique
                  ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
                  ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
       ; traceTcS "New Flatten Skolem Born" $
         ppr tv <+> text "[:= " <+> ppr ty <+> text "]"
1291
       ; return tv }
1292
1293
1294
1295

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

1296
1297
1298
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
instDFunType dfun_id mb_inst_tys 
  = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
1299
  where
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
    (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)

instFlexiTcS :: TyVar -> TcS TcType 
dimitris's avatar
dimitris committed
1316
1317
-- Like TcM.instMetaTyVar but the variable that is created is 
-- always touchable; we are supposed to guess its instantiation.
1318
-- See Note [Touchable meta type variables] 
1319
instFlexiTcS tv = wrapTcS (instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) )
1320

1321
1322
1323
1324
1325
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
1326
       ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
1327
1328
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

1329
1330
1331
1332
1333
1334
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

1335
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1336
instFlexiTcSHelper tvname tvkind
1337
  = do { uniq <- TcM.newUnique 
1338
1339
1340
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
1341
       ; return (mkTyVarTy (mkTcTyVar name kind (MetaTv TcsTv ref))) }
1342
1343


dimitris's avatar
dimitris committed
1344
1345
1346
1347
-- Creating and setting evidence variables and CtFlavors
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data XEvTerm = 
1348
  XEvTerm { ev_comp   :: [EvTerm] -> EvTerm
dimitris's avatar
dimitris committed
1349
                         -- How to compose evidence 
1350
          , ev_decomp :: EvTerm -> [EvTerm]
dimitris's avatar
dimitris committed
1351
1352
1353
                         -- How to decompose evidence 
          }

1354
data MaybeNew = Fresh CtEvidence | Cached EvTerm
dimitris's avatar
dimitris committed
1355

1356
isFresh :: MaybeNew -> Bool
dimitris's avatar
dimitris committed
1357