TcSMonad.hs 118 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, getEvExpr,
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
    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 Module ( HasModule, getModule )
147
import RdrName ( GlobalRdrEnv, GlobalRdrElt )
148
import qualified RnEnv as TcM
149
import Var
150
import VarEnv
151
import VarSet
152 153
import Outputable
import Bag
154
import UniqSupply
Ian Lynagh's avatar
Ian Lynagh committed
155
import Util
Ian Lynagh's avatar
Ian Lynagh committed
156
import TcRnTypes
157

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

163
import TrieMap
164
import Control.Monad
quchen's avatar
quchen committed
165
import qualified Control.Monad.Fail as MonadFail
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
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
254 255
-- Count the things we need to solve
-- excluding the insolubles (c.f. inert_count)
256
workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
257 258 259 260 261 262 263
  = 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
264

265
extendWorkListEq :: Ct -> WorkList -> WorkList
266 267 268 269
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

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

271
extendWorkListFunEq :: Ct -> WorkList -> WorkList
272
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
273

274 275
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
276 277 278 279 280 281 282 283 284 285
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 }
286
  | otherwise                 = extendWorkListEqs (map mkNonCanonical evs) wl
287

288 289
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
290

291 292 293
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
294
 = case classifyPredType (ctPred ct) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
295
     EqPred NomEq ty1 _
Ben Gamari's avatar
Ben Gamari committed
296
       | Just tc <- tcTyConAppTyCon_maybe ty1
297
       , isTypeFamilyTyCon tc
298
       -> extendWorkListFunEq ct wl
299

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
300
     EqPred {}
301 302
       -> extendWorkListEq ct wl

Gabor Greif's avatar
Gabor Greif committed
303
     ClassPred cls _  -- See Note [Prioritise class equalities]
304 305 306 307
       |  cls `hasKey` heqTyConKey
       || cls `hasKey` eqTyConKey
       -> extendWorkListEq ct wl

308
     _ -> extendWorkListNonEq ct wl
309

Simon Peyton Jones's avatar
Simon Peyton Jones committed
310
extendWorkListCts :: [Ct] -> WorkList -> WorkList
311
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
312
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
313 314

isEmptyWorkList :: WorkList -> Bool
315
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
316 317
                    , wl_rest = rest, wl_deriv = ders, wl_implics = implics })
  = null eqs && null rest && null funeqs && isEmptyBag implics && null ders
318 319

emptyWorkList :: WorkList
320
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
321 322 323 324 325 326 327 328 329 330
                   , 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

331 332 333 334
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef
                 ; wrapTcS (TcM.readTcRef wl_var) }

335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352
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
353

354 355 356
       ; try (selectWorkItem wl) $

    do { ics <- getInertCans
357
       ; if inert_count ics == 0
358 359
         then return Nothing
         else try (selectDerivedWorkItem wl) (return Nothing) } }
dimitris's avatar
dimitris committed
360

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

379 380

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
381
*                                                                      *
382
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
383 384
*                                                                      *
*                                                                      *
385
********************************************************************* -}
386

387 388
data InertSet
  = IS { inert_cans :: InertCans
389
              -- Canonical Given, Wanted, Derived
390
              -- Sometimes called "the inert set"
391

392 393 394 395 396 397 398 399 400 401
       , 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.

402
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
403
              -- See Note [Type family equations]
404 405 406
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: F tys ~ rhs
              --       flav is [G] or [WD]
407 408 409 410 411 412 413
              --
              -- 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)
414

415 416
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

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

423
instance Outputable InertSet where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
424 425 426 427 428 429 430
  ppr (IS { inert_cans = ics
          , inert_fsks = ifsks
          , inert_solved_dicts = solved_dicts })
      = vcat [ ppr ics
             , text "Inert fsks =" <+> ppr ifsks
             , ppUnless (null dicts) $
               text "Solved dicts =" <+> vcat (map ppr dicts) ]
431
         where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
432
           dicts = bagToList (dictsToBag solved_dicts)
433

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

446

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

454
But in particular, we can use it to create *recursive* dictionaries.
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 604
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
605
-}
606

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

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

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

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

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

642
       , inert_irreds :: Cts
643 644 645
              -- 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])
646 647 648 649 650 651

       , 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
652
       }
653

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

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

661
  * All canonical
662

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

680 681 682 683 684 685 686 687 688 689 690 691 692 693
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

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

  * The work-list, of course

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

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

    It contains lots of things that are still in the work-list.
708 709 710 711 712 713 714 715
    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!

716
The CFunEqCan Ownership Invariant:
717

718 719 720 721 722
  * 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)
723

724 725 726 727
  * 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
728 729 730 731 732 733 734 735


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
736 737
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
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 763
       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
764
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
765 766 767 768 769 770 771 772 773 774 775

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

779 780 781 782 783 784 785 786 787
----------------------------------------------------------------
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
788 789
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
790
Main Theorem [Stability under extension]
791 792 793
   Suppose we have a "work item"
       a -fw-> t
   and an inert generalised substitution S,
794
   THEN the extended substitution T = S+(a -fw-> t)
795 796
        is an inert generalised substitution
   PROVIDED
797 798 799 800
      (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

801 802 803 804 805 806
      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
807

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

812 813 814 815 816 817 818 819 820
                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) } }
821 822


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

826 827 828 829 830
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
831 832
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
833 834 835 836 837 838 839 840 841 842 843

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

844
* Assume we have  G>=G, G>=W and that's all.  Then, when performing
845 846 847 848
  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.

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

856 857 858 859 860 861 862
* 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
863
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
864 865 866
  - (T3) guarantees (WF2).

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

  - (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
Gabor Greif's avatar
Gabor Greif committed
878
    work item does not generate any new opportunities for applying S
879 880 881 882

  - (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
883
      * or fs>=fw; so by the argument in K2b we can't have a loop
884 885 886 887 888 889 890 891 892 893

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
896 897 898
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
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
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
932
  inert-item   a -W/R-> b c
933 934

The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
935 936
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:
937

938 939 940
  work-item    b -G/N-> Id
  inert-items  a -W/R-> b c
               c -G/N-> a
941 942 943 944 945
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
946 947 948 949 950 951 952 953 954 955 956 957 958 959
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.
960 961 962

Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
963 964
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
965 966 967
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}.
968 969 970 971
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
972 973 974 975 976 977 978 979 980

  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
981
substitution means that the proof in Note [The inert equalities] may need
982 983
to be revisited, but we don't think that the end conclusion is wrong.
-}
984

985
instance Outputable InertCans where
986
  ppr (IC { inert_eqs = eqs
987 988
          , inert_funeqs = funeqs, inert_dicts = dicts
          , inert_safehask = safehask, inert_irreds = irreds
989
          , inert_count = count })
990
    = braces $ vcat
991
      [ ppUnless (isEmptyDVarEnv eqs) $
992
        text "Equalities:"
993
          <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
994
      , ppUnless (isEmptyTcAppMap funeqs) $
995
        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
996
      , ppUnless (isEmptyTcAppMap dicts) $
997
        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
998
      , ppUnless (isEmptyTcAppMap safehask) $
999
        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1000
      , ppUnless (isEmptyCts irreds) $