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, extendWorkListDerived,
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 40
    emitNewDerived, emitNewDeriveds, emitNewDerivedEq,
    checkReductionDepth,
41

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

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

    -- The Model
64
    kickOutAfterUnification,
65

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

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

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

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

81 82 83
    -- Irreds
    foldIrreds,

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

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

91
    instDFunType,                              -- Instantiation
92 93

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

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

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

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

#include "HsVersions.h"

import HscTypes

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

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

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

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

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

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

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

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

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

191
As a simple form of priority queue, our worklist separates out
192 193 194 195
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
196

197 198 199 200 201 202
Note [Process derived items last]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can often solve all goals without processing *any* derived constraints.
The derived constraints are just there to help us if we get stuck.  So
we keep them in a separate list.

203 204 205 206 207 208 209 210 211 212 213 214 215
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.

216
  NB: since we do not currently apply the substitution to the
217 218
  inert_solved_dicts, the knot-tying still seems a bit fragile.
  But this makes it better.
219
-}
220

221
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
222
data WorkList
223 224 225 226
  = WL { wl_eqs     :: [Ct]  -- Both equality constraints and their
                             -- class-level variants (a~b) and (a~~b);
                             -- See Note [Prioritise class equalities]

227
       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
228

229
       , wl_rest    :: [Ct]
230

231 232
       , wl_deriv   :: [CtEvidence]  -- Implicitly non-canonical
                                     -- See Note [Process derived items last]
233

234 235
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
236

Simon Peyton Jones's avatar
Simon Peyton Jones committed
237
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
238
appendWorkList
239 240 241 242
    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
        , wl_deriv = ders1, wl_implics = implics1 })
    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
        , wl_deriv = ders2, wl_implics = implics2 })
243 244 245
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
246
        , wl_deriv   = ders1    ++ ders2
247
        , wl_implics = implics1 `unionBags`   implics2 }
248

249
workListSize :: WorkList -> Int
250 251 252 253 254 255
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest })
  = length eqs + length funeqs + length rest + length ders

workListWantedCount :: WorkList -> Int
workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
  = count isWantedCt eqs + count isWantedCt rest
256

257
extendWorkListEq :: Ct -> WorkList -> WorkList
258 259 260 261
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

extendWorkListEqs :: [Ct] -> WorkList -> WorkList
extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl }
262

263
extendWorkListFunEq :: Ct -> WorkList -> WorkList
264
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
265

266 267
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
268 269 270 271 272 273 274 275 276 277
extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }

extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList
extendWorkListDerived loc ev wl
  | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl }
  | otherwise                 = extendWorkListEq (mkNonCanonical ev) wl

extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds loc evs wl
  | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl }
278
  | otherwise                 = extendWorkListEqs (map mkNonCanonical evs) wl
279

280 281
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
282

283 284 285
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
286
 = case classifyPredType (ctPred ct) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
287
     EqPred NomEq ty1 _
Ben Gamari's avatar
Ben Gamari committed
288
       | Just tc <- tcTyConAppTyCon_maybe ty1
289
       , isTypeFamilyTyCon tc
290
       -> extendWorkListFunEq ct wl
291

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
292
     EqPred {}
293 294
       -> extendWorkListEq ct wl

Gabor Greif's avatar
Gabor Greif committed
295
     ClassPred cls _  -- See Note [Prioritise class equalities]
296 297 298 299
       |  cls `hasKey` heqTyConKey
       || cls `hasKey` eqTyConKey
       -> extendWorkListEq ct wl

300
     _ -> extendWorkListNonEq ct wl
301

Simon Peyton Jones's avatar
Simon Peyton Jones committed
302
extendWorkListCts :: [Ct] -> WorkList -> WorkList
303
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
304
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
305 306

isEmptyWorkList :: WorkList -> Bool
307
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
308 309
                    , wl_rest = rest, wl_deriv = ders, wl_implics = implics })
  = null eqs && null rest && null funeqs && isEmptyBag implics && null ders
310 311

emptyWorkList :: WorkList
312
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
313 314 315 316 317 318 319 320 321 322
                   , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag }

selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
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

323 324 325 326
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef
                 ; wrapTcS (TcM.readTcRef wl_var) }

327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
selectDerivedWorkItem  :: WorkList -> Maybe (Ct, WorkList)
selectDerivedWorkItem wl@(WL { wl_deriv = ders })
  | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv  = evs })
  | otherwise      = Nothing

selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
  = do { wl_var <- getTcSWorkListRef
       ; wl <- wrapTcS (TcM.readTcRef wl_var)

       ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct)
             try mb_work do_this_if_fail
                | Just (ct, new_wl) <- mb_work
                = do { checkReductionDepth (ctLoc ct) (ctPred ct)
                     ; wrapTcS (TcM.writeTcRef wl_var new_wl)
                     ; return (Just ct) }
                | otherwise
                = do_this_if_fail
dimitris's avatar
dimitris committed
345

