TcSMonad.hs 65.7 KB
Newer Older
1 2
{-# LANGUAGE CPP, TypeFamilies #-}

3
-- Type definitions for the constraint solver
4
module TcSMonad (
5

6
    -- The work list
7
    WorkList(..), isEmptyWorkList, emptyWorkList,
8
    extendWorkListNonEq, extendWorkListCt,
9 10
    extendWorkListCts, appendWorkList, selectWorkItem,
    workListSize,
Adam Gundry's avatar
Adam Gundry committed
11
    updWorkListTcS, updWorkListTcS_return,
12
    runFlatten, emitFlatWork,
13

14 15 16
    -- The TcS monad
    TcS, runTcS, runTcSWithEvBinds,
    failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
17

18
    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
19

20 21
    -- Tracing etc
    panicTcS, traceTcS,
22
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
23
    wrapErrTcS, wrapWarnTcS,
24

25
    -- Evidence creation and transformation
dimitris's avatar
dimitris committed
26
    XEvTerm(..),
27
    Freshness(..), freshGoals, isFresh,
28

Austin Seipp's avatar
Austin Seipp committed
29
    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
30 31
    setWantedTyBind, reportUnifications,
    setEvBind,
32 33
    newEvVar, newGivenEvVar, newGivenEvVars,
    newDerived, emitNewDerived,
34

35
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
36
    getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
37
    getTcEvBindsMap,
38

39 40
        -- Inerts
    InertSet(..), InertCans(..),
41
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
42
    getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
Austin Seipp's avatar
Austin Seipp committed
43
    emptyInert, getTcSInerts, setTcSInerts,
44
    getUnsolvedInerts, checkAllSolved,
Adam Gundry's avatar
Adam Gundry committed
45
    splitInertCans, removeInertCts,
46
    prepareInertsForImplications,
47
    addInertCan, insertInertItemTcS, insertFunEq,
48
    emitInsoluble, emitWorkNC,
49
    EqualCtList,
50

51
    -- Inert CDictCans
52
    lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
53

54 55 56 57 58 59 60 61 62 63 64
    -- Inert CTyEqCans
    findTyEqs,

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems

    -- Inert CFunEqCans
    updInertFunEqs, findFunEq, sizeFunEqMap,
65
    findFunEqsByTyCon, findFunEqs, partitionFunEqs,
66

67
    instDFunType,                              -- Instantiation
68 69

    -- MetaTyVars
70
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
71
    cloneMetaTyVar, demoteUnfilledFmv,
72

73
    TcLevel, isTouchableMetaTyVarTcS,
74
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
75
    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples,
76

77 78
    -- References
    newTcRef, readTcRef, updTcRef,
79

80 81
    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
Adam Gundry's avatar
Adam Gundry committed
82
    matchFam, matchFamTcM,
83
    checkWellStagedDFun,
84
    pprEq                                    -- Smaller utils, re-exported from TcM
85
                                             -- TODO (DV): these are only really used in the
86 87
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
88 89
                                             -- here
) where
90 91 92 93 94

#include "HsVersions.h"

import HscTypes

95
import qualified Inst as TcM
96 97
import InstEnv
import FamInst
98 99 100 101
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
102
import qualified TcEnv as TcM
103
       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
104
import Kind
105 106
import TcType
import DynFlags
107
import Type
108

109
import TcEvidence
110 111
import Class
import TyCon
112

113
import Name
114 115
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
116
import Var
117
import VarEnv
118
import VarSet
119 120
import Outputable
import Bag
121
import UniqSupply
122

123
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
124
import Util
Ian Lynagh's avatar
Ian Lynagh committed
125
import TcRnTypes
126

127
import Unique
128
import UniqFM
129
import Maybes ( orElse, firstJusts )
130

131
import TrieMap
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
132
import Control.Arrow ( first )
133
import Control.Monad( ap, when, unless, MonadPlus(..) )
134
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
135
import Data.IORef
Adam Gundry's avatar
Adam Gundry committed
136
import Data.List ( partition, foldl' )
137

138 139 140
#ifdef DEBUG
import Digraph
#endif
141

Austin Seipp's avatar
Austin Seipp committed
142 143 144 145 146 147 148 149 150
{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************
151

152 153
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
154 155 156
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.
157

158
As a simple form of priority queue, our worklist separates out
159 160 161 162
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.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
163

164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
Note [The flattening work list]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "flattening work list", held in the tcs_flat_work field of TcSEnv,
is a list of CFunEqCans generated during flattening.  The key idea
is this.  Consider flattening (Eq (F (G Int) (H Bool)):
  * The flattener recursively calls itself on sub-terms before building
    the main term, so it will encounter the terms in order
              G Int
              H Bool
              F (G Int) (H Bool)
    flattening to sub-goals
              w1: G Int ~ fuv0
              w2: H Bool ~ fuv1
              w3: F fuv0 fuv1 ~ fuv2

  * Processing w3 first is BAD, because we can't reduce i t,so it'll
    get put into the inert set, and later kicked out when w1, w2 are
    solved.  In Trac #9872 this led to inert sets containing hundreds
    of suspended calls.

  * So we want to process w1, w2 first.

  * So you might think that we should just use a FIFO deque for the work-list,
    so that putting adding goals in order w1,w2,w3 would mean we processed
    w1 first.

  * BUT suppose we have 'type instance G Int = H Char'.  Then processing
    w1 leads to a new goal
                w4: H Char ~ fuv0
    We do NOT want to put that on the far end of a deque!  Instead we want
    to put it at the *front* of the work-list so that we continue to work
    on it.

So the work-list structure is this:

  * The wl_funeqs is a LIFO stack; we push new goals (such as w4) on
    top (extendWorkListFunEq), and take new work from the top
    (selectWorkItem).

  * When flattening, emitFlatWork pushes new flattening goals (like
    w1,w2,w3) onto the flattening work list, tcs_flat_work, another
    push-down stack.

  * When we finish flattening, we *reverse* the tcs_flat_work stack
    onto the wl_funeqs stack (which brings w1 to the top).

The function runFlatten initialised the tcs_flat_work stack, and reverses
it onto wl_fun_eqs at the end.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
212

213
-}
214

215
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
216
data WorkList
217
  = WL { wl_eqs     :: [Ct]
218
       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
219 220 221
       , wl_rest    :: [Ct]
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
222

Simon Peyton Jones's avatar
Simon Peyton Jones committed
223
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
224
appendWorkList
225 226
    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
227 228 229
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
230
        , wl_implics = implics1 `unionBags`   implics2 }
231

232

233
workListSize :: WorkList -> Int
234
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
235
  = length eqs + length funeqs + length rest
236

237
extendWorkListEq :: Ct -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
238
extendWorkListEq ct wl
dimitris's avatar
dimitris committed
239
  = wl { wl_eqs = ct : wl_eqs wl }
240

241
extendWorkListFunEq :: Ct -> WorkList -> WorkList
242
extendWorkListFunEq ct wl
243
  = wl { wl_funeqs = ct : wl_funeqs wl }
244

245 246
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
247
extendWorkListNonEq ct wl
248
  = wl { wl_rest = ct : wl_rest wl }
249

250 251 252 253
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl
  = wl { wl_implics = implic `consBag` wl_implics wl }

254 255 256
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
257
 = case classifyPredType (ctPred ct) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
258
     EqPred NomEq ty1 _
259
       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
260
       , isTypeFamilyTyCon tc
261
       -> extendWorkListFunEq ct wl
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
262
     EqPred {}
263 264 265
       -> extendWorkListEq ct wl

     _ -> extendWorkListNonEq ct wl
266

Simon Peyton Jones's avatar
Simon Peyton Jones committed
267
extendWorkListCts :: [Ct] -> WorkList -> WorkList
268
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
269
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
270 271

isEmptyWorkList :: WorkList -> Bool
272 273
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
                    , wl_rest = rest, wl_implics = implics })
274
  = null eqs && null rest && null funeqs && isEmptyBag implics
275 276

emptyWorkList :: WorkList
277
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
278
                   , wl_funeqs = [], wl_implics = emptyBag }
