TcSMonad.hs 76.5 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 29

    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
30

31 32
    xCtEvidence,        -- Transform a CtEvidence during a step
    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
33 34 35
    rewriteEqEvidence,  -- Yet more specialised, for equality coercions
    maybeSym,

Austin Seipp's avatar
Austin Seipp committed
36
    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
37 38
    setWantedTyBind, reportUnifications,
    setEvBind,
Austin Seipp's avatar
Austin Seipp committed
39
    newEvVar, newGivenEvVar,
40
    emitNewDerived, emitNewDerivedEq,
41
    instDFunConstraints,
42

43
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
44
    getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
45
    getTcEvBindsMap,
46

47 48
        -- Inerts
    InertSet(..), InertCans(..),
49
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
50
    getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
Austin Seipp's avatar
Austin Seipp committed
51
    emptyInert, getTcSInerts, setTcSInerts,
52
    getUnsolvedInerts, checkAllSolved,
Adam Gundry's avatar
Adam Gundry committed
53
    splitInertCans, removeInertCts,
54
    prepareInertsForImplications,
55
    addInertCan, insertInertItemTcS, insertFunEq,
56
    emitInsoluble, emitWorkNC,
57
    EqualCtList,
58

59
    -- Inert CDictCans
60
    lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
61

62 63 64 65 66 67 68 69 70 71 72
    -- Inert CTyEqCans
    findTyEqs,

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

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

    -- Inert CFunEqCans
    updInertFunEqs, findFunEq, sizeFunEqMap,
73
    findFunEqsByTyCon, findFunEqs, partitionFunEqs,
74

75
    instDFunType,                              -- Instantiation
76 77

    -- MetaTyVars
78
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
79
    cloneMetaTyVar, demoteUnfilledFmv,
80

81
    TcLevel, isTouchableMetaTyVarTcS,
82 83
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
84

85 86
    -- References
    newTcRef, readTcRef, updTcRef,
87

88 89
    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
90
    matchFam,
91
    checkWellStagedDFun,
92
    pprEq                                    -- Smaller utils, re-exported from TcM
93
                                             -- TODO (DV): these are only really used in the
94 95
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
96 97
                                             -- here
) where
98 99 100 101 102 103

#include "HsVersions.h"

import HscTypes

import Inst
104 105
import InstEnv
import FamInst
106 107 108 109
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
110
import qualified TcEnv as TcM
111
       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
112
import Kind
113 114
import TcType
import DynFlags
115
import Type
116
import CoAxiom(sfMatchFam)
117

118
import TcEvidence
119 120
import Class
import TyCon
121

122
import Name
123 124
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
125
import Var
126
import VarEnv
127
import VarSet
128 129
import Outputable
import Bag
130
import UniqSupply
131

132
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
133
import Util
134
import Id
Ian Lynagh's avatar
Ian Lynagh committed
135
import TcRnTypes
136

137
import BasicTypes
138
import Unique
139
import UniqFM
140
import Maybes ( orElse, firstJusts )
141

142
import TrieMap
143 144
import Control.Monad( ap, when, unless )
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
145
import Data.IORef
Adam Gundry's avatar
Adam Gundry committed
146
import Data.List ( partition, foldl' )
147
import Pair
148

149 150 151
#ifdef DEBUG
import Digraph
#endif
152

Austin Seipp's avatar
Austin Seipp committed
153 154 155 156 157 158 159 160 161
{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************
162

163 164
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
165 166 167
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.
168

169
As a simple form of priority queue, our worklist separates out
170 171 172 173
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
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 212 213 214 215 216 217 218 219 220 221 222
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
223

224
-}
225

226
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
227
data WorkList
228
  = WL { wl_eqs     :: [Ct]
229
       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
230 231 232
       , wl_rest    :: [Ct]
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
233

Simon Peyton Jones's avatar
Simon Peyton Jones committed
234
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
235
appendWorkList
236 237
    (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 })
238 239 240
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
241
        , wl_implics = implics1 `unionBags`   implics2 }
242

243

244
workListSize :: WorkList -> Int
245
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
246
  = length eqs + length funeqs + length rest
