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

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
20
    updWorkListTcS, updWorkListTcS_return,
21
22
    
    getTcSImplics, updTcSImplics, emitTcSImplication, 
23

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

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

30
    canRewrite, canSolve,
31
    mkGivenLoc, ctWantedLoc,
32

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

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

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

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

59
60

    newFlattenSkolemTy,                         -- Flatten skolems 
61

Simon Peyton Jones's avatar
Simon Peyton Jones committed
62
63
64
        -- Deque
    Deque(..), insertDeque, emptyDeque,

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

79
    instDFunType,                              -- Instantiation
80
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
81
    cloneMetaTyVar,
82

83
    compatKind, mkKindErrorCtxtTcS,
84

85
    Untouchables, isTouchableMetaTyVarTcS,
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
import Outputable
import Bag
import MonadUtils
128

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

134
135
import Unique 
import UniqFM
136
import Maybes ( orElse, catMaybes, firstJust )
137

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

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

149

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

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

160
161
\end{code}

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

171
172
173
174
175
Note [WorkList]
~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors). 
Notice that each Ct now has a simplification depth. We may 
consider using this depth for prioritization as well in the future. 
176

177
178
179
180
181
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. 
182

183
184
185
186
187
188
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. 
189

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

193
194
195
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)
196

197
\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
                            -- First to remove is at head of LH field

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

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

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

insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)

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

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

223
-- See Note [WorkList]
224
data WorkList = WorkList { wl_eqs    :: [Ct]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
225
                         , wl_funeqs :: Deque Ct
226
227
                         , wl_rest   :: [Ct] 
                         }
228

batterseapower's avatar
batterseapower committed
229

Simon Peyton Jones's avatar
Simon Peyton Jones committed
230
231
232
233
234
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList new_wl orig_wl 
   = WorkList { wl_eqs    = wl_eqs new_wl    ++            wl_eqs orig_wl
              , wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
              , wl_rest   = wl_rest new_wl   ++            wl_rest orig_wl }
235

236

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
245
246
247
248
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
extendWorkListEqs cts wl = foldr extendWorkListEq wl cts

249
250
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
251
252
extendWorkListNonEq ct wl 
  = wl { wl_rest = ct : wl_rest wl }
253

254
255
256
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
dimitris's avatar
dimitris committed
257
 | isEqPred (ctPred ct) = extendWorkListEq ct wl
258
 | otherwise = extendWorkListNonEq ct wl
259

Simon Peyton Jones's avatar
Simon Peyton Jones committed
260
extendWorkListCts :: [Ct] -> WorkList -> WorkList
261
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
262
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
263
264

isEmptyWorkList :: WorkList -> Bool
dimitris's avatar
dimitris committed
265
isEmptyWorkList wl 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
266
  = null (wl_eqs wl) &&  null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
267
268

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

271
workListFromEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
272
workListFromEq ct = extendWorkListEq ct emptyWorkList
273

274
workListFromNonEq :: Ct -> WorkList
dimitris's avatar
dimitris committed
275
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
276

277
278
workListFromCt :: Ct -> WorkList
-- Agnostic 
dimitris's avatar
dimitris committed
279
280
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct 
                  | otherwise            = workListFromNonEq ct
281

dimitris's avatar
dimitris committed
282
283
284
285
286

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

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


dimitris's avatar
dimitris committed
300
-- Canonical constraint maps
301
302
303
304
305
306
307
data CCanMap a 
  = CCanMap { cts_given   :: UniqFM Cts   -- All Given
            , cts_derived :: UniqFM Cts   -- All Derived
            , cts_wanted  :: UniqFM Cts } -- All Wanted

keepGivenCMap :: CCanMap a -> CCanMap a
keepGivenCMap cc = emptyCCanMap { cts_given = cts_given cc }
308
309
310
311
312
313
314
315
316
317
318

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 
319
  = case cc_ev ct of 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
320
321
322
      CtWanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
      CtGiven {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
      CtDerived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
  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

339
340
341
342
343
344
345
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))
346

347
348
349
350
351
352
353
354
355
356
     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
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371

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

372
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
373
374
375
376
377
378
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

379
380
381
382
extractUnsolvedCMap :: CCanMap a -> Cts
-- Gets the wanted or derived constraints
extractUnsolvedCMap cmap = foldUFM unionBags emptyCts (cts_wanted cmap)
              `unionBags`  foldUFM unionBags emptyCts (cts_derived cmap)