dimitris's avatar
dimitris committed
279 280

selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
281
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
dimitris's avatar
dimitris committed
282
  = case (eqs,feqs,rest) of
283 284 285 286
      (ct:cts,_,_) -> (Just ct, wl { wl_eqs    = cts })
      (_,ct:fes,_) -> (Just ct, wl { wl_funeqs = fes })
      (_,_,ct:cts) -> (Just ct, wl { wl_rest   = cts })
      (_,_,_)      -> (Nothing,wl)
dimitris's avatar
dimitris committed
287

288 289
-- Pretty printing
instance Outputable WorkList where
290 291 292
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
          , wl_rest = rest, wl_implics = implics })
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
293
     vcat [ ppUnless (null eqs) $
294
            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
295 296
          , ppUnless (null feqs) $
            ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
297
          , ppUnless (null rest) $
298
            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
299 300 301
          , ppUnless (isEmptyBag implics) $
            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
          ])
dimitris's avatar
dimitris committed
302

303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
emitFlatWork :: Ct -> TcS ()
-- See Note [The flattening work list]
emitFlatWork ct
  = TcS $ \env ->
    do { let flat_ref = tcs_flat_work env
       ; TcM.updTcRef flat_ref (ct :) }

runFlatten :: TcS a -> TcS a
-- Run thing_inside (which does flattening), and put all
-- the work it generates onto the main work list
-- See Note [The flattening work list]
runFlatten (TcS thing_inside)
  = TcS $ \env ->
    do { let flat_ref = tcs_flat_work env
       ; old_flats <- TcM.updTcRefX flat_ref (\_ -> [])
       ; res <- thing_inside env
       ; new_flats <- TcM.updTcRefX flat_ref (\_ -> old_flats)
       ; TcM.updTcRef (tcs_worklist env) (add_flats new_flats)
       ; return res }
  where
    add_flats new_flats wl
      = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }

    add_funeqs []     wl = wl
    add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
      -- add_funeqs fs ws = reverse fs ++ ws
      -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
      --        = [f3,f2,f1,w1,w2,w3,w4]