247

248
extendWorkListEq :: Ct -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
249
extendWorkListEq ct wl
dimitris's avatar
dimitris committed
250
  = wl { wl_eqs = ct : wl_eqs wl }
251

252
extendWorkListFunEq :: Ct -> WorkList -> WorkList
253
extendWorkListFunEq ct wl
254
  = wl { wl_funeqs = ct : wl_funeqs wl }
255

256 257
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
258
extendWorkListNonEq ct wl
259
  = wl { wl_rest = ct : wl_rest wl }
260

261 262 263 264
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl
  = wl { wl_implics = implic `consBag` wl_implics wl }

265 266 267
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
268 269 270
 = case classifyPredType (ctPred ct) of
     EqPred ty1 _
       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
271
       , isTypeFamilyTyCon tc
272 273 274 275 276
       -> extendWorkListFunEq ct wl
       | otherwise
       -> extendWorkListEq ct wl

     _ -> extendWorkListNonEq ct wl
277

Simon Peyton Jones's avatar
Simon Peyton Jones committed
278
extendWorkListCts :: [Ct] -> WorkList -> WorkList
279
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
280
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
281 282

isEmptyWorkList :: WorkList -> Bool
283 284
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
                    , wl_rest = rest, wl_implics = implics })
285
  = null eqs && null rest && null funeqs && isEmptyBag implics
286 287

emptyWorkList :: WorkList
288
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
289
                   , wl_funeqs = [], wl_implics = emptyBag }
dimitris's avatar
dimitris committed
290 291

selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
292
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
dimitris's avatar
dimitris committed
293
  = case (eqs,feqs,rest) of
294 295 296 297
      (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
298

299 300
-- Pretty printing
instance Outputable WorkList where
301 302 303
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
          , wl_rest = rest, wl_implics = implics })
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
304
     vcat [ ppUnless (null eqs) $
305
            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
306 307
          , ppUnless (null feqs) $
            ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
308
          , ppUnless (null rest) $
309
            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
310 311 312
          , ppUnless (isEmptyBag implics) $
            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
          ])
dimitris's avatar
dimitris committed
313

314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
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
343 344 345 346 347 348 349
{-
************************************************************************
*                                                                      *
*                            Inert Sets                                *
*                                                                      *
*                                                                      *
************************************************************************
dimitris's avatar
dimitris committed
350 351 352 353

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

355
  * All canonical
356

357 358 359 360 361 362 363 364 365 366 367 368 369 370
  * 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
371 372
  * CTyEqCan equalities: see Note [Applying the inert substitution]
                         in TcFlatten
373

374 375
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
376
Type-family equations, of form (ev : F tys ~ ty), live in three places
377 378 379 380 381 382 383

  * 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
384
        list.  Now if we flatten w2 before we get to w3, we still want to
385 386 387
        share that (G a).

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

391
  * The inert_funeqs are un-solved but fully processed and in the InertCans.
Austin Seipp's avatar
Austin Seipp committed
392
-}
393 394 395

-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
396
data InertCans
397 398
  = IC { inert_eqs :: TyVarEnv EqualCtList
              -- All CTyEqCans; index is the LHS tyvar
399

400
       , inert_funeqs :: FunEqMap Ct
401 402 403
              -- All CFunEqCans; index is the whole family head type.

       , inert_dicts :: DictMap Ct
404
              -- Dictionaries only, index is the class
405
              -- NB: index is /not/ the whole type because FD reactions
406
              -- need to match the class but not necessarily the whole type.
407

408
       , inert_irreds :: Cts
409 410
              -- Irreducible predicates

411
       , inert_insols :: Cts
412 413
              -- Frozen errors (as non-canonicals)
       }
414

415 416 417 418 419 420 421 422 423 424 425
type EqualCtList = [Ct]
-- 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
--   - Multiple Wanteds, or
--   - Multiple Deriveds
426

dimitris's avatar
dimitris committed
427 428 429
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
430
              -- Canonical Given, Wanted, Derived (no Solved)
431
              -- Sometimes called "the inert set"
