TcSMonad.hs 117 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
    extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
10
    appendWorkList, extendWorkListImplic,
11 12
    selectNextWorkItem,
    workListSize, workListWantedCount,
13
    getWorkList, updWorkListTcS,
14

15
    -- The TcS monad
16
    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
17
    failTcS, warnTcS, addErrTcS,
18
    runTcSEqualities,
19
    nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication,
20

21
    runTcPluginTcS, addUsedGRE, addUsedGREs,
22

23 24
    -- Tracing etc
    panicTcS, traceTcS,
25
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
26
    wrapErrTcS, wrapWarnTcS,
27

28
    -- Evidence creation and transformation
29
    MaybeNew(..), freshGoals, isFresh, getEvTerm,
30

31
    newTcEvBinds,
32
    newWantedEq, emitNewWantedEq,
33
    newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
34
    newBoundEvVarId,
35
    unifyTyVar, unflattenFmv, reportUnifications,
36 37
    setEvBind, setWantedEq, setEqIfWanted,
    setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
38
    newEvVar, newGivenEvVar, newGivenEvVars,
39
    emitNewDeriveds, emitNewDerivedEq,
40
    checkReductionDepth,
41

42
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
43
    getTopEnv, getGblEnv, getLclEnv,
44
    getTcEvBindsVar, getTcLevel,
45 46
    getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
    tcLookupClass, tcLookupId,
47

48
    -- Inerts
49
    InertSet(..), InertCans(..),
50
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
51
    getNoGivenEqs, setInertCans,
52 53
    getInertEqs, getInertCans, getInertGivens,
    getInertInsols,
54
    getTcSInerts, setTcSInerts,
55
    matchableGivens, prohibitedSuperClassSolve,
56
    getUnsolvedInerts,
57
    removeInertCts, getPendingScDicts,
58
    addInertCan, addInertEq, insertFunEq,
59
    emitWorkNC, emitWork,
60
    isImprovable,
61 62

    -- The Model
63
    kickOutAfterUnification,
64

65 66 67 68
    -- Inert Safe Haskell safe-overlap failures
    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
    getSafeOverlapFailures,

69
    -- Inert CDictCans
70 71
    DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
    addDictsByClass, delDict, foldDicts, filterDicts, findDict,
72

73
    -- Inert CTyEqCans
74
    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
75
    lookupFlattenTyVar, lookupInertTyVar,
76 77 78 79

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

80 81 82
    -- Irreds
    foldIrreds,

83 84 85 86
    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems

    -- Inert CFunEqCans
87
    updInertFunEqs, findFunEq,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
88
    findFunEqsByTyCon,
89

90
    instDFunType,                              -- Instantiation
91 92

    -- MetaTyVars
93
    newFlexiTcSTy, instFlexi, instFlexiX,
94
    cloneMetaTyVar, demoteUnfilledFmv,
95
    tcInstType, tcInstSkolTyVarsX,
96

97
    TcLevel, isTouchableMetaTyVarTcS,
98
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
99
    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
100
    zonkTyCoVarsAndFVList,
101
    zonkSimples, zonkWC,
102

103 104
    -- References
    newTcRef, readTcRef, updTcRef,
105

106 107
    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
Adam Gundry's avatar
Adam Gundry committed
108
    matchFam, matchFamTcM,
109
    checkWellStagedDFun,
110
    pprEq                                    -- Smaller utils, re-exported from TcM
111
                                             -- TODO (DV): these are only really used in the
112 113
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
114 115
                                             -- here
) where
116 117 118

#include "HsVersions.h"

119 120
import GhcPrelude

121 122
import HscTypes

123
import qualified Inst as TcM
124 125
import InstEnv
import FamInst
126 127 128 129
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
130
import qualified TcEnv as TcM
131
       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass, tcLookupId )
132
import PrelNames( heqTyConKey, eqTyConKey )
133
import Kind
134 135
import TcType
import DynFlags
136
import Type
137
import Coercion
138
import Unify
139