383

dimitris's avatar
dimitris committed
384
-- Maps from PredTypes to Constraints
385
386
387
388
389
390
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
391

392
393
394
395
396
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 [])
397

398
399
400
401
402
403
sizePredMap :: PredMap a -> Int
sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m

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

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

407
408
lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
lookupFamHead (FamHeadMap m) key = lookupTM key m
dimitris's avatar
dimitris committed
409

410
411
412
413
414
415
416
417
418
insertFamHead :: FamHeadMap a -> TcType -> a -> FamHeadMap a
insertFamHead (FamHeadMap m) key value = FamHeadMap (alterTM key (const (Just value)) m)

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

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

dimitris's avatar
dimitris committed
419
420
421
422
423
partCtFamHeadMap :: (Ct -> Bool) 
                 -> CtFamHeadMap 
                 -> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
  = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
424
    in (cts, FamHeadMap tymap_final)
dimitris's avatar
dimitris committed
425
  where
426
    tymap_inside = unFamHeadMap ctmap 
dimitris's avatar
dimitris committed
427
    upd_acc ct (cts,acc_map)
428
429
         | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
         | otherwise = (cts,acc_map)
dimitris's avatar
dimitris committed
430
431
432
433
         where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
                      = ty1 
                      | otherwise 
                      = panic "partCtFamHeadMap, encountered non equality!"
434
435
436
437
438

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
439
440
441
442
443
444
445
446
447
448
\end{code}

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

\begin{code}
449
-- All Given (fully known) or Wanted or Derived
dimitris's avatar
dimitris committed
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
-- See Note [Detailed InertCans Invariants] for more
data InertCans 
  = IC { inert_eqs :: TyVarEnv Ct
              -- Must all be CTyEqCans! If an entry exists of the form: 
              --   a |-> ct,co
              -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
              -- And  co : a ~ xi
       , inert_dicts :: CCanMap Class
              -- Dictionaries only, index is the class
              -- NB: index is /not/ the whole type because FD reactions 
              -- need to match the class but not necessarily the whole type.
       , inert_funeqs :: CtFamHeadMap
              -- Family equations, index is the whole family head type.
       , inert_irreds :: Cts       
              -- Irreducible predicates
       }
    
                     
\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
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
  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
507
508
  9 Given family or dictionary constraints don't mention touchable unification variables

509
510
511
512
513
514
515
516
517
518
519
520
521
522
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

523
524
525
526
* A solved Derived in inert_solved is possible; purpose is to avoid
  creating tons of identical Derived goals.

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

528
529

\begin{code}
dimitris's avatar
dimitris committed
530
531
532
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
533
534
535
              -- Canonical Given, Wanted, Derived (no Solved)
	      -- Sometimes called "the inert set"

536
       , inert_insols :: Cts       
dimitris's avatar
dimitris committed
537
538
              -- Frozen errors (as non-canonicals)
                               
539
       , inert_fsks :: [TcTyVar]  -- Flatten-skolems allocated in this local scope
dimitris's avatar
dimitris committed
540
541
              -- All ``flattening equations'' are kept here. 
              -- Always canonical CTyFunEqs (Given or Wanted only!)
542
543
544
              -- Key is by family head. We use this field during flattening only
              -- Not necessarily inert wrt top-level equations (or inert_cans)

545
546
547
548
       , inert_solved_funeqs :: CtFamHeadMap  
              -- Of form co :: F xis ~ xi 
              -- Always the result of using a top-level family axiom F xis ~ tau
              -- No Deriveds 
549

550
551
552
       , inert_solved_dicts   :: PredMap CtEvidence 
       	      -- Of form ev :: C t1 .. tn
              -- Always the result of using a top-level instance declaration
553
              -- See Note [Solved constraints]
554
555
       	      -- - Used to avoid creating a new EvVar when we have a new goal 
       	      --   that we have solved in the past
Simon Peyton Jones's avatar
Simon Peyton Jones committed
556
       	      -- - Stored not necessarily as fully rewritten 
557
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
558
       }
559
560