Austin Seipp's avatar
Austin Seipp committed
332 333 334 335 336 337 338
{-
************************************************************************
*                                                                      *
*                            Inert Sets                                *
*                                                                      *
*                                                                      *
************************************************************************
dimitris's avatar
dimitris committed
339 340 341 342

Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
343

344
  * All canonical
345

346 347 348 349 350 351 352 353 354 355 356 357 358 359
  * No two dictionaries with the same head
  * No two CIrreds with the same type

  * Family equations inert wrt top-level family axioms

  * Dictionaries have no matching top-level instance

  * Given family or dictionary constraints don't mention touchable
    unification variables

  * Non-CTyEqCan constraints are fully rewritten with respect
    to the CTyEqCan equalities (modulo canRewrite of course;
    eg a wanted cannot rewrite a given)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
360 361
  * CTyEqCan equalities: see Note [Applying the inert substitution]
                         in TcFlatten
362

363 364
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
365
Type-family equations, of form (ev : F tys ~ ty), live in three places
366 367 368 369 370 371 372

  * The work-list, of course

  * The inert_flat_cache.  This is used when flattening, to get maximal
    sharing.  It contains lots of things that are still in the work-list.
    E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
        work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
373
        list.  Now if we flatten w2 before we get to w3, we still want to
374 375 376
        share that (G a).

    Because it contains work-list things, DO NOT use the flat cache to solve
377 378
    a top-level goal.  Eg in the above example we don't want to solve w3
    using w3 itself!
379

380
  * The inert_funeqs are un-solved but fully processed and in the InertCans.
Austin Seipp's avatar
Austin Seipp committed
381
-}
382 383 384

