TcSMonad.hs 70 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
26
    Freshness(..), freshGoals, isFresh,
27

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

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

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

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

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

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

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

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

66
    instDFunType,                              -- Instantiation
67 68

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

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

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

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

#include "HsVersions.h"

import HscTypes

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

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

108
import TcEvidence
109 110
import Class
import TyCon
111

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

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

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

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

137 138 139
#ifdef DEBUG
import Digraph
#endif
140

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

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

157
As a simple form of priority queue, our worklist separates out
158 159 160 161
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
162

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
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
211

212
-}
213

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

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

231

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

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

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

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

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

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

     _ -> extendWorkListNonEq ct wl
265

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

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

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

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

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

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
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
331 332 333 334 335 336 337
{-
************************************************************************
*                                                                      *
*                            Inert Sets                                *
*                                                                      *
*                                                                      *
************************************************************************
dimitris's avatar
dimitris committed
338 339 340 341

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

343
  * All canonical
344

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

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

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

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

379
  * The inert_funeqs are un-solved but fully processed and in the InertCans.
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538

Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~
When we apply a top-level instance declararation, we add the "solved"
dictionary to the inert_solved_dicts.  In general, we use it to avoid
creating a new EvVar when we have a new goal that we have solved in
the past.

But in particular, we can use it to create *recursive* dicationaries.
The simplest, degnerate case is
    instance C [a] => C [a] where ...
If we have
    [W] d1 :: C [x]
then we can apply the instance to get
    d1 = $dfCList d
    [W] d2 :: C [x]
Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
    d1 = $dfCList d
    d2 = d1

See Note [Example of recursive dictionaries]
Other notes about solved dictionaries

* See also Note [Do not add superclasses of solved dictionaries]

* The inert_solved_dicts field is not rewritten by equalities, so it may
  get out of date.

Note [Do not add superclasses of solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Every member of inert_solved_dicts is the result of applying a dictionary
function, NOT of applying superclass selection to anything.
Consider

        class Ord a => C a where
        instance Ord [a] => C [a] where ...

Suppose we are trying to solve
  [G] d1 : Ord a
  [W] d2 : C [a]

Then we'll use the instance decl to give

  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
  [W] d3 : Ord [a]

We must not add d4 : Ord [a] to the 'solved' set (by taking the
superclass of d2), otherwise we'll use it to solve d3, without ever
using d1, which would be a catastrophe.

Solution: when extending the solved dictionaries, do not add superclasses.
That's why each element of the inert_solved_dicts is the result of applying
a dictionary function.

Note [Example of recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Example 1

    data D r = ZeroD | SuccD (r (D r));

    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;

    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])). Here's how we go:

   [W] d1 : Eq (D [])
By instance decl of Eq (D r):
   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
By instance decl of Eq [a]:
   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
                                   d1 = dfEqD d2
Now this wanted can interact with our "solved" d1 to get:
    d3 = d1

-- Example 2:
This code arises in the context of "Scrap Your Boilerplate with Class"

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2

    class Data Maybe a => Foo a

    instance Foo t => Sat (Maybe t)                             -- dfunSat

    instance Data Maybe a => Foo a                              -- dfunFoo1
    instance Foo a        => Foo [a]                            -- dfunFoo2
    instance                 Foo [Char]                         -- dfunFoo3

Consider generating the superclasses of the instance declaration
         instance Foo a => Foo [a]

So our problem is this
    [G] d0 : Foo t
    [W] d1 : Data Maybe [t]   -- Desired superclass

We may add the given in the inert set, along with its superclasses
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  WorkList
    [W] d1 : Data Maybe [t]

Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
  WorkList:
    [W] d2 : Sat (Maybe [t])
    [W] d3 : Data Maybe t

Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList:
    [W] d3 : Data Maybe t
    [W] d4 : Foo [t]

Now, we can just solve d3 from d01; d3 := d01
  Inert
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList
    [W] d4 : Foo [t]

Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
  Inert
    [G] d0  : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
        d4 : Foo [t]
  WorkList:
    [W] d5 : Foo t