140
import TcEvidence
141 142
import Class
import TyCon
143
import TcErrors   ( solverDepthErrorTcS )
144

145
import Name
146
import RdrName ( GlobalRdrEnv, GlobalRdrElt )
147
import qualified RnEnv as TcM
148
import Var
149
import VarEnv
150
import VarSet
151 152
import Outputable
import Bag
153
import UniqSupply
Ian Lynagh's avatar
Ian Lynagh committed
154
import Util
Ian Lynagh's avatar
Ian Lynagh committed
155
import TcRnTypes
156

157
import Unique
158
import UniqFM
159
import UniqDFM
160
import Maybes
161

162
import TrieMap
163
import Control.Monad
quchen's avatar
quchen committed
164
import qualified Control.Monad.Fail as MonadFail
165
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
166
import Data.IORef
167
import Data.List ( foldl', partition )
168

Ben Gamari's avatar
Ben Gamari committed
169
#if defined(DEBUG)
170
import Digraph
David Feuer's avatar
David Feuer committed
171
import UniqSet
172
#endif
173

Austin Seipp's avatar
Austin Seipp committed
174 175 176 177 178 179 180 181 182
{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************
183

184 185
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
186 187 188
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.
189

190
As a simple form of priority queue, our worklist separates out
Simon Peyton Jones's avatar
Simon Peyton Jones committed
191

192
* equalities (wl_eqs); see Note [Prioritise equalities]
193 194
* type-function equalities (wl_funeqs)
* all the rest (wl_rest)
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214

Note [Prioritise equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very important to process equalities /first/:

* (Efficiency)  The general reason to do so is that if we process a
  class constraint first, we may end up putting it into the inert set
  and then kicking it out later.  That's extra work compared to just
  doing the equality first.

* (Avoiding fundep iteration) As Trac #14723 showed, it's possible to
  get non-termination if we
      - Emit the Derived fundep equalities for a class constraint,
        generating some fresh unification variables.
      - That leads to some unification
      - Which kicks out the class constraint
      - Which isn't solved (because there are still some more Derived
        equalities in the work-list), but generates yet more fundeps
  Solution: prioritise derived equalities over class constraints

215 216 217
* (Class equalities) We need to prioritise equalities even if they
  are hidden inside a class constraint;
  see Note [Prioritise class equalities]
218 219 220 221 222

* (Kick-out) We want to apply this priority scheme to kicked-out
  constraints too (see the call to extendWorkListCt in kick_out_rewritable
  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
  homo-kinded when kicked out, and hence we want to priotitise it.
223

224 225 226 227 228 229
* (Derived equalities) Originally we tried to postpone processing
  Derived equalities, in the hope that we might never need to deal
  with them at all; but in fact we must process Derived equalities
  eagerly, partly for the (Efficiency) reason, and more importantly
  for (Avoiding fundep iteration).

230 231 232 233 234 235 236 237 238 239 240 241 242
Note [Prioritise class equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prioritise equalities in the solver (see selectWorkItem). But class
constraints like (a ~ b) and (a ~~ b) are actually equalities too;
see Note [The equality types story] in TysPrim.

Failing to prioritise these is inefficient (more kick-outs etc).
But, worse, it can prevent us spotting a "recursive knot" among
Wanted constraints.  See comment:10 of Trac #12734 for a worked-out
example.

So we arrange to put these particular class constraints in the wl_eqs.

243
  NB: since we do not currently apply the substitution to the
244 245
  inert_solved_dicts, the knot-tying still seems a bit fragile.
  But this makes it better.
246
-}
247

248
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
249
data WorkList
250 251 252 253 254 255
  = WL { wl_eqs     :: [Ct]  -- CTyEqCan, CDictCan, CIrredCan
                             -- Given, Wanted, and Derived
                       -- Contains both equality constraints and their
                       -- class-level variants (a~b) and (a~~b);
                       -- See Note [Prioritise equalities]
                       -- See Note [Prioritise class equalities]
256

257
       , wl_funeqs  :: [Ct]
258

259
       , wl_rest    :: [Ct]
260

261 262
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
263

Simon Peyton Jones's avatar
Simon Peyton Jones committed
264
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
265
appendWorkList
266
    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
267
        , wl_implics = implics1 })
268
    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
269
        , wl_implics = implics2 })