-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
385
data InertCans
386
  = IC { inert_eqs :: TyVarEnv EqualCtList
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
387
              -- All CTyEqCans with NomEq; index is the LHS tyvar
388

389
       , inert_funeqs :: FunEqMap Ct
390 391 392
              -- All CFunEqCans; index is the whole family head type.

       , inert_dicts :: DictMap Ct
393
              -- Dictionaries only, index is the class
394
              -- NB: index is /not/ the whole type because FD reactions
395
              -- need to match the class but not necessarily the whole type.
396

397
       , inert_irreds :: Cts
398 399
              -- Irreducible predicates

400
       , inert_insols :: Cts
401 402
              -- Frozen errors (as non-canonicals)
       }
403

404
type EqualCtList = [Ct]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
405 406 407 408 409 410 411 412 413 414 415 416
{-
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * All are equalities
    * All these equalities have the same LHS
    * The list is never empty
    * No element of the list can rewrite any other

 From the fourth invariant it follows that the list is
   - A single Given, or
   - Any number of Wanteds and/or Deriveds
-}
417

dimitris's avatar
dimitris committed
418 419 420
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
421
              -- Canonical Given, Wanted, Derived (no Solved)
422
              -- Sometimes called "the inert set"
423

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
424
       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
425
              -- See Note [Type family equations]
426 427 428
              -- If    F tys :-> (co, ty, ev),
              -- then  co :: F tys ~ ty
              --
429 430 431 432 433
              -- Just a hash-cons cache for use when flattening only
              -- These include entirely un-processed goals, so don't use
              -- them to solve a top-level goal, else you may end up solving
              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
              -- when allocating a new flatten-skolem.
434
              -- Not necessarily inert wrt top-level equations (or inert_cans)
435

436
       , inert_solved_dicts   :: DictMap CtEvidence
437
              -- Of form ev :: C t1 .. tn
438
              -- Always the result of using a top-level instance declaration
439 440 441 442
              -- - Used to avoid creating a new EvVar when we have a new goal
              --   that we have solved in the past
              -- - Stored not necessarily as fully rewritten
              --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
443
       }
444

445 446
instance Outputable InertCans where
  ppr ics = vcat [ ptext (sLit "Equalities:")
447 448
                   <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
                                          emptyCts (inert_eqs ics))
449
                 , ptext (sLit "Type-function equalities:")
450
                   <+> pprCts (funEqsToBag (inert_funeqs ics))
451
                 , ptext (sLit "Dictionaries:")
452
                   <+> pprCts (dictsToBag (inert_dicts ics))
453
                 , ptext (sLit "Irreds:")
454
                   <+> pprCts (inert_irreds ics)
455 456
                 , text "Insolubles =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
dimitris's avatar
dimitris committed
457
                 ]
458 459

instance Outputable InertSet where
dimitris's avatar
dimitris committed
460
  ppr is = vcat [ ppr $ inert_cans is
461
                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
462

dimitris's avatar
dimitris committed
463 464
emptyInert :: InertSet
emptyInert
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
465 466 467 468 469
  = IS { inert_cans = IC { inert_eqs      = emptyVarEnv
                         , inert_dicts    = emptyDicts
                         , inert_funeqs   = emptyFunEqs
                         , inert_irreds   = emptyCts
                         , inert_insols   = emptyCts
470 471 472
                         }
       , inert_flat_cache    = emptyFunEqs
       , inert_solved_dicts  = emptyDictMap }
473

474 475 476
---------------
addInertCan :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
477
addInertCan ics item@(CTyEqCan {})
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
478 479 480 481 482 483
  = ics { inert_eqs = add_eq (inert_eqs ics) item }
  where
    add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList
    add_eq old_list it
      = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
                       old_list (cc_tyvar it) [it]
484

485 486
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
487 488

addInertCan ics item@(CIrredEvCan {})
489
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
490 491 492 493 494
       -- The 'False' is because the irreducible constraint might later instantiate
       -- to an equality.
       -- But since we try to simplify first, if there's a constraint function FC with
       --    type instance FC Int = Show
       -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
495 496 497

addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
  = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
498

499 500 501 502 503 504
addInertCan _ item
  = pprPanic "upd_inert set: can't happen! Inserting " $
    ppr item   -- Can't be CNonCanonical, CHoleCan,
               -- because they only land in inert_insols

--------------
505
insertInertItemTcS :: Ct -> TcS ()
506
-- Add a new item in the inerts of the monad
507
insertInertItemTcS item
508
  = do { traceTcS "insertInertItemTcS {" $
509 510
         text "Trying to insert new inert item:" <+> ppr item

511
       ; updInertCans (\ics -> addInertCan ics item)
512

513
       ; traceTcS "insertInertItemTcS }" $ empty }
514

515
addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
516
-- Add a new item in the solved set of the monad
517
addSolvedDict item cls tys
518
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
519
  = return ()
520
  | otherwise
521
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
522 523
       ; updInertTcS $ \ ics ->
             ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
524

525
updInertTcS :: (InertSet -> InertSet) -> TcS ()
526
-- Modify the inert set with the supplied function
527
updInertTcS upd_fn
528
  = do { is_var <- getTcSInertsRef
529
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
530
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
531

532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559
getInertCans :: TcS InertCans
getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }

setInertCans :: InertCans -> TcS ()
setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }

updInertCans :: (InertCans -> InertCans) -> TcS ()
-- Modify the inert set with the supplied function
updInertCans upd_fn
  = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }

updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertDicts upd_fn
  = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }

updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertFunEqs upd_fn
  = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }

updInertIrreds :: (Cts -> Cts) -> TcS ()
-- Modify the inert set with the supplied function
updInertIrreds upd_fn
  = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }


prepareInertsForImplications :: InertSet -> (InertSet)
560
-- See Note [Preparing inert set for implications]
561 562 563
prepareInertsForImplications is@(IS { inert_cans = cans })
  = is { inert_cans       = getGivens cans
       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
564
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
565 566 567 568 569 570 571 572 573
    getGivens (IC { inert_eqs      = eqs
                  , inert_irreds   = irreds
                  , inert_funeqs   = funeqs
                  , inert_dicts    = dicts })
      = IC { inert_eqs      = filterVarEnv  is_given_ecl eqs
           , inert_funeqs   = filterFunEqs  isGivenCt funeqs
           , inert_irreds   = Bag.filterBag isGivenCt irreds
           , inert_dicts    = filterDicts   isGivenCt dicts
           , inert_insols   = emptyCts }
574

575 576 577
    is_given_ecl :: EqualCtList -> Bool
    is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
    is_given_ecl _                        = False
578

Austin Seipp's avatar
Austin Seipp committed
579
{-
580 581 582 583 584 585 586
Note [Do not inherit the flat cache]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do not want to inherit the flat cache when processing nested
implications.  Consider
   a ~ F b, forall c. b~Int => blah
If we have F b ~ fsk in the flat-cache, and we push that into the
nested implication, we might miss that F b can be rewritten to F Int,
Austin Seipp's avatar
Austin Seipp committed
587 588
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
589 590
do that flattening recursively.

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

597 598
There might be cases where interactions between wanteds at different levels
could help to solve a constraint. For example
599

600 601
        class C a b | a -> b
        (C Int alpha), (forall d. C d blah => C Int a)
602

603
If we pushed the (C Int alpha) inwards, as a given, it can produce a
604 605 606
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.
607

608 609
For Derived constraints we don't have evidence, so we do not turn
them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
Austin Seipp's avatar
Austin Seipp committed
610
-}
611

612
getInertEqs :: TcS (TyVarEnv EqualCtList)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
613 614 615
getInertEqs
  = do { inert <- getTcSInerts
       ; return (inert_eqs (inert_cans inert)) }
616

617 618
getUnsolvedInerts :: TcS ( Bag Implication
                         , Cts     -- Tyvar eqs: a ~ ty
619 620 621 622
                         , Cts     -- Fun eqs:   F a ~ ty
                         , Cts     -- Insoluble
                         , Cts )   -- All others
getUnsolvedInerts
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
623 624
 = do { IC { inert_eqs    = tv_eqs
           , inert_funeqs = fun_eqs
625 626 627
           , inert_irreds = irreds, inert_dicts = idicts
           , inert_insols = insols } <- getInertCans

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
628 629
      ; let unsolved_tv_eqs   = foldVarEnv (\cts rest ->
                                             foldr add_if_unsolved rest cts)
630
                                          emptyCts tv_eqs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
631 632 633 634 635
            unsolved_fun_eqs  = foldFunEqs add_if_unsolved fun_eqs emptyCts
            unsolved_irreds   = Bag.filterBag is_unsolved irreds
            unsolved_dicts    = foldDicts add_if_unsolved idicts emptyCts

            others       = unsolved_irreds `unionBags` unsolved_dicts
636

637 638 639
      ; implics <- getWorkListImplics

      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
640 641
              -- Keep even the given insolubles
              -- so that we can report dead GADT pattern match branches
642
  where
643
    add_if_unsolved :: Ct -> Cts -> Cts
644
    add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
645 646
                           | otherwise      = cts

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

649
getNoGivenEqs :: TcLevel     -- TcLevel of this implication
650 651 652
               -> [TcTyVar]       -- Skolems of this implication
               -> TcS Bool        -- True <=> definitely no residual given equalities
-- See Note [When does an implication have given equalities?]
653
getNoGivenEqs tclvl skol_tvs
654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674
  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
             <- getInertCans
       ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet

             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence)  False iirreds
                          || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs

       ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
       ; return (not has_given_eqs) }
  where
    eqs_given_here :: VarSet -> EqualCtList -> Bool
    eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
                              -- Givens are always a sigleton
      = not (skolem_bound_here local_fsks tv) && ev_given_here ev
    eqs_given_here _ _ = False

    ev_given_here :: CtEvidence -> Bool
    -- True for a Given bound by the curent implication,
    -- i.e. the current level
    ev_given_here ev
      =  isGiven ev