432

433
       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtEvidence)
434
              -- See Note [Type family equations]
435 436 437 438 439
              -- If    F tys :-> (co, ty, ev),
              -- then  co :: F tys ~ ty
              --
              -- The 'ev' field is just for the G/W/D flavour, nothing more!
              --
440 441 442 443 444
              -- 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.
445
              -- Not necessarily inert wrt top-level equations (or inert_cans)
446

447
       , inert_solved_dicts   :: DictMap CtEvidence
448
              -- Of form ev :: C t1 .. tn
449
              -- Always the result of using a top-level instance declaration
450
              -- See Note [Solved constraints]
451 452 453 454
              -- - 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
455
       }
456

457 458
instance Outputable InertCans where
  ppr ics = vcat [ ptext (sLit "Equalities:")
459 460
                   <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
                                          emptyCts (inert_eqs ics))
461
                 , ptext (sLit "Type-function equalities:")
462
                   <+> pprCts (funEqsToBag (inert_funeqs ics))
463
                 , ptext (sLit "Dictionaries:")
464
                   <+> pprCts (dictsToBag (inert_dicts ics))
465
                 , ptext (sLit "Irreds:")
466
                   <+> pprCts (inert_irreds ics)
467 468
                 , text "Insolubles =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
dimitris's avatar
dimitris committed
469
                 ]
470 471

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

dimitris's avatar
dimitris committed
475 476
emptyInert :: InertSet
emptyInert
477 478 479 480 481 482 483 484
  = IS { inert_cans = IC { inert_eqs     = emptyVarEnv
                         , inert_dicts   = emptyDicts
                         , inert_funeqs  = emptyFunEqs
                         , inert_irreds  = emptyCts
                         , inert_insols  = emptyCts
                         }
       , inert_flat_cache    = emptyFunEqs
       , inert_solved_dicts  = emptyDictMap }
485

486 487 488
---------------
addInertCan :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
489
addInertCan ics item@(CTyEqCan {})
490 491
  = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
                              (inert_eqs ics)
492
                              (cc_tyvar item) [item] }
493

494 495
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
496 497

addInertCan ics item@(CIrredEvCan {})
498
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
499 500 501 502 503
       -- 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
504 505 506

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

508 509 510 511 512 513
addInertCan _ item
  = pprPanic "upd_inert set: can't happen! Inserting " $
    ppr item   -- Can't be CNonCanonical, CHoleCan,
               -- because they only land in inert_insols

--------------
514
insertInertItemTcS :: Ct -> TcS ()
515
-- Add a new item in the inerts of the monad
516
insertInertItemTcS item
517
  = do { traceTcS "insertInertItemTcS {" $
518 519
         text "Trying to insert new inert item:" <+> ppr item

520
       ; updInertCans (\ics -> addInertCan ics item)
521

522
       ; traceTcS "insertInertItemTcS }" $ empty }
523

524
addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
525
-- Add a new item in the solved set of the monad
526
addSolvedDict item cls tys
527
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
528
  = return ()
529
  | otherwise
530
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
531 532
       ; updInertTcS $ \ ics ->
             ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
533