270 271 272
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
273
        , wl_implics = implics1 `unionBags`   implics2 }
274

275
workListSize :: WorkList -> Int
276 277
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
  = length eqs + length funeqs + length rest
278 279

workListWantedCount :: WorkList -> Int
280 281
-- Count the things we need to solve
-- excluding the insolubles (c.f. inert_count)
282
workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
283 284 285 286 287 288 289
  = count isWantedCt eqs + count is_wanted rest
  where
    is_wanted ct
     | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
     = not insol && isWanted ev
     | otherwise
     = isWantedCt ct
290

291
extendWorkListEq :: Ct -> WorkList -> WorkList
292 293
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

294
extendWorkListFunEq :: Ct -> WorkList -> WorkList
295
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
296

297 298
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
299 300
extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }

301 302 303
extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds evs wl
  = extendWorkListCts (map mkNonCanonical evs) wl
304

305 306
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
307

308 309 310
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
311
 = case classifyPredType (ctPred ct) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
312
     EqPred NomEq ty1 _
Ben Gamari's avatar
Ben Gamari committed
313
       | Just tc <- tcTyConAppTyCon_maybe ty1
314
       , isTypeFamilyTyCon tc
315
       -> extendWorkListFunEq ct wl
316

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
317
     EqPred {}
318 319
       -> extendWorkListEq ct wl

Gabor Greif's avatar
Gabor Greif committed
320
     ClassPred cls _  -- See Note [Prioritise class equalities]
321 322 323 324
       |  cls `hasKey` heqTyConKey
       || cls `hasKey` eqTyConKey
       -> extendWorkListEq ct wl

325
     _ -> extendWorkListNonEq ct wl
326

Simon Peyton Jones's avatar
Simon Peyton Jones committed
327
extendWorkListCts :: [Ct] -> WorkList -> WorkList
328
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
329
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
330 331

isEmptyWorkList :: WorkList -> Bool
332
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
333 334
                    , wl_rest = rest, wl_implics = implics })
  = null eqs && null rest && null funeqs && isEmptyBag implics
335 336

emptyWorkList :: WorkList
337
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
338
                   , wl_funeqs = [], wl_implics = emptyBag }
339 340

selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
341
-- See Note [Prioritise equalities]
342 343 344 345 346 347 348
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
                      , wl_rest = rest })
  | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
  | ct:fes <- feqs = Just (ct, wl { wl_funeqs = fes })
  | ct:cts <- rest = Just (ct, wl { wl_rest   = cts })
  | otherwise      = Nothing

349 350 351 352
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef
                 ; wrapTcS (TcM.readTcRef wl_var) }

353
selectNextWorkItem :: TcS (Maybe Ct)
354 355
-- Pick which work item to do next
-- See Note [Prioritise equalities]
356 357 358
selectNextWorkItem
  = do { wl_var <- getTcSWorkListRef
       ; wl <- wrapTcS (TcM.readTcRef wl_var)
359 360 361 362 363 364
       ; case selectWorkItem wl of {
           Nothing -> return Nothing ;
           Just (ct, new_wl) ->
    do { checkReductionDepth (ctLoc ct) (ctPred ct)
       ; wrapTcS (TcM.writeTcRef wl_var new_wl)
       ; return (Just ct) } } }
dimitris's avatar
dimitris committed
365

366 367
-- Pretty printing
instance Outputable WorkList where
368
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
369
          , wl_rest = rest, wl_implics = implics })
