TcSMonad.lhs 64.7 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,
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
    isFlexiTcsTv, instFlexiTcSHelperTcS,
31

32
    canRewrite, canSolve,
33
    mkGivenLoc, ctWantedLoc,
34

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

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

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

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

62
63

    newFlattenSkolemTy,                         -- Flatten skolems 
64

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

78
    instDFunType,                              -- Instantiation
79
    newFlexiTcSTy, instFlexiTcS,
80

81
    compatKind, mkKindErrorCtxtTcS,
82

83
    TcsUntouchables,
84
    isTouchableMetaTyVar,
85
    isTouchableMetaTyVar_InRange, 
86
87
88
89
90
91

    getDefaultInfo, getDynFlags,

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

118
import TcEvidence
119
120
import Class
import TyCon
121

122
123
import Name
import Var
124
import VarEnv
125
126
127
128
import Outputable
import Bag
import MonadUtils
import VarSet
129

130
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
131
import Util
132
import Id 
Ian Lynagh's avatar
Ian Lynagh committed
133
import TcRnTypes
134

135
136
import Unique 
import UniqFM
137
138
139
#ifdef DEBUG
import Digraph
#endif
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


dimitris's avatar
dimitris committed
277
-- Canonical constraint maps
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
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 
295
  = case cc_ev ct of 
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
      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

315
316
317
318
319
320
321
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))
322

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

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

348
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
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
366
-- Maps from PredTypes to Constraints
367
368
369
370
371
372
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
373

374
375
376
377
378
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 [])
379
380
381
382

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

383
384
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
dimitris's avatar
dimitris committed
385
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
492
493
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
494

495
496

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

dimitris's avatar
dimitris committed
503
504
505
506
507
508
       , 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!)
509
510
511
512
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)

       , 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
516
       	      -- - Constraints of form (F xis ~ xi) live in inert_solved_funeqs, 
517
       	      --   all the others are in inert_solved
Simon Peyton Jones's avatar
Simon Peyton Jones committed
518
       	      -- - Used to avoid creating a new EvVar when we have a new goal that we
519
       	      --   have solvedin the past
Simon Peyton Jones's avatar
Simon Peyton Jones committed
520
       	      -- - Stored not necessarily as fully rewritten 
521
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
522
       }
523
524


dimitris's avatar
dimitris committed
525
526
527
528
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 $ 
529
                                  ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
dimitris's avatar
dimitris committed
530
531
532
533
534
                 , vcat (map ppr (Bag.bagToList $ inert_irreds ics))
                 ]
            
instance Outputable InertSet where 
  ppr is = vcat [ ppr $ inert_cans is
535
536
                , text "Frozen errors =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
dimitris's avatar
dimitris committed
537
538
                , text "Solved and cached" <+>
                    int (foldTypeMap (\_ x -> x+1) 0 
539
                             (unPredMap $ inert_solved is)) <+> 
dimitris's avatar
dimitris committed
540
                    text "more constraints" ]
541

dimitris's avatar
dimitris committed
542
543
544
545
546
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                         , inert_eq_tvs = emptyInScopeSet
                         , inert_dicts  = emptyCCanMap
547
                         , inert_funeqs = FamHeadMap emptyTM 
dimitris's avatar
dimitris committed
548
549
                         , inert_irreds = emptyCts }
       , inert_frozen        = emptyCts
550
551
552
       , inert_flat_cache    = FamHeadMap emptyTM
       , inert_solved        = PredMap emptyTM 
       , inert_solved_funeqs = FamHeadMap emptyTM }
553

554
555
556
updSolvedSet :: InertSet -> CtEvidence -> InertSet 
updSolvedSet is item 
  = let pty = ctEvPred item
dimitris's avatar
dimitris committed
557
558
559
560
        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 = 
561
562
563
               PredMap $ 
               alterTM pty upd_solved (unPredMap $ inert_solved is) }

dimitris's avatar
dimitris committed
564

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

          | 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!"