dimitris's avatar
dimitris committed
561
instance Outputable InertCans where 
562
563
564
565
  ppr ics = vcat [ ptext (sLit "Equalities:") 
                   <+> vcat (map ppr (varEnvElts (inert_eqs ics)))
                 , ptext (sLit "Type-function equalities:")
                   <+> vcat (map ppr (Bag.bagToList $ 
566
                                  ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
567
568
569
570
                 , ptext (sLit "Dictionaries:")
                   <+> vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
                 , ptext (sLit "Irreds:")
                   <+> vcat (map ppr (Bag.bagToList $ inert_irreds ics))
dimitris's avatar
dimitris committed
571
572
573
574
                 ]
            
instance Outputable InertSet where 
  ppr is = vcat [ ppr $ inert_cans is
575
                , text "Frozen errors =" <+> -- Clearly print frozen errors
576
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols is)))
577
578
                , text "Solved dicts"  <+> int (sizePredMap (inert_solved_dicts is))
                , text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
579

dimitris's avatar
dimitris committed
580
581
582
583
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                         , inert_dicts  = emptyCCanMap
584
                         , inert_funeqs = FamHeadMap emptyTM 
dimitris's avatar
dimitris committed
585
                         , inert_irreds = emptyCts }
586
       , inert_insols        = emptyCts
587
       , inert_fsks          = []
588
       , inert_solved_dicts  = PredMap emptyTM 
589
       , inert_solved_funeqs = FamHeadMap emptyTM }
590

591
insertInertItem :: Ct -> InertSet -> InertSet 
592
-- Add a new inert element to the inert set. 
593
insertInertItem item is
594
595
596
597
  = -- A canonical Given, Wanted, or Derived
    ASSERT2( not (isCNonCanonical item), ppr item )
        -- Can't be CNonCanonical, because they only land in inert_insols
    is { inert_cans = upd_inert_cans (inert_cans is) item }
dimitris's avatar
dimitris committed
598
  
599
  where upd_inert_cans :: InertCans -> Ct -> InertCans
dimitris's avatar
dimitris committed
600
601
602
        -- Precondition: item /is/ canonical
        upd_inert_cans ics item
          | isCTyEqCan item                     
603
          = let upd_err a b = pprPanic "insertInertItem" $
dimitris's avatar
dimitris committed
604
605
606
607
608
609
                              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        
610
611

            in ics { inert_eqs = eqs' }
dimitris's avatar
dimitris committed
612
613
614
615
616
617
618
619
620
621
622

          | 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) 
623
                  = panic "insertInertItem: item already there!"
624
            in ics { inert_funeqs = FamHeadMap 
dimitris's avatar
dimitris committed
625
                                      (alterTM fam_head upd_funeqs $ 
626
                                         (unFamHeadMap $ inert_funeqs ics)) }
dimitris's avatar
dimitris committed
627
628
629
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
            ppr item 
630

631
insertInertItemTcS :: Ct -> TcS ()
632
-- Add a new item in the inerts of the monad
633
634
insertInertItemTcS item
  = do { traceTcS "insertInertItemTcS {" $ 
635
636
         text "Trying to insert new inert item:" <+> ppr item

637
       ; updInertTcS (insertInertItem item) 
638
                        
639
       ; traceTcS "insertInertItemTcS }" $ empty }
640

641
addSolvedDict :: CtEvidence -> TcS ()
642
-- Add a new item in the solved set of the monad
643
addSolvedDict item
644
645
646
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
  = return () 
  | otherwise
647
648
649
650
651
652
653
654
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
       ; updInertTcS upd_solved_dicts }
  where
    upd_solved_dicts is 
      = is { inert_solved_dicts = PredMap $ alterTM pred upd_solved $ 
                                  unPredMap $ inert_solved_dicts is }
    pred = ctEvPred item
    upd_solved _ = Just item
655

656
657
addSolvedFunEq :: Ct -> TcType -> TcS ()
addSolvedFunEq fun_eq fam_ty
658
  = updInertTcS upd_solved_funeqs
659
  where 
660
661
    upd_solved_funeqs inert 
      = inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) fam_ty fun_eq }
662

663
664
665
666
667
668
669
670
671
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 }

672
673
674
675
676
677
678
679
680
681
682
updInertTcS :: (InertSet -> InertSet) -> TcS () 
-- Modify the inert set with the supplied function
updInertTcS upd 
  = do { is_var <- getTcSInertsRef
       ; curr_inert <- wrapTcS (TcM.readTcRef is_var)
       ; let new_inert = upd curr_inert
       ; wrapTcS (TcM.writeTcRef is_var new_inert) }