370
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
371
     vcat [ ppUnless (null eqs) $
372
            text "Eqs =" <+> vcat (map ppr eqs)
373
          , ppUnless (null feqs) $
374
            text "Funeqs =" <+> vcat (map ppr feqs)
375
          , ppUnless (null rest) $
376
            text "Non-eqs =" <+> vcat (map ppr rest)
377
          , ppUnless (isEmptyBag implics) $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
378 379
            ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
                       (text "(Implics omitted)")
380
          ])
dimitris's avatar
dimitris committed
381

382 383

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
384
*                                                                      *
385
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
386 387
*                                                                      *
*                                                                      *
388
********************************************************************* -}
389

390 391
data InertSet
  = IS { inert_cans :: InertCans
392
              -- Canonical Given, Wanted, Derived
393
              -- Sometimes called "the inert set"
394

395 396 397 398 399 400 401 402 403 404
       , inert_fsks :: [(TcTyVar, TcType)]
              -- A list of (fsk, ty) pairs; we add one element when we flatten
              -- a function application in a Given constraint, creating
              -- a new fsk in newFlattenSkolem.  When leaving a nested scope,
              -- unflattenGivens unifies fsk := ty
              --
              -- We could also get this info from inert_funeqs, filtered by
              -- level, but it seems simpler and more direct to capture the
              -- fsk as we generate them.

405
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
406
              -- See Note [Type family equations]
407 408 409
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: F tys ~ rhs
              --       flav is [G] or [WD]
410 411 412 413 414 415 416
              --
              -- 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.
              -- Not necessarily inert wrt top-level equations (or inert_cans)
417

418 419
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

420 421 422 423 424
       , inert_solved_dicts   :: DictMap CtEvidence
              -- Of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }
425

426 427
instance Outputable InertSet where
  ppr is = vcat [ ppr $ inert_cans is
428 429 430 431
                , ppUnless (null dicts) $
                  text "Solved dicts" <+> vcat (map ppr dicts) ]
         where
           dicts = bagToList (dictsToBag (inert_solved_dicts is))
432

433 434 435
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_count    = 0
436
                         , inert_eqs      = emptyDVarEnv
437 438 439
                         , inert_dicts    = emptyDicts
                         , inert_safehask = emptyDicts
                         , inert_funeqs   = emptyFunEqs
440
                         , inert_irreds   = emptyCts }
441
       , inert_flat_cache    = emptyExactFunEqs
442
       , inert_fsks          = []
443
       , inert_solved_dicts  = emptyDictMap }
444

445

446 447
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
448
When we apply a top-level instance declaration, we add the "solved"
449 450 451 452
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.

453
But in particular, we can use it to create *recursive* dictionaries.
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 539 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 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603
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
604
-}
605

606 607 608 609 610 611 612 613
{- *********************************************************************
*                                                                      *
                InertCans: the canonical inerts
*                                                                      *
*                                                                      *
********************************************************************* -}

data InertCans   -- See Note [Detailed InertCans Invariants] for more
614
  = IC { inert_eqs :: InertEqs
615
              -- See Note [inert_eqs: the inert equalities]
616 617
              -- All CTyEqCans; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified
618

619
       , inert_funeqs :: FunEqMap Ct
620
              -- All CFunEqCans; index is the whole family head type.
621
              -- All Nominal (that's an invarint of all CFunEqCans)
622
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
623 624 625
              --     wrt inert_eqs
              -- Can include all flavours, [G], [W], [WD], [D]
              -- See Note [Type family equations]
626 627

       , inert_dicts :: DictMap Ct
628
              -- Dictionaries only
629
              -- All fully rewritten (modulo flavour constraints)
630
              --     wrt inert_eqs
631

632 633
       , inert_safehask :: DictMap Ct
              -- Failed dictionary resolution due to Safe Haskell overlapping
Gabor Greif's avatar
Gabor Greif committed
634
              -- instances restriction. We keep this separate from inert_dicts
635 636 637 638 639 640
              -- as it doesn't cause compilation failure, just safe inference
              -- failure.
              --
              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
              -- in TcSimplify

641
       , inert_irreds :: Cts
642 643 644
              -- Irreducible predicates that cannot be made canonical,
              --     and which don't interact with others (e.g.  (c a))
              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])