604
            in ics { inert_funeqs = FamHeadMap 
dimitris's avatar
dimitris committed
605
                                      (alterTM fam_head upd_funeqs $ 
606
                                         (unFamHeadMap $ inert_funeqs ics)) }
dimitris's avatar
dimitris committed
607
608
609
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
            ppr item 
610

611
updInertSetTcS :: Ct -> TcS ()
612
613
614
615
616
617
618
619
620
621
-- 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 }


622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
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

648
649
650
651
652
653
654
655
656
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
657

658
659
660
extractUnsolvedTcS :: TcS (Cts,Cts) 
-- Extracts frozen errors and remaining unsolved and sets the 
-- inert set to be the remaining! 
661
extractUnsolvedTcS = modifyInertTcS extractUnsolved 
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677

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
678
679
680
681
682
683
684
extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
                                      , inert_eq_tvs = eq_tvs
                                      , inert_irreds = irreds
                                      , inert_funeqs = funeqs
                                      , inert_dicts  = dicts
                                      }
                    , inert_frozen = frozen
685
686
687
688
                    , inert_solved = solved
                    , inert_flat_cache = flat_cache 
                    , inert_solved_funeqs = funeq_cache
                    })
dimitris's avatar
dimitris committed
689
690
691
692
693
694
695
696
  
  = let is_solved  = IS { inert_cans = IC { inert_eqs    = solved_eqs
                                          , inert_eq_tvs = eq_tvs
                                          , inert_dicts  = solved_dicts
                                          , inert_irreds = solved_irreds
                                          , inert_funeqs = solved_funeqs }
                        , inert_frozen = emptyCts -- All out
                                         
697
698
699
                              -- 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
700
701
702
                        , inert_solved        = solved      -- PredMap emptyTM
                        , inert_flat_cache    = flat_cache  -- FamHeadMap emptyTM
                        , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
703
                        }
dimitris's avatar
dimitris committed
704
    in ((frozen, unsolved), is_solved)
705

706
  where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
dimitris's avatar
dimitris committed
707
        unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
708
709
                       eqs `minusVarEnv` solved_eqs

710
        (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
dimitris's avatar
dimitris committed
711
        (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap dicts
712
        (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
713
714

        unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
715
                   unsolved_dicts `unionBags` unsolved_funeqs
716
717
718
719
720
721
722
723



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
724
725
726
727
728
729
730
731
732
733
  = 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)  = 
734
                  let funeq_map = unFamHeadMap $ inert_funeqs ics
dimitris's avatar
dimitris committed
735
736
737
738
739
740
741
742
                      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)
743
            in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
dimitris's avatar
dimitris committed
744
745
746
747
748
749
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
        extract_ics_relevants _ ics = (emptyCts,ics)
        

750
lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
751
752
753
-- 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
754
755
      Just ctev -> return ctev
      Nothing   -> lookupInInertCans ics pty
dimitris's avatar
dimitris committed
756

757
lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
758
-- Returns just if exactly this predicate type exists in the solved.
759
lookupInSolved tm pty = lookupTM pty $ unPredMap tm
dimitris's avatar
dimitris committed
760

761
lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
762
763
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans ics pty
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
  = 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
784
785
\end{code}

786

dimitris's avatar
dimitris committed
787
788


789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
%************************************************************************
%*									*
%*		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 { 
811
      tcs_ev_binds    :: EvBindsVar,
dimitris's avatar
dimitris committed
812
      
813
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
814
          -- Global type bindings
815
                     
816
817
      tcs_untch :: TcsUntouchables,

dimitris's avatar
dimitris committed
818
819
820
      tcs_ic_depth   :: Int,       -- Implication nesting depth
      tcs_count      :: IORef Int, -- Global step count

821
      tcs_inerts   :: IORef InertSet, -- Current inert set
822
823
824
825
826
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
      -- while solving the current worklist.
      tcs_implics  :: IORef (Bag Implication)
827
    }
dimitris's avatar
dimitris committed
828

829
830
831
832
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify
833
834
835
\end{code}

\begin{code}
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870

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

873
874
875
876
877
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

878
traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
879
880
881
882
883
884
885
886
887
-- 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 }
888

