TcSMonad.hs 66.6 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
    instDFunConstraints,
35

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

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

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

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

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

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

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

68
    instDFunType,                              -- Instantiation
69 70

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

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

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

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

#include "HsVersions.h"

import HscTypes

import Inst
97 98
import InstEnv
import FamInst
99 100 101 102
import FamInstEnv

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

110
import TcEvidence
111 112
import Class
import TyCon
113

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

124
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
125
import Util
126
import Id
Ian Lynagh's avatar
Ian Lynagh committed
127
import TcRnTypes
128

129
import Unique
130
import UniqFM
131
import Maybes ( orElse, firstJusts )
132

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

140 141 142
#ifdef DEBUG
import Digraph
#endif
143

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

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

160
As a simple form of priority queue, our worklist separates out
161 162 163 164
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
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 212 213
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
214

215
-}
216

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

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

234

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

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

243
extendWorkListFunEq :: Ct -> WorkList -> WorkList
244
extendWorkListFunEq ct wl
245
  = wl { wl_funeqs = ct : wl_funeqs wl }
246

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

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

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

     _ -> extendWorkListNonEq ct wl
268

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

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

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

selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
283
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
dimitris's avatar
dimitris committed
284
  = case (eqs,feqs,rest) of
285 286 287 288
      (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
289

290 291
-- Pretty printing
instance Outputable WorkList where
292 293 294
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
          , wl_rest = rest, wl_implics = implics })
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
295
     vcat [ ppUnless (null eqs) $
296
            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
297 298
          , ppUnless (null feqs) $
            ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
299
          , ppUnless (null rest) $
300
            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
301 302 303
          , ppUnless (isEmptyBag implics) $
            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
          ])
dimitris's avatar
dimitris committed
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 332 333
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
334 335 336 337 338 339 340
{-
************************************************************************
*                                                                      *
*                            Inert Sets                                *
*                                                                      *
*                                                                      *
************************************************************************
dimitris's avatar
dimitris committed
341 342 343 344

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

346
  * All canonical
347

348 349 350 351 352 353 354 355 356 357 358 359 360 361
  * 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
362 363
  * CTyEqCan equalities: see Note [Applying the inert substitution]
                         in TcFlatten
364

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

  * 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
375
        list.  Now if we flatten w2 before we get to w3, we still want to
376 377 378
        share that (G a).

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

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

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

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

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

399
       , inert_irreds :: Cts
400 401
              -- Irreducible predicates

402
       , inert_insols :: Cts
403 404
              -- Frozen errors (as non-canonicals)
       }
405

406
type EqualCtList = [Ct]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
407 408 409 410 411 412 413 414 415 416 417 418
{-
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
-}
419

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
426
       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
427
              -- See Note [Type family equations]
428 429 430
              -- If    F tys :-> (co, ty, ev),
              -- then  co :: F tys ~ ty
              --
431 432 433 434 435
              -- 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.
436
              -- Not necessarily inert wrt top-level equations (or inert_cans)
437

438
       , inert_solved_dicts   :: DictMap CtEvidence
439
              -- Of form ev :: C t1 .. tn
440
              -- Always the result of using a top-level instance declaration
441 442 443 444
              -- - 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
445
       }
446

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

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

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

476 477 478
---------------
addInertCan :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
479
addInertCan ics item@(CTyEqCan {})
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
480 481 482 483 484 485
  = 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]
486

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

addInertCan ics item@(CIrredEvCan {})
491
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
492 493 494 495 496
       -- 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
497 498 499

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

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

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

513
       ; updInertCans (\ics -> addInertCan ics item)
514

515
       ; traceTcS "insertInertItemTcS }" $ empty }
516

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

527
updInertTcS :: (InertSet -> InertSet) -> TcS ()
528
-- Modify the inert set with the supplied function
529
updInertTcS upd_fn
530
  = do { is_var <- getTcSInertsRef
531
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
532
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
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 560 561
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)
562
-- See Note [Preparing inert set for implications]
563 564 565
prepareInertsForImplications is@(IS { inert_cans = cans })
  = is { inert_cans       = getGivens cans
       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
566
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
567 568 569 570 571 572 573 574 575
    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 }
576

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

Austin Seipp's avatar
Austin Seipp committed
581
{-
582 583 584 585 586 587 588
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
589 590
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
591 592
do that flattening recursively.

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

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

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

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

610 611
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
612
-}
613

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

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
630 631
      ; let unsolved_tv_eqs   = foldVarEnv (\cts rest ->
                                             foldr add_if_unsolved rest cts)
632
                                          emptyCts tv_eqs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
633 634 635 636 637
            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
638

639 640 641
      ; implics <- getWorkListImplics

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

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

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

    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
691
{-
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
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
707 708
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731
   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
732 733 734
 * We do *not* need to worry about representational equalities, because
   these do not affect the ability to float constraints.

735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
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
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
781 782
    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
      is { inert_eqs    = delTyEq (inert_eqs is) x ty }
Adam Gundry's avatar
Adam Gundry committed
783 784 785 786 787 788

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


789 790 791 792 793 794 795
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
796 797 798 799 800 801 802
            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)
803 804 805

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
806
                     || not (isEmptyBag (inert_insols icans)))) }
807

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

    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys

823

824
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
825
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
826
lookupInInerts loc pty
827
  | ClassPred cls tys <- classifyPredType pty
828
  = do { inerts <- getTcSInerts
829 830 831 832
       ; 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
833

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

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

type TyEqMap a = TyVarEnv a

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

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
866

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