534
updInertTcS :: (InertSet -> InertSet) -> TcS ()
535
-- Modify the inert set with the supplied function
536
updInertTcS upd_fn
537
  = do { is_var <- getTcSInertsRef
538
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
539
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
540

541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568
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)
569
-- See Note [Preparing inert set for implications]
570 571 572
prepareInertsForImplications is@(IS { inert_cans = cans })
  = is { inert_cans       = getGivens cans
       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
573
  where
574
    getGivens (IC { inert_eqs    = eqs
575
                  , inert_irreds = irreds
576
                  , inert_funeqs = funeqs
577
                  , inert_dicts  = dicts })
578 579
      = IC { inert_eqs     = filterVarEnv  is_given_ecl eqs
           , inert_funeqs  = filterFunEqs  isGivenCt funeqs
580
           , inert_irreds  = Bag.filterBag isGivenCt irreds
581 582
           , inert_dicts   = filterDicts   isGivenCt dicts
           , inert_insols  = emptyCts }
583

584 585 586
    is_given_ecl :: EqualCtList -> Bool
    is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
    is_given_ecl _                        = False
587

Austin Seipp's avatar
Austin Seipp committed
588
{-
589 590 591 592 593 594 595
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
596 597
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
598 599
do that flattening recursively.

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

606 607
There might be cases where interactions between wanteds at different levels
could help to solve a constraint. For example
608

609 610
        class C a b | a -> b
        (C Int alpha), (forall d. C d blah => C Int a)
611

612
If we pushed the (C Int alpha) inwards, as a given, it can produce a
613 614 615
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.
616

617 618
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
619
-}
620

621
getInertEqs :: TcS (TyVarEnv EqualCtList)
622
getInertEqs = do { inert <- getTcSInerts
623
                 ; return (inert_eqs (inert_cans inert)) }
624

625 626
getUnsolvedInerts :: TcS ( Bag Implication
                         , Cts     -- Tyvar eqs: a ~ ty
627 628 629 630 631 632 633 634 635 636 637 638 639 640 641
                         , Cts     -- Fun eqs:   F a ~ ty
                         , Cts     -- Insoluble
                         , Cts )   -- All others
getUnsolvedInerts
 = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs
           , inert_irreds = irreds, inert_dicts = idicts
           , inert_insols = insols } <- getInertCans

      ; let unsolved_tv_eqs  = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts)
                                          emptyCts tv_eqs
            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

642 643 644
      ; implics <- getWorkListImplics

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

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

654
getNoGivenEqs :: TcLevel     -- TcLevel of this implication
655 656 657
               -> [TcTyVar]       -- Skolems of this implication
               -> TcS Bool        -- True <=> definitely no residual given equalities
-- See Note [When does an implication have given equalities?]
658
getNoGivenEqs tclvl skol_tvs
659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679
  = 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
680
      && tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
681 682 683 684 685 686 687 688 689 690 691 692 693

    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
694
{-
695 696 697 698 699 700 701 702 703 704 705 706 707 708 709
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
710 711
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
   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

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
753
-}
754

Adam Gundry's avatar
Adam Gundry committed
755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
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 }

    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
      is { inert_eqs = delTyEq (inert_eqs is) x ty }

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


789 790 791 792 793 794 795 796
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)
797 798
            unsolved_dicts  = foldDicts ((||)  . isWantedCt) (inert_dicts icans)  False
            unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False
799
            unsolved_eqs    = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans)
800 801 802

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

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

    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys

820

821
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
822
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
823 824
lookupInInerts loc pty
  = do { inerts <- getTcSInerts
825 826
       ; return $ case (classifyPredType pty) of
           ClassPred cls tys
827 828 829 830
              | Just ev <- lookupSolvedDict inerts loc cls tys
              -> Just ev
              | otherwise
              -> lookupInertDict (inert_cans inerts) loc cls tys
831

832
           _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
833 834
      }

835 836 837 838 839 840 841 842 843
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
844
-- Returns just if exactly this predicate type exists in the solved.
845 846 847 848
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
  = case findDict solved cls tys of
      Just ev | ctEvCheckDepth cls loc ev -> Just ev
      _                                   -> Nothing
849

Austin Seipp's avatar
Austin Seipp committed
850 851 852
{-
************************************************************************
*                                                                      *
853
                   TyEqMap
Austin Seipp's avatar
Austin Seipp committed
854 855 856
*                                                                      *
************************************************************************
-}
857 858 859 860 861

type TyEqMap a = TyVarEnv a

findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
findTyEqs m tv = lookupVarEnv m tv `orElse` []
Adam Gundry's avatar
Adam Gundry committed
862 863 864 865 866

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
867

Austin Seipp's avatar
Austin Seipp committed
868 869 870
{-
************************************************************************
*                                                                      *
871
                   TcAppMap, DictMap, FunEqMap
Austin Seipp's avatar
Austin Seipp committed
872 873 874
*                                                                      *
************************************************************************
-}
875

876 877 878
type TcAppMap a = UniqFM (ListMap TypeMap a)