889
890
891
892
runTcSWithEvBinds :: EvBindsVar
                  -> TcS a 
                  -> TcM a
runTcSWithEvBinds ev_binds_var tcs
893
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
894
       ; impl_var <- TcM.newTcRef emptyBag
895
       ; step_count <- TcM.newTcRef 0
896
897
898
899

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

900
901
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
902
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
903
904
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
905
                          , tcs_inerts   = inert_var
906
907
                          , tcs_worklist = wl_var 
                          , tcs_implics  = impl_var }
908
909

	     -- Run the computation
910
       ; res <- unTcS tcs env
911
912
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
913
       ; mapM_ do_unification (varEnvElts ty_binds)
914

915
916
917
918
       ; when debugIsOn $ 
         do { count <- TcM.readTcRef step_count
            ; when (opt_PprStyle_Debug && count > 0) $
              TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count ) }
919
             -- And return
920
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
921
       ; checkForCyclicBinds ev_binds
922
       ; return res }
923
924
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
925
926
927
928
929
930
931
932
933
934
935
    untouch = NoUntouchables
    is = emptyInert
    wl = emptyWorkList
    
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) }
936

937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
checkForCyclicBinds :: Bag EvBind -> TcM ()
#ifndef DEBUG
checkForCyclicBinds _ = return ()
#else
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       
958
959
960
961

doWithInert :: InertSet -> TcS a -> TcS a 
doWithInert inert (TcS action)
  = TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert
dimitris's avatar
dimitris committed
962
                     ; action (env { tcs_inerts = new_inert_var }) }
963
964
965
966
967
968
969
970

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_inerts = inert_var
971
972
                   , tcs_worklist = wl_var 
                   , tcs_implics = _impl_var } -> 
dimitris's avatar
dimitris committed
973
    do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
974
975
976
977
       		   -- 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
978

979
980
981
         -- Inherit the inerts from the outer scope
       ; orig_inerts <- TcM.readTcRef inert_var
       ; new_inert_var <- TcM.newTcRef orig_inerts
982
983
984
985
         -- 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
986
                           
987
988
989
990
991
992
993
994
995
       ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                               , tcs_ty_binds    = ty_binds
                               , tcs_untch       = inner_untch
                               , tcs_count       = count
                               , tcs_ic_depth    = idepth+1
                               , tcs_inerts      = new_inert_var
                               , tcs_worklist    = wl_var 
                               -- NB: worklist is going to be empty anyway, 
                               -- so reuse the same ref cell
996
                               , tcs_implics     = new_implics_var
997
                               }
998
999
1000
1001
1002
1003
1004
       ; res <- thing_inside nest_env 
                
       -- Perform a check that the thing_inside did not cause cycles
       ; ev_binds <- TcM.getTcEvBinds ref
       ; checkForCyclicBinds ev_binds
         
       ; return res }
1005

1006
1007
1008
1009
1010
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

1011
tryTcS :: TcS a -> TcS a
1012
1013
1014
-- 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
1015
tryTcS tcs
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
  = 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
1030
1031
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
-- 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) 

1042
1043
1044
1045
1046
1047
1048

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

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

1049
1050
1051
getTcSWorkList :: TcS WorkList
getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 

1052
1053
1054
1055
1056
1057
1058
1059
1060
1061

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 


1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
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 }
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
    

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)

1085

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

1097
instance HasDynFlags TcS where
1098
    getDynFlags = wrapTcS getDynFlags
1099
1100
1101
1102
1103


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

dimitris's avatar
dimitris committed
1104
getFlatCache :: TcS CtTypeMap 
1105
getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
dimitris's avatar
dimitris committed
1106
1107
1108

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

