TcSMonad.lhs 62.7 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
    updTcSImplics, 
23

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

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

30
    canRewrite, canSolve,
31
    mkGivenLoc, 
32

33
    TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality 
34
    traceFireTcS, bumpStepCountTcS, 
35
    tryTcS, nestTcS, nestImplicTcS, recoverTcS,
36 37
    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, isFilledMetaTyVar_maybe,
86 87 88 89 90

    getDefaultInfo, getDynFlags,

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

117
import TcEvidence
118 119
import Class
import TyCon
120

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

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

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

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

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

148

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

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

159 160
\end{code}

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

170 171 172 173 174
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. 
175

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

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

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

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

196
\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
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"
221

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

batterseapower's avatar
batterseapower committed
228

Simon Peyton Jones's avatar
Simon Peyton Jones committed
229 230 231 232 233
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 }
234

235

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

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

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

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

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

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

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

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

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

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

dimitris's avatar
dimitris committed
281 282 283 284 285

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
286 287
      (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
                       -> (Just ct, wl { wl_funeqs = fun_eqs' })
dimitris's avatar
dimitris committed
288 289 290
      (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
      (_,_,_)          -> (Nothing,wl)

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


dimitris's avatar
dimitris committed
299
-- Canonical constraint maps
300 301 302 303 304 305 306
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 }
307

308 309 310
instance Outputable (CCanMap a) where
  ppr (CCanMap given derived wanted) = ptext (sLit "CCanMap") <+> (ppr given) <+> (ppr derived) <+> (ppr wanted)

311 312 313 314 315 316 317 318 319 320
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 
321
  = case cc_ev ct of 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
322 323 324
      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) }
325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340
  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

341 342 343 344 345 346 347
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))
348

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

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

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

381 382 383 384
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)
385

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

394 395 396 397 398
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 [])
399

400 401 402 403 404 405
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

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

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

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

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

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

\begin{code}
451
-- All Given (fully known) or Wanted or Derived
dimitris's avatar
dimitris committed
452 453 454 455 456 457 458 459 460 461 462 463 464 465 466
-- 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
467 468 469

       , inert_insols :: Cts       
              -- Frozen errors (as non-canonicals)
dimitris's avatar
dimitris committed
470 471 472 473 474 475 476 477 478 479 480
       }
    
                     
\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
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 507 508 509 510 511
  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
512 513
  9 Given family or dictionary constraints don't mention touchable unification variables

514 515 516 517 518 519 520 521 522 523 524 525 526 527
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

528 529 530 531
* 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
532

533 534

\begin{code}
dimitris's avatar
dimitris committed
535 536 537
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
538 539 540
              -- Canonical Given, Wanted, Derived (no Solved)
	      -- Sometimes called "the inert set"

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

547 548 549 550
       , 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 
551

552 553 554
       , inert_solved_dicts   :: PredMap CtEvidence 
       	      -- Of form ev :: C t1 .. tn
              -- Always the result of using a top-level instance declaration
555
              -- See Note [Solved constraints]
556 557
       	      -- - 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
558
       	      -- - Stored not necessarily as fully rewritten 
559
       	      --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
560
       }
561 562


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

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

593
insertInertItem :: Ct -> InertSet -> InertSet 
594
-- Add a new inert element to the inert set. 
595
insertInertItem item is
596 597
  = -- A canonical Given, Wanted, or Derived
    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
          | otherwise
          = pprPanic "upd_inert set: can't happen! Inserting " $ 
629 630 631
            ppr item   -- Can't be CNonCanonical, CHoleCan, 
                       -- because they only land in inert_insols

632

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

639
       ; updInertTcS (insertInertItem item) 
640
                        
641
       ; traceTcS "insertInertItemTcS }" $ empty }
642

643
addSolvedDict :: CtEvidence -> TcS ()
644
-- Add a new item in the solved set of the monad
645
addSolvedDict item
646 647 648
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
  = return () 
  | otherwise
649 650 651 652 653 654 655 656
  = 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
657

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

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

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

    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
704
        given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
705
                           , ctev_pred = ctev_pred ev }
706 707 708 709 710 711 712
\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
713

714 715 716 717
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
718

719 720 721 722 723 724 725 726 727 728
   [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.  
729

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

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

735 736 737
  * 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.
738

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

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

745 746 747 748
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.
749 750


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

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

771
      ; return (unsolved_flats, inert_insols icans) }
772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792
  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
793
                     || not (isEmptyBag (inert_insols icans)))) }
794

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

        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)

817 818 819 820
        extract_ics_relevants (CHoleCan {}) ics
            = pprPanic "extractRelevantInerts" (ppr wi)
              -- Holes are put straight into inert_frozen, so never get here

dimitris's avatar
dimitris committed
821 822 823
        extract_ics_relevants (CIrredEvCan { }) ics = 
            let cts = inert_irreds ics 
            in (cts, ics { inert_irreds = emptyCts })
824

dimitris's avatar
dimitris committed
825 826 827
        extract_ics_relevants _ ics = (emptyCts,ics)
        

828 829 830 831
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
832 833 834
       ; return (lookupFamHead solved_funeqs fam_ty 
                 `firstJust` lookupFamHead inert_funeqs fam_ty  
                )  }
835 836

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

844
lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
845
-- Returns just if exactly this predicate type exists in the solved.
846
lookupInSolved tm pty = lookupTM pty $ unPredMap tm
dimitris's avatar
dimitris committed
847

848
lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
dimitris's avatar
dimitris committed
849 850
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans ics pty
851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869
  = 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)
    
870
      _other -> Nothing -- NB: No caching for IPs or holes
871 872
\end{code}

873

dimitris's avatar
dimitris committed
874 875


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

905
      tcs_inerts   :: IORef InertSet, -- Current inert set
906 907 908
      tcs_worklist :: IORef WorkList, -- Current worklist
      
      -- Residual implication constraints that are generated 
909 910 911
      -- 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)
912
      tcs_implics  :: IORef (Bag Implication)
913
    }
914 915 916
\end{code}

\begin{code}
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 948 949 950 951

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

954 955 956
instance HasDynFlags TcS where
    getDynFlags = wrapTcS getDynFlags

957 958 959 960 961
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                    ; n <- TcM.readTcRef ref
                                    ; TcM.writeTcRef ref (n+1) }

962
traceFireTcS :: Ct -> SDoc -> TcS ()
963
-- Dump a rule-firing trace
964
traceFireTcS ct doc 
965 966 967
  = TcS $ \env -> 
    TcM.ifDOptM Opt_D_dump_cs_trace $ 
    do { n <- TcM.readTcRef (tcs_count env)
968
       ; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
969
       ; TcM.dumpTcRn msg }
970

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

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

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

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

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

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

1010
       ; return res }
1011 1012
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
1013 1014
    is = emptyInert
    
1015
#ifdef DEBUG
1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033
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