675
      && tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
676 677 678 679 680 681 682 683 684 685 686 687 688

    add_fsk :: Ct -> VarSet -> VarSet
    add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
                    , isGiven ev = extendVarSet fsks tv
                    | otherwise  = fsks

    skol_tv_set = mkVarSet skol_tvs
    skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
      = case tcTyVarDetails tv of
          SkolemTv {} -> tv `elemVarSet` skol_tv_set
          FlatSkol {} -> not (tv `elemVarSet` local_fsks)
          _           -> False

Austin Seipp's avatar
Austin Seipp committed
689
{-
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
   beta => alpha ~ Int
where beta is a unification variable that has already been unified
to () in an outer scope.  Then we can float the (alpha ~ Int) out
just fine. So when deciding whether the givens contain an equality,
we should canonicalise first, rather than just looking at the original
givens (Trac #8644).

So we simply look at the inert, canonical Givens and see if there are
any equalities among them, the calculation of has_given_eqs.  There
are some wrinkles:

 * We must know which ones are bound in *this* implication and which
705 706
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729
   of the TcLclEnv stored in the Given (ev_given_here).

   What about interactions between inner and outer givens?
      - Outer given is rewritten by an inner given, then there must
        have been an inner given equality, hence the “given-eq” flag
        will be true anyway.

      - Inner given rewritten by outer, retains its level (ie. The inner one)

 * We must take account of *potential* equalities, like the one above:
      beta => ...blah...
   If we still don't know what beta is, we conservatively treat it as potentially
   becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.

 * When flattening givens, we generate Given equalities like
     <F [a]> : F [a] ~ f,
   with Refl evidence, and we *don't* want those to count as an equality
   in the givens!  After all, the entire flattening business is just an
   internal matter, and the evidence does not mention any of the 'givens'
   of this implication.  So we do not treat inert_funeqs as a 'given equality'.

 * See Note [Let-bound skolems] for another wrinkle

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
730 731 732
 * We do *not* need to worry about representational equalities, because
   these do not affect the ability to float constraints.

733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and  * 'a' is a skolem bound in this very implication, b

then:
a) The Given is pretty much a let-binding, like
      f :: (a ~ b->c) => a -> a
   Here the equality constraint is like saying
      let a = b->c in ...
   It is not adding any new, local equality  information,
   and hence can be ignored by has_given_eqs

b) 'a' will have been completely substituted out in the inert set,
   so we can safely discard it.  Notably, it doesn't need to be
   returned as part of 'fsks'