prepareInertsForImplications :: InertSet -> InertSet
-- See Note [Preparing inert set for implications]
prepareInertsForImplications is
683
684
685
  = is { inert_cans   = getGivens (inert_cans is)
       , inert_fsks   = []
       , inert_insols = emptyCts }
686
  where
687
    getGivens (IC { inert_eqs    = eqs
688
689
690
                  , inert_irreds = irreds
                  , inert_funeqs = FamHeadMap funeqs
                  , inert_dicts  = dicts })
691
      = IC { inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
692
693
694
695
696
697
698
699
700
701
           , inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
           , inert_irreds = Bag.filterBag isGivenCt irreds
           , inert_dicts  = keepGivenCMap dicts }

    given_from_wanted funeq   -- This is where the magic processing happens 
      | isGiven ev = funeq    -- for type-function equalities
                              -- See Note [Preparing inert set for implications]
      | otherwise  = funeq { cc_ev = given_ev }
      where
        ev = ctEvidence funeq
Simon Peyton Jones's avatar
Simon Peyton Jones committed
702
703
704
        given_ev = CtGiven { ctev_gloc = setCtLocOrigin (ctev_wloc ev) UnkSkol
                           , ctev_evtm = EvId (ctev_evar ev)
                           , ctev_pred = ctev_pred ev }
705
706
707
708
709
710
711
\end{code}

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

713
714
715
716
With one wrinkle!  We take all *wanted* *funeqs*, and turn them into givens.
Consider (Trac #4935)
   type instance F True a b = a 
   type instance F False a b = b
717

718
719
720
721
722
723
724
725
726
727
   [w] F c a b ~ gamma 
   (c ~ True) => a ~ gamma 
   (c ~ False) => b ~ gamma

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

729
730
Turning type-function equalities into Givens is easy becase they 
*stay inert*.  No need to re-process them.
731

732
We don't try to turn any *other* Wanteds into Givens:
733

734
735
736
  * For example, we should not push given dictionaries in because
    of example LongWayOverlapping.hs, where we might get strange
    overlap errors between far-away constraints in the program.
737

738
739
There might be cases where interactions between wanteds can help
to solve a constraint. For example
740

741
742
  	class C a b | a -> b
  	(C Int alpha), (forall d. C d blah => C Int a)
743

744
745
746
747
If we push the (C Int alpha) inwards, as a given, it can produce a
fundep (alpha~a) and this can float out again and be used to fix
alpha.  (In general we can't float class constraints out just in case
(C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
748
749


750
\begin{code}
751
getInertEqs :: TcS (TyVarEnv Ct)
752
getInertEqs = do { inert <- getTcSInerts
753
                 ; return (inert_eqs (inert_cans inert)) }
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769

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

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

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

770
      ; return (unsolved_flats, inert_insols is) }
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
  where
    add_if_unsolved ct cts
      | is_unsolved ct = cts `extendCts` ct
      | otherwise      = cts

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

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

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

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
792
                     || not (isEmptyBag (inert_insols is)))) }
793

794
795
796
797
798
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
799
800
801
802
803
804
805
806
  = 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 })
807
808
809
810
811
812
813
814
815

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

dimitris's avatar
dimitris committed
816
817
818
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
819

dimitris's avatar
dimitris committed
820
821
822
        extract_ics_relevants _ ics = (emptyCts,ics)
        

823
824
825
826
lookupFlatEqn :: TcType -> TcS (Maybe Ct)
lookupFlatEqn fam_ty 
  = do { IS { inert_solved_funeqs = solved_funeqs
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
Simon Peyton Jones's avatar
Simon Peyton Jones committed
827
828
829
       ; return (lookupFamHead solved_funeqs fam_ty 
                 `firstJust` lookupFamHead inert_funeqs fam_ty  
                )  }
830
831

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

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

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

868

dimitris's avatar
dimitris committed
869
870


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

901
      tcs_inerts   :: IORef InertSet, -- Current inert set
902
903
904
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
905
906
907
      -- while solving or canonicalising the current worklist.
      -- Specifically, when canonicalising (forall a. t1 ~ forall a. t2)
      -- from which we get the implication (forall a. t1 ~ t2)
908
      tcs_implics  :: IORef (Bag Implication)
909
    }
910
911
912
\end{code}

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

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

950
951
952
instance HasDynFlags TcS where
    getDynFlags = wrapTcS getDynFlags

953
954
955
956
957
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