Now, d5 can be solved! d5 := d0

Result
   d1 := dfunData2 d2 d3
   d2 := dfunSat d4
   d3 := d01
   d4 := dfunFoo2 d5
   d5 := d0
Austin Seipp's avatar
Austin Seipp committed
539
-}
540 541 542

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

547
       , inert_funeqs :: FunEqMap Ct
548 549 550
              -- All CFunEqCans; index is the whole family head type.

       , inert_dicts :: DictMap Ct
551
              -- Dictionaries only, index is the class
552
              -- NB: index is /not/ the whole type because FD reactions
553
              -- need to match the class but not necessarily the whole type.
554

555
       , inert_irreds :: Cts
556 557
              -- Irreducible predicates

558
       , inert_insols :: Cts
559 560
              -- Frozen errors (as non-canonicals)
       }
561

562
type EqualCtList = [Ct]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
563 564 565 566 567 568 569 570 571 572 573 574
{-
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
-}
575

dimitris's avatar
dimitris committed
576 577 578
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
579
              -- Canonical Given, Wanted, Derived (no Solved)
580
              -- Sometimes called "the inert set"
581

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
582
       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
583
              -- See Note [Type family equations]
584 585 586
              -- If    F tys :-> (co, ty, ev),
              -- then  co :: F tys ~ ty
              --
587 588 589 590 591
              -- 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.
592
              -- Not necessarily inert wrt top-level equations (or inert_cans)
593

594
       , inert_solved_dicts   :: DictMap CtEvidence
595
              -- Of form ev :: C t1 .. tn
596 597
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
dimitris's avatar
dimitris committed
598
       }
599

600 601
instance Outputable InertCans where
  ppr ics = vcat [ ptext (sLit "Equalities:")
602 603
                   <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
                                          emptyCts (inert_eqs ics))
604
                 , ptext (sLit "Type-function equalities:")
605
                   <+> pprCts (funEqsToBag (inert_funeqs ics))
606
                 , ptext (sLit "Dictionaries:")
607
                   <+> pprCts (dictsToBag (inert_dicts ics))
608
                 , ptext (sLit "Irreds:")
609
                   <+> pprCts (inert_irreds ics)
610 611
                 , text "Insolubles =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
dimitris's avatar
dimitris committed
612
                 ]
613 614

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

dimitris's avatar
dimitris committed
618 619
emptyInert :: InertSet
emptyInert
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
620 621 622 623 624
  = IS { inert_cans = IC { inert_eqs      = emptyVarEnv
                         , inert_dicts    = emptyDicts
                         , inert_funeqs   = emptyFunEqs
                         , inert_irreds   = emptyCts
                         , inert_insols   = emptyCts
625 626 627
                         }
       , inert_flat_cache    = emptyFunEqs
       , inert_solved_dicts  = emptyDictMap }
628

629 630 631
---------------
addInertCan :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
632
addInertCan ics item@(CTyEqCan {})
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
633 634 635 636 637 638
  = 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]
639

640 641
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
642 643

addInertCan ics item@(CIrredEvCan {})
644
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
645 646 647 648 649
       -- 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
650 651 652

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

654 655 656 657 658 659
addInertCan _ item
  = pprPanic "upd_inert set: can't happen! Inserting " $
    ppr item   -- Can't be CNonCanonical, CHoleCan,
               -- because they only land in inert_insols

--------------
660
insertInertItemTcS :: Ct -> TcS ()
661
-- Add a new item in the inerts of the monad
662
insertInertItemTcS item
663
  = do { traceTcS "insertInertItemTcS {" $
664 665
         text "Trying to insert new inert item:" <+> ppr item

666
       ; updInertCans (\ics -> addInertCan ics item)
667

668
       ; traceTcS "insertInertItemTcS }" $ empty }
669

670
addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
671
-- Add a new item in the solved set of the monad
672
-- See Note [Solved dictionaries]
673
addSolvedDict item cls tys
674
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
675
  = return ()
676
  | otherwise
677
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
678 679
       ; updInertTcS $ \ ics ->
             ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