For an example, see Trac #9211.
Austin Seipp's avatar
Austin Seipp committed
751
-}
752

Adam Gundry's avatar
Adam Gundry committed
753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
-- ^ Extract the (given, derived, wanted) inert constraints
splitInertCans iCans = (given,derived,wanted)
  where
    allCts   = foldDicts  (:) (inert_dicts iCans)
             $ foldFunEqs (:) (inert_funeqs iCans)
             $ concat (varEnvElts (inert_eqs iCans))

    (derived,other) = partition isDerivedCt allCts
    (wanted,given)  = partition isWantedCt  other

removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
-- typechecker plugin wishes to discard a given.
removeInertCts cts icans = foldl' removeInertCt icans cts

removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
  case ct of

    CDictCan  { cc_class = cl, cc_tyargs = tys } ->
      is { inert_dicts = delDict (inert_dicts is) cl tys }

    CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
      is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
779 780
    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
      is { inert_eqs    = delTyEq (inert_eqs is) x ty }
Adam Gundry's avatar
Adam Gundry committed
781 782 783 784 785 786

    CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
    CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
    CHoleCan {}      -> panic "removeInertCt: CHoleCan"


787 788 789 790 791 792 793
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
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
794 795 796 797 798 799 800
            unsolved_irreds  = Bag.anyBag isWantedCt (inert_irreds icans)
            unsolved_dicts   = foldDicts  ((||)  . isWantedCt)
                                          (inert_dicts icans)  False
            unsolved_funeqs  = foldFunEqs ((||) . isWantedCt)
                                          (inert_funeqs icans) False
            unsolved_eqs     = foldVarEnv ((||) . any isWantedCt) False
                                          (inert_eqs icans)
801 802 803

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
804
                     || not (isEmptyBag (inert_insols icans)))) }
805

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
806
lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
807 808
lookupFlatCache fam_tc tys
  = do { IS { inert_flat_cache = flat_cache
809
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
810 811
       ; return (firstJusts [lookup_inerts inert_funeqs,
                             lookup_flats flat_cache]) }
812
  where
813
    lookup_inerts inert_funeqs
814 815
      | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
           <- findFunEqs inert_funeqs fam_tc tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
816
      = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
817 818 819 820
      | otherwise = Nothing

    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys

821

822
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
823
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
824
lookupInInerts loc pty
825
  | ClassPred cls tys <- classifyPredType pty
826
  = do { inerts <- getTcSInerts
827 828 829 830
       ; return (lookupSolvedDict inerts loc cls tys `mplus`
                 lookupInertDict (inert_cans inerts) loc cls tys) }
  | otherwise -- NB: No caching for equalities, IPs, holes, or errors
  = return Nothing
831

832 833 834 835 836 837 838 839 840
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
  = case findDict dicts cls tys of
      Just ct | let ev = ctEvidence ct
              , ctEvCheckDepth cls loc ev
              -> Just ev
      _       -> Nothing

lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
841
-- Returns just if exactly this predicate type exists in the solved.
842 843 844 845
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
  = case findDict solved cls tys of
      Just ev | ctEvCheckDepth cls loc ev -> Just ev
      _                                   -> Nothing
846

Austin Seipp's avatar
Austin Seipp committed
847 848 849
{-
************************************************************************
*                                                                      *
850
                   TyEqMap
Austin Seipp's avatar
Austin Seipp committed
851 852 853
*                                                                      *
************************************************************************
-}
854 855 856

type TyEqMap a = TyVarEnv a

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
857 858
findTyEqs :: InertCans -> TyVar -> EqualCtList
findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
Adam Gundry's avatar
Adam Gundry committed
859 860 861 862 863

delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
        isThisOne _                          = False
864

Austin Seipp's avatar
Austin Seipp committed
865 866 867
{-
************************************************************************
*                                                                      *
868
                   TcAppMap, DictMap, FunEqMap
Austin Seipp's avatar
Austin Seipp committed
869 870 871
*                                                                      *
************************************************************************
-}
872