645 646 647 648 649

       , inert_count :: Int
              -- Number of Wanted goals in
              --     inert_eqs, inert_dicts, inert_safehask, inert_irreds
              -- Does not include insolubles
650
              -- When non-zero, keep trying to solve
651
       }
652

653 654
type InertEqs    = DTyVarEnv EqualCtList
type EqualCtList = [Ct]  -- See Note [EqualCtList invariants]
655

656
{- Note [Detailed InertCans Invariants]
657
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
658
The InertCans represents a collection of constraints with the following properties:
659

660
  * All canonical
661

662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
  * 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)

  * CTyEqCan equalities: see Note [Applying the inert substitution]
                         in TcFlatten

679 680 681 682 683 684 685 686 687 688 689 690 691 692
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
    * Derived before Wanted

From the fourth invariant it follows that the list is
   - A single [G], or
   - Zero or one [D] or [WD], followd by any number of [W]

The Wanteds can't rewrite anything which is why we put them last

693 694
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
695 696
Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
live in three places
697 698 699

  * The work-list, of course

700 701 702
  * The inert_funeqs are un-solved but fully processed, and in
    the InertCans. They can be [G], [W], [WD], or [D].

703
  * The inert_flat_cache.  This is used when flattening, to get maximal
704 705 706
    sharing. Everthing in the inert_flat_cache is [G] or [WD]

    It contains lots of things that are still in the work-list.
707 708 709 710 711 712 713 714
    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
        list.  Now if we flatten w2 before we get to w3, we still want to
        share that (G a).
    Because it contains work-list things, DO NOT use the flat cache to solve
    a top-level goal.  Eg in the above example we don't want to solve w3
    using w3 itself!

715
The CFunEqCan Ownership Invariant:
716

717 718 719 720 721
  * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv
    It "owns" that fsk/fmv, in the sense that:
      - reducing a [W/WD] CFunEqCan fills in the fmv
      - unflattening a [W/WD] CFunEqCan fills in the fmv
      (in both cases unless an occurs-check would result)
722

723 724 725 726
  * In contrast a [D] CFunEqCan does not "own" its fmv:
      - reducing a [D] CFunEqCan does not fill in the fmv;
        it just generates an equality
      - unflattening ignores [D] CFunEqCans altogether
727 728 729 730 731 732 733 734