346 347 348
       ; try (selectWorkItem wl) $

    do { ics <- getInertCans
349
       ; if inert_count ics == 0
350 351
         then return Nothing
         else try (selectDerivedWorkItem wl) (return Nothing) } }
dimitris's avatar
dimitris committed
352

353 354
-- Pretty printing
instance Outputable WorkList where
355
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
356
          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
357
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
358
     vcat [ ppUnless (null eqs) $
359
            text "Eqs =" <+> vcat (map ppr eqs)
360
          , ppUnless (null feqs) $
361
            text "Funeqs =" <+> vcat (map ppr feqs)
362
          , ppUnless (null rest) $
363
            text "Non-eqs =" <+> vcat (map ppr rest)
364
          , ppUnless (null ders) $
365
            text "Derived =" <+> vcat (map ppr ders)
366
          , ppUnless (isEmptyBag implics) $
Sylvain Henry's avatar
Sylvain Henry committed
367 368
            sdocWithPprDebug $ \dbg ->
            if dbg  -- Typically we only want the work list for this level
369 370
            then text "Implics =" <+> vcat (map ppr (bagToList implics))
            else text "(Implics omitted)"
371
          ])
dimitris's avatar
dimitris committed
372

373 374

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
375
*                                                                      *
376
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
377 378
*                                                                      *
*                                                                      *
379
********************************************************************* -}
380

381 382
data InertSet
  = IS { inert_cans :: InertCans
383
              -- Canonical Given, Wanted, Derived
384
              -- Sometimes called "the inert set"
385

386 387 388 389 390 391 392 393 394 395
       , 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.

396
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
397
              -- See Note [Type family equations]
398 399 400
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: F tys ~ rhs
              --       flav is [G] or [WD]
401 402 403 404 405 406 407
              --
              -- 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)
408

409 410
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

411 412 413 414 415
       , inert_solved_dicts   :: DictMap CtEvidence
              -- Of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }
416

417 418
instance Outputable InertSet where
  ppr is = vcat [ ppr $ inert_cans is
419 420 421 422
                , ppUnless (null dicts) $
                  text "Solved dicts" <+> vcat (map ppr dicts) ]
         where
           dicts = bagToList (dictsToBag (inert_solved_dicts is))
423

424 425 426
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_count    = 0
427
                         , inert_eqs      = emptyDVarEnv
428 429 430 431
                         , inert_dicts    = emptyDicts
                         , inert_safehask = emptyDicts
                         , inert_funeqs   = emptyFunEqs
                         , inert_irreds   = emptyCts
432
                         , inert_insols   = emptyCts }
433
       , inert_flat_cache    = emptyExactFunEqs
434
       , inert_fsks          = []
435
       , inert_solved_dicts  = emptyDictMap }
436

437

438 439
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
440
When we apply a top-level instance declaration, we add the "solved"
441 442 443 444
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.

445
But in particular, we can use it to create *recursive* dictionaries.
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 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
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
596
-}
597

598 599 600 601 602 603 604 605
{- *********************************************************************
*                                                                      *
                InertCans: the canonical inerts
*                                                                      *
*                                                                      *
********************************************************************* -}