958
traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
959
960
961
962
963
964
965
966
967
-- 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 }
968

969
970
971
972
973
974
975
976
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) }

977
978
979
980
runTcSWithEvBinds :: EvBindsVar
                  -> TcS a 
                  -> TcM a
runTcSWithEvBinds ev_binds_var tcs
981
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
982
       ; step_count <- TcM.newTcRef 0
983
984
       ; inert_var <- TcM.newTcRef is 

985
986
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
987
988
			  , tcs_count    = step_count
			  , tcs_ic_depth = 0
989
                          , tcs_inerts   = inert_var
990
991
992
                          , tcs_worklist    = panic "runTcS: worklist"
                          , tcs_implics     = panic "runTcS: implics" }
                               -- NB: Both these are initialised by withWorkList
993
994

	     -- Run the computation
995
       ; res <- unTcS tcs env
996
997
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
998
       ; mapM_ do_unification (varEnvElts ty_binds)
999

1000
1001
1002
1003
1004
#ifdef DEBUG
       ; count <- TcM.readTcRef step_count
       ; when (opt_PprStyle_Debug && count > 0) $
         TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count )

1005
       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1006
       ; checkForCyclicBinds ev_binds
1007
1008
#endif

1009
       ; return res }
1010
1011
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
1012
1013
    is = emptyInert
    
1014
#ifdef DEBUG
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
checkForCyclicBinds :: Bag EvBind -> TcM ()
checkForCyclicBinds ev_binds
  | null cycles 
  = return ()
  | null coercion_cycles
  = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
  | otherwise
  = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
  where
    cycles :: [[EvBind]]
    cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]

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

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

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

1060
1061
1062
1063
1064
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

1065
tryTcS :: TcS a -> TcS a
1066
1067
1068
-- 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
1069
tryTcS tcs
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
  = 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
1084
1085
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1086
1087
1088
1089
1090
1091
1092
1093
1094
-- 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) 

1095
1096
1097
1098
1099
1100
1101

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

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

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

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

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

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)

1146

1147
emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
1148
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
dimitris's avatar
dimitris committed
1149
emitFrozenError fl depth 
1150
  = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
1151
1152
1153
1154
1155
1156
1157
       ; updInertTcS add_insol }
  where
    add_insol inerts@(IS { inert_insols = old_insols })
      | already_there = inerts
      | otherwise     = inerts { inert_insols = extendCts old_insols insol_ct }
      where
        already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
1158
	     -- See Note [Do not add duplicate derived insolubles]
1159

1160
1161
    insol_ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
    this_pred = ctEvPred fl
1162
1163
1164
1165

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

1166
1167
getUntouchables :: TcS Untouchables
getUntouchables = wrapTcS TcM.getUntouchables
1168

1169
1170
getFlattenSkols :: TcS [TcTyVar]
getFlattenSkols = do { is <- getTcSInerts; return (inert_fsks is) }
1171

1172
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
1173
1174
getTcSTyBinds = TcS (return . tcs_ty_binds)

1175
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
1176
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
1177

1178
1179
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
1180
1181
1182
1183
1184
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
1185
-- We never do this twice!
1186
1187
1188
1189
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
Ian Lynagh's avatar
Ian Lynagh committed
1190
1191
1192
1193
1194
            ; 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)]
1195
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
1196
1197
1198
\end{code}

\begin{code}
1199
1200
1201
1202
1203
warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
warnTcS loc warn_if doc 
  | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
  | otherwise = return ()

1204
1205
getDefaultInfo ::  TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
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
1234

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

1237
1238
isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
isTouchableMetaTyVarTcS tv 
1239
  = do { untch <- getUntouchables
1240
       ; return $ isTouchableMetaTyVar untch tv } 
1241
1242
\end{code}

1243
1244
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245
In general we *do* want to add an insoluble (Int ~ Bool) even if there is one
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
such there already, because they may come from distinct call sites.  But for
*derived* insolubles, we only want to report each one once.  Why?

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

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

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

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

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

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

Assume we have started with an implication:

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

which we have simplified to:

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

For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
1279
dropDerivedWC, then we will end up trying to solve the following
1280
1281
1282
1283
1284
1285
1286
1287
1288
constraints the second time:

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

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

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

1290
1291


1292
\begin{code}
1293
1294
1295
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newFlattenSkolemTy :: TcType -> TcS TcType
1296
newFlattenSkolemTy fam_ty