Note [inert_eqs: the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Definition [Can-rewrite relation]
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties

Simon Peyton Jones's avatar
Simon Peyton Jones committed
735 736
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762
       then either f1 >= f2 or f2 >= f1

Lemma.  If f1 >= f then f1 >= f1
Proof.  By property (R2), with f1=f2

Definition [Generalised substitution]
A "generalised substitution" S is a set of triples (a -f-> t), where
  a is a type variable
  t is a type
  f is a flavour
such that
  (WF1) if (a -f1-> t1) in S
           (a -f2-> t2) in S
        then neither (f1 >= f2) nor (f2 >= f1) hold
  (WF2) if (a -f-> t) is in S, then t /= a

Definition [Applying a generalised substitution]
If S is a generalised substitution
   S(f,a) = t,  if (a -fs-> t) in S, and fs >= f
          = a,  otherwise
Application extends naturally to types S(f,t), modulo roles.
See Note [Flavours with roles].

Theorem: S(f,a) is well defined as a function.
Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
               and  f1 >= f and f2 >= f
Simon Peyton Jones's avatar
Simon Peyton Jones committed
763
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
764 765 766 767 768 769 770 771 772 773 774

Notation: repeated application.
  S^0(f,t)     = t
  S^(n+1)(f,t) = S(f, S^n(t))

Definition: inert generalised substitution
A generalised substitution S is "inert" iff

  (IG1) there is an n such that
        for every f,t, S^n(f,t) = S^(n+1)(f,t)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
775 776 777
By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.

778 779 780 781 782 783 784 785 786
----------------------------------------------------------------
Our main invariant:
   the inert CTyEqCans should be an inert generalised substitution
----------------------------------------------------------------

Note that inertness is not the same as idempotence.  To apply S to a
type, you may have to apply it recursive.  But inertness does
guarantee that this recursive use will terminate.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
787 788
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
789
Main Theorem [Stability under extension]
790 791 792
   Suppose we have a "work item"
       a -fw-> t
   and an inert generalised substitution S,
793
   THEN the extended substitution T = S+(a -fw-> t)
794 795
        is an inert generalised substitution
   PROVIDED
796 797 798 799
      (T1) S(fw,a) = a     -- LHS of work-item is a fixpoint of S(fw,_)
      (T2) S(fw,t) = t     -- RHS of work-item is a fixpoint of S(fw,_)
      (T3) a not in t      -- No occurs check in the work item

800 801 802 803 804 805
      AND, for every (b -fs-> s) in S:
           (K0) not (fw >= fs)
                Reason: suppose we kick out (a -fs-> s),
                        and add (a -fw-> t) to the inert set.
                        The latter can't rewrite the former,
                        so the kick-out achieved nothing
806

807 808 809
           OR { (K1) not (a = b)
                     Reason: if fw >= fs, WF1 says we can't have both
                             a -fw-> t  and  a -fs-> s
810

811 812 813 814 815 816 817 818 819
                AND (K2): guarantees inertness of the new substitution
                    {  (K2a) not (fs >= fs)
                    OR (K2b) fs >= fw
                    OR (K2d) a not in s }

                AND (K3) See Note [K3: completeness of solving]
                    { (K3a) If the role of fs is nominal: s /= a
                      (K3b) If the role of fs is representational:
                            s is not of form (a t1 .. tn) } }
820 821


Simon Peyton Jones's avatar
Simon Peyton Jones committed
822
Conditions (T1-T3) are established by the canonicaliser
Gabor Greif's avatar
Gabor Greif committed
823
Conditions (K1-K3) are established by TcSMonad.kickOutRewritable
Simon Peyton Jones's avatar
Simon Peyton Jones committed
824

825 826 827 828 829
The idea is that
* (T1-2) are guaranteed by exhaustively rewriting the work-item
  with S(fw,_).

* T3 is guaranteed by a simple occurs-check on the work item.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
830 831
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
832 833 834 835 836 837 838 839 840 841 842

* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
  "keep" criteria.) If the current inert S contains a triple that does
  not satisfy (K1-3), then we remove it from S by "kicking it out",
  and re-processing it.

* Note that kicking out is a Bad Thing, because it means we have to
  re-process a constraint.  The less we kick out, the better.
  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
  this but haven't done the empirical study to check.

843
* Assume we have  G>=G, G>=W and that's all.  Then, when performing
844 845 846 847
  a unification we add a new given  a -G-> ty.  But doing so does NOT require
  us to kick out an inert wanted that mentions a, because of (K2a).  This
  is a common case, hence good not to kick out.

848
* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
849
  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
850
         and so K0 holds.  Intuitively, since fw can't rewrite anything,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
851 852
         adding it cannot cause any loops
  This is a common case, because Wanteds cannot rewrite Wanteds.
853
  It's used to avoid even looking for constraint to kick out.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
854

855 856 857 858 859 860 861
* Lemma (L1): The conditions of the Main Theorem imply that there is no
              (a -fs-> t) in S, s.t.  (fs >= fw).
  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
  S(fw,a)=a.  But since fs>=fw, S(fw,a) = s, hence s=a.  But now we
  have (a -fs-> a) in S, which contradicts (WF2).