data InertCans   -- See Note [Detailed InertCans Invariants] for more
606
  = IC { inert_eqs :: InertEqs
607
              -- See Note [inert_eqs: the inert equalities]
608 609
              -- All CTyEqCans; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified
610

611
       , inert_funeqs :: FunEqMap Ct
612
              -- All CFunEqCans; index is the whole family head type.
613
              -- All Nominal (that's an invarint of all CFunEqCans)
614
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
615 616 617
              --     wrt inert_eqs
              -- Can include all flavours, [G], [W], [WD], [D]
              -- See Note [Type family equations]
618 619

       , inert_dicts :: DictMap Ct
620
              -- Dictionaries only
621
              -- All fully rewritten (modulo flavour constraints)
622
              --     wrt inert_eqs
623

624 625
       , inert_safehask :: DictMap Ct
              -- Failed dictionary resolution due to Safe Haskell overlapping
Gabor Greif's avatar
Gabor Greif committed
626
              -- instances restriction. We keep this separate from inert_dicts
627 628 629 630 631 632
              -- as it doesn't cause compilation failure, just safe inference
              -- failure.
              --
              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
              -- in TcSimplify

633
       , inert_irreds :: Cts
634 635
              -- Irreducible predicates

636
       , inert_insols :: Cts
637
              -- Frozen errors (as non-canonicals)
638 639 640 641 642 643

       , inert_count :: Int
              -- Number of Wanted goals in
              --     inert_eqs, inert_dicts, inert_safehask, inert_irreds
              -- Does not include insolubles
              -- When non-zero, keep trying to solved
644
       }
645

646 647
type InertEqs    = DTyVarEnv EqualCtList
type EqualCtList = [Ct]  -- See Note [EqualCtList invariants]
648

649
{- Note [Detailed InertCans Invariants]
650
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
651
The InertCans represents a collection of constraints with the following properties:
652

653
  * All canonical
654

655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671
  * 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

672 673 674 675 676 677 678 679 680 681 682 683 684 685
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

686 687
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 689
Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
live in three places
690 691 692

  * The work-list, of course

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

696
  * The inert_flat_cache.  This is used when flattening, to get maximal
697 698 699
    sharing. Everthing in the inert_flat_cache is [G] or [WD]

    It contains lots of things that are still in the work-list.
700 701 702 703 704 705 706 707
    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!

708
The CFunEqCan Ownership Invariant:
709

710 711 712 713 714
  * 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)
715

716 717 718 719
  * 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
720 721 722 723 724 725 726 727


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
728 729
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755
       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
756
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
757 758 759 760 761 762 763 764 765 766 767

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
768 769 770
By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.

771 772 773 774 775 776 777 778 779
----------------------------------------------------------------
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
780 781
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
782 783
Theorem [Stability under extension]
   This is the main theorem!
784 785 786 787 788 789 790 791 792
   Suppose we have a "work item"
       a -fw-> t
   and an inert generalised substitution S,
   such that
      (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

      (K1) for every (a -fs-> s) in S, then not (fw >= fs)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
793 794 795
           Reason: the work item is fully rewritten by S, hence not (fs >= fw)
                   but if (fw >= fs) then the work item could rewrite
                   the inert item
796 797 798 799 800 801 802

      (K2) for every (b -fs-> s) in S, where b /= a, then
              (K2a) not (fs >= fs)
           or (K2b) fs >= fw
           or (K2c) not (fw >= fs)
           or (K2d) a not in s

Simon Peyton Jones's avatar
Simon Peyton Jones committed
803 804
      (K3) See Note [K3: completeness of solving]
           If (b -fs-> s) is in S with (fw >= fs), then
805 806 807 808 809
        (K3a) If the role of fs is nominal: s /= a
        (K3b) If the role of fs is representational: EITHER
                a not in s, OR
                the path from the top of s to a includes at least one non-newtype

810
   then the extended substitution T = S+(a -fw-> t)
811 812
   is an inert generalised substitution.

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

816 817 818 819 820
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
821 822
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
823 824 825 826 827 828 829 830 831 832 833

* (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.

834
* Assume we have  G>=G, G>=W and that's all.  Then, when performing
835 836 837 838
  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.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
839 840
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
841
         and so K1-K3 hold.  Intuitively, since fw can't rewrite anything,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
842 843 844
         adding it cannot cause any loops
  This is a common case, because Wanteds cannot rewrite Wanteds.

845 846 847 848 849 850 851
* 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
852
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
853 854 855 856
  - (T3) guarantees (WF2).

* (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
  T^1(f,t), T^2(f,T).... must pass through the new work item infnitely
Gabor Greif's avatar
Gabor Greif committed
857
  often, since the substitution without the work item is inert; and must
858 859 860 861 862 863 864 865 866 867 868 869 870 871
  pass through at least one of the triples in S infnitely often.

  - (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
872
      * or fs>=fw; so by the argument in K2b we can't have a loop
873 874 875 876 877 878 879 880 881 882

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

883
Also, consider roles more carefully. See Note [Flavours with roles]
884

Simon Peyton Jones's avatar
Simon Peyton Jones committed
885 886 887
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
888 889 890 891 892 893 894 895 896 897 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 931 932 933 934 935 936 937 938 939 940 941 942
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

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

The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were
condition (K3a), then we would keep the inert around and add the work item.
But then, consider if we hit the following:

  work-item2   b -G/N-> Id

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
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
not under some proper data-type constructor, like [] or Maybe. See
isTyVarExposed in TcType. This is encoded in (K3b).

Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
943 944
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
945 946 947
set of flavours. In GHC, flavours have two components: the flavour proper,
taken from {Wanted, Derived, Given} and the equality relation (often called
role), taken from {NomEq, ReprEq}.
948 949 950 951
When substituting w.r.t. the inert set,
as described in Note [inert_eqs: the inert equalities],
we must be careful to respect all components of a flavour.
For example, if we have
952 953 954 955 956 957 958 959 960

  inert set: a -G/R-> Int
             b -G/R-> Bool

  type role T nominal representational

and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
T Int Bool. The reason is that T's first parameter has a nominal role, and
thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
Gabor Greif's avatar
Gabor Greif committed
961
substitution means that the proof in Note [The inert equalities] may need
962 963
to be revisited, but we don't think that the end conclusion is wrong.
-}
964

965
instance Outputable InertCans where
966
  ppr (IC { inert_eqs = eqs
967 968 969 970
          , inert_funeqs = funeqs, inert_dicts = dicts
          , inert_safehask = safehask, inert_irreds = irreds
          , inert_insols = insols, inert_count = count })
    = braces $ vcat
971
      [ ppUnless (isEmptyDVarEnv eqs) $
972
        text "Equalities:"
973
          <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
974
      , ppUnless (isEmptyTcAppMap funeqs) $
975
        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
976
      , ppUnless (isEmptyTcAppMap dicts) $
977
        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
978
      , ppUnless (isEmptyTcAppMap safehask) $
979
        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
980
      , ppUnless (isEmptyCts irreds) $
981
        text "Irreds =" <+> pprCts irreds