1122
getUntouchables :: TcS TcsUntouchables
1123
1124
getUntouchables = TcS (return . tcs_untch)

1125
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1126
1127
getTcSTyBinds = TcS (return . tcs_ty_binds)

1128
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1129
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1130

1131
1132
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
1133
1134
1135
1136
1137
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
1138
-- We never do this twice!
1139
1140
1141
1142
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
Ian Lynagh's avatar
Ian Lynagh committed
1143
1144
1145
1146
1147
            ; 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)]
1148
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1149
1150


1151
1152
1153
1154
1155
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
\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}
1196

1197
1198
1199
1200
1201
1202

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

1203
1204
getDefaultInfo ::  TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233

-- 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
1234
pprEq ty1 ty2 = pprType $ mkEqPred ty1 ty2
1235
1236

isTouchableMetaTyVar :: TcTyVar -> TcS Bool
1237
isTouchableMetaTyVar tv 
1238
1239
1240
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

1241
1242
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
1243
1244
  = ASSERT2 ( isTcTyVar tv, ppr tv )
    case tcTyVarDetails tv of 
1245
1246
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
1247
      MetaTv {}      -> inTouchableRange untch tv && not (tv `elemVarSet` untch_tcs)
1248
1249
1250
      _              -> False 


1251
1252
\end{code}

1253

1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
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.
1264
1265


1266
\begin{code}
1267
1268
1269
1270
1271
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
1272
1273
1274

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
dimitris's avatar
dimitris committed
1275
1276
1277
1278
1279
1280
  = 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 "]"
1281
       ; return tv }
1282
1283
1284
1285

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

1286
1287
1288
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
instDFunType dfun_id mb_inst_tys 
  = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
1289
  where
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
    (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)

1305
instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
dimitris's avatar
dimitris committed
1306
1307
-- Like TcM.instMetaTyVar but the variable that is created is 
-- always touchable; we are supposed to guess its instantiation.
1308
-- See Note [Touchable meta type variables] 
1309
1310
1311
1312
1313
instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
  where
     inst_one subst tv = do { ty' <- instFlexiTcSHelper (tyVarName tv) 
                                                        (substTy subst (tyVarKind tv))
                            ; return (extendTvSubst subst tv ty', ty') }
1314

1315
1316
1317
1318
1319
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
1320
       ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
1321
1322
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

1323
1324
1325
1326
1327
1328
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

1329
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1330
instFlexiTcSHelper tvname tvkind
1331
  = do { uniq <- TcM.newUnique 
1332
1333
1334
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
1335
       ; return (mkTyVarTy (mkTcTyVar name kind (MetaTv TcsTv ref))) }
1336

1337
1338
instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
1339

dimitris's avatar
dimitris committed
1340
1341
1342
1343
-- Creating and setting evidence variables and CtFlavors
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data XEvTerm = 
1344
  XEvTerm { ev_comp   :: [EvTerm] -> EvTerm
dimitris's avatar
dimitris committed
1345
                         -- How to compose evidence 
1346
          , ev_decomp :: EvTerm -> [EvTerm]
dimitris's avatar
dimitris committed
1347
1348
1349
                         -- How to decompose evidence 
          }

1350
data MaybeNew = Fresh CtEvidence | Cached EvTerm
dimitris's avatar
dimitris committed
1351

1352
isFresh :: MaybeNew -> Bool
dimitris's avatar
dimitris committed
1353
1354
1355
isFresh (Fresh {}) = True
isFresh _ = False

1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
getEvTerm :: MaybeNew -> EvTerm
getEvTerm (Fresh ctev) = ctEvTerm ctev
getEvTerm (Cached tm)  = tm

getEvTerms :: [MaybeNew] -> [EvTerm]
getEvTerms = map getEvTerm

freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals mns = [ ctev | Fresh ctev <- mns ]

dimitris's avatar
dimitris committed
1366
setEvBind :: EvVar -> EvTerm -> TcS ()