* The extended substitution satisfies (WF1) and (WF2)
Gabor Greif's avatar
Gabor Greif committed
862
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
863 864 865
  - (T3) guarantees (WF2).

* (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
866
  T^1(f,t), T^2(f,T).... must pass through the new work item infinitely
Gabor Greif's avatar
Gabor Greif committed
867
  often, since the substitution without the work item is inert; and must
868
  pass through at least one of the triples in S infinitely often.
869 870 871 872 873 874 875 876 877 878 879 880 881

  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
    and hence this triple never plays a role in application S(f,a).
    It is always safe to extend S with such a triple.

    (NB: we could strengten K1) in this way too, but see K3.

  - (K2b): If this holds then, by (T2), b is not in t.  So applying the
    work item does not genenerate any new opportunities for applying S

  - (K2c): If this holds, we can't pass through this triple infinitely
    often, because if we did then fs>=f, fw>=f, hence by (R2)
      * either fw>=fs, contradicting K2c
Gabor Greif's avatar
Gabor Greif committed
882
      * or fs>=fw; so by the argument in K2b we can't have a loop
883 884 885 886 887 888 889 890 891 892

  - (K2d): if a not in s, we hae no further opportunity to apply the
    work item, similar to (K2b)

  NB: Dimitrios has a PDF that does this in more detail

Key lemma to make it watertight.
  Under the conditions of the Main Theorem,
  forall f st fw >= f, a is not in S^k(f,t), for any k

893
Also, consider roles more carefully. See Note [Flavours with roles]
894

Simon Peyton Jones's avatar
Simon Peyton Jones committed
895 896 897
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930
to be inert.  In fact K1 could be made stronger by saying
   ... then (not (fw >= fs) or not (fs >= fs))
But it's not enough for S to be inert; we also want completeness.
That is, we want to be able to solve all soluble wanted equalities.
Suppose we have

   work-item   b -G-> a
   inert-item  a -W-> b

Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
so we could extend the inerts, thus:

   inert-items   b -G-> a
                 a -W-> b

But if we kicked-out the inert item, we'd get

   work-item     a -W-> b
   inert-item    b -G-> a

Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
So we add one more clause to the kick-out criteria

Another way to understand (K3) is that we treat an inert item
        a -f-> b
in the same way as
        b -f-> a
So if we kick out one, we should kick out the other.  The orientation
is somewhat accidental.

When considering roles, we also need the second clause (K3b). Consider

  work-item    c -G/N-> a
931
  inert-item   a -W/R-> b c
932 933

The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
934 935
But we don't kick out the inert item because not (W/R >= W/R).  So we just
add the work item. But then, consider if we hit the following:
936

937 938 939
  work-item    b -G/N-> Id
  inert-items  a -W/R-> b c
               c -G/N-> a
940 941 942 943 944
where
  newtype Id x = Id x

For similar reasons, if we only had (K3a), we wouldn't kick the
representational inert out. And then, we'd miss solving the inert, which
945 946 947 948 949 950 951 952 953 954 955 956 957 958
now reduced to reflexivity.

The solution here is to kick out representational inerts whenever the
tyvar of a work item is "exposed", where exposed means being at the
head of the top-level application chain (a t1 .. tn).  See
TcType.isTyVarHead. This is encoded in (K3b).

Beware: if we make this test succeed too often, we kick out too much,
and the solver might loop.  Consider (Trac #14363)
  work item:   [G] a ~R f b
  inert item:  [G] b ~R f a
In GHC 8.2 the completeness tests more aggressive, and kicked out
the inert item; but no rewriting happened and there was an infinite
loop.  All we need is to have the tyvar at the head.
959 960 961

Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
962 963
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
964 965 966
set of flavours. In GHC, flavours have two components: the flavour proper,
taken from {Wanted, Derived, Given} and the equality relation (o