680

681
updInertTcS :: (InertSet -> InertSet) -> TcS ()
682
-- Modify the inert set with the supplied function
683
updInertTcS upd_fn
684
  = do { is_var <- getTcSInertsRef
685
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
686
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
687

688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
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)
716
-- See Note [Preparing inert set for implications]
717 718 719
prepareInertsForImplications is@(IS { inert_cans = cans })
  = is { inert_cans       = getGivens cans
       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
720
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
721 722 723 724 725 726 727 728 729
    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 }
730

731 732 733
    is_given_ecl :: EqualCtList -> Bool
    is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
    is_given_ecl _                        = False
734

Austin Seipp's avatar
Austin Seipp committed
735
{-
736 737 738 739 740 741 742
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
743 744
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
745 746
do that flattening recursively.

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

753 754
There might be cases where interactions between wanteds at different levels
could help to solve a constraint. For example
755

756 757
        class C a b | a -> b
        (C Int alpha), (forall d. C d blah => C Int a)
758

759
If we pushed the (C Int alpha) inwards, as a given, it can produce a
760 761 762
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.
763

764 765
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
766
-}
767

768
getInertEqs :: TcS (TyVarEnv EqualCtList)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
769 770 771
getInertEqs
  = do { inert <- getTcSInerts
       ; return (inert_eqs (inert_cans inert)) }
772

773 774
getUnsolvedInerts :: TcS ( Bag Implication
                         , Cts     -- Tyvar eqs: a ~ ty
775 776 777 778
                         , Cts     -- Fun eqs:   F a ~ ty
                         , Cts     -- Insoluble
                         , Cts )   -- All others
getUnsolvedInerts
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
779 780
 = do { IC { inert_eqs    = tv_eqs
           , inert_funeqs = fun_eqs
781 782 783
           , inert_irreds = irreds, inert_dicts = idicts
           , inert_insols = insols } <- getInertCans

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
784 785
      ; let unsolved_tv_eqs   = foldVarEnv (\cts rest ->
                                             foldr add_if_unsolved rest cts)
786
                                          emptyCts tv_eqs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
787 788 789 790 791
            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
792

793 794 795
      ; implics <- getWorkListImplics

      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
796 797
              -- Keep even the given insolubles
              -- so that we can report dead GADT pattern match branches
798
  where
799
    add_if_unsolved :: Ct -> Cts -> Cts
800
    add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
801 802
                           | otherwise      = cts

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

805
getNoGivenEqs :: TcLevel     -- TcLevel of this implication
806 807 808
               -> [TcTyVar]       -- Skolems of this implication
               -> TcS Bool        -- True <=> definitely no residual given equalities
-- See Note [When does an implication have given equalities?]
809
getNoGivenEqs tclvl skol_tvs
810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830
  = 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
831
      && tclvl == ctLocLevel (ctEvLoc ev)
832 833 834 835 836 837 838 839 840 841 842 843 844

    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
845
{-
846 847 848 849 850 851 852 853 854 855 856 857 858 859 860
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
861 862
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885
   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
886 887 888
 * We do *not* need to worry about representational equalities, because
   these do not affect the ability to float constraints.

889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906
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
907
-}
908

Adam Gundry's avatar
Adam Gundry committed
909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934
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
935 936
    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
      is { inert_eqs    = delTyEq (inert_eqs is) x ty }
Adam Gundry's avatar
Adam Gundry committed
937 938 939 940 941 942

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


943 944 945 946 947 948 949
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
950 951 952 953 954 955 956
            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)
957 958 959

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
960
                     || not (isEmptyBag (inert_insols icans)))) }
961

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
962
lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
963 964
lookupFlatCache fam_tc tys
  = do { IS { inert_flat_cache = flat_cache
965
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
966 967
       ; return (firstJusts [lookup_inerts inert_funeqs,
                             lookup_flats flat_cache]) }
968
  where
969
    lookup_inerts inert_funeqs
970 971
      | 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
972
      = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
973 974 975 976
      | otherwise = Nothing

    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys