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

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

21
    runTcPluginTcS, addUsedDataCons, deferTcSForAllEq,
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 32 33 34
    newTcEvBinds,
    newWantedEq,
    newWanted, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
    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 44
    getTopEnv, getGblEnv, getLclEnv,
    getTcEvBinds, getTcEvBindsFromVar, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
45
    getTcEvBindsMap,
46
    tcLookupClass,
47

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

    -- The Model
    InertModel, kickOutAfterUnification,
62

63 64 65 66
    -- Inert Safe Haskell safe-overlap failures
    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
    getSafeOverlapFailures,

67
    -- Inert CDictCans
68 69
    lookupInertDict, findDictsByClass, addDict, addDictsByClass,
    delDict, partitionDicts, foldDicts, filterDicts,
70

71
    -- Inert CTyEqCans
72
    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
73 74 75 76

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

77 78 79
    -- Irreds
    foldIrreds,

80 81 82 83
    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems

    -- Inert CFunEqCans
84
    updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs,
85
    findFunEqsByTyCon, partitionFunEqs, foldFunEqs,
86

87
    instDFunType,                              -- Instantiation
88 89

    -- MetaTyVars
90
    newFlexiTcSTy, instFlexiTcS,
91
    cloneMetaTyVar, demoteUnfilledFmv,
92

93
    TcLevel, isTouchableMetaTyVarTcS,
94
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
95 96
    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
    zonkSimples, zonkWC,
97

98 99
    -- References
    newTcRef, readTcRef, updTcRef,
100

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

#include "HsVersions.h"

import HscTypes

116
import qualified Inst as TcM
117 118
import InstEnv
import FamInst
119 120 121 122
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
123
import qualified TcEnv as TcM
124
       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass )
125
import Kind
126 127
import TcType
import DynFlags
128
import Type
129
import Coercion
130
import Unify
131

132
import TcEvidence
133 134
import Class
import TyCon
135
import TcErrors   ( solverDepthErrorTcS )
136

137
import Name
138 139
import RdrName ( GlobalRdrEnv)
import qualified RnEnv as TcM
140
import Var
141
import VarEnv
142
import VarSet
143 144
import Outputable
import Bag
145
import UniqSupply
Ian Lynagh's avatar
Ian Lynagh committed
146
import Util
Ian Lynagh's avatar
Ian Lynagh committed
147
import TcRnTypes
148

149
import Unique
150
import UniqFM
151
import Maybes
152

153
import StaticFlags( opt_PprStyle_Debug )
154
import TrieMap
155
import Control.Monad
quchen's avatar
quchen committed
156 157 158
#if __GLASGOW_HASKELL__ > 710
import qualified Control.Monad.Fail as MonadFail
#endif
159
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
160
import Data.IORef
161
import Data.List ( foldl', partition )
162

163 164 165
#ifdef DEBUG
import Digraph
#endif
166

Austin Seipp's avatar
Austin Seipp committed
167 168 169 170 171 172 173 174 175
{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************
176

177 178
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
179 180 181
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.
182

183
As a simple form of priority queue, our worklist separates out
184 185 186 187
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
188

189 190 191 192 193 194
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.

195
-}
196

197
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
198
data WorkList
199
  = WL { wl_eqs     :: [Ct]
200
       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
201
       , wl_rest    :: [Ct]
202 203
       , wl_deriv   :: [CtEvidence]  -- Implicitly non-canonical
                                     -- See Note [Process derived items last]
204 205
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
206

Simon Peyton Jones's avatar
Simon Peyton Jones committed
207
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
208
appendWorkList
209 210 211 212
    (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 })
213 214 215
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
216
        , wl_deriv   = ders1    ++ ders2
217
        , wl_implics = implics1 `unionBags`   implics2 }
218

219
workListSize :: WorkList -> Int
220 221 222 223 224 225
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
226

227
extendWorkListEq :: Ct -> WorkList -> WorkList
228 229 230 231
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

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

233
extendWorkListFunEq :: Ct -> WorkList -> WorkList
234
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
235

236 237
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
238 239 240 241 242 243 244 245 246 247
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 }
248
  | otherwise                 = extendWorkListEqs (map mkNonCanonical evs) wl
249

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

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

     _ -> extendWorkListNonEq ct wl
265

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

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

emptyWorkList :: WorkList
276
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
277 278 279 280 281 282 283 284 285 286
                   , 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

287 288 289 290
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef
                 ; wrapTcS (TcM.readTcRef wl_var) }

291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
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
309

310 311 312
       ; try (selectWorkItem wl) $

    do { ics <- getInertCans
313 314
       ; solve_deriveds <- keepSolvingDeriveds
       ; if inert_count ics == 0 && not solve_deriveds
315 316
         then return Nothing
         else try (selectDerivedWorkItem wl) (return Nothing) } }
dimitris's avatar
dimitris committed
317

318 319
-- Pretty printing
instance Outputable WorkList where
320
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
321
          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
322
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
323
     vcat [ ppUnless (null eqs) $
324
            text "Eqs =" <+> vcat (map ppr eqs)
325
          , ppUnless (null feqs) $
326
            text "Funeqs =" <+> vcat (map ppr feqs)
327
          , ppUnless (null rest) $
328
            text "Non-eqs =" <+> vcat (map ppr rest)
329
          , ppUnless (null ders) $
330
            text "Derived =" <+> vcat (map ppr ders)
331
          , ppUnless (isEmptyBag implics) $
332 333 334
            if opt_PprStyle_Debug  -- Typically we only want the work list for this level
            then text "Implics =" <+> vcat (map ppr (bagToList implics))
            else text "(Implics omitted)"
335
          ])
dimitris's avatar
dimitris committed
336

337 338

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
339
*                                                                      *
340
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
341 342
*                                                                      *
*                                                                      *
343
********************************************************************* -}
344

345 346 347 348
data InertSet
  = IS { inert_cans :: InertCans
              -- Canonical Given, Wanted, Derived (no Solved)
              -- Sometimes called "the inert set"
349

350
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
351 352 353 354 355 356 357 358 359 360
              -- See Note [Type family equations]
              -- If    F tys :-> (co, ty, ev),
              -- then  co :: F tys ~ ty
              --
              -- 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)
361

362 363
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

364 365 366 367 368
       , inert_solved_dicts   :: DictMap CtEvidence
              -- Of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }
369

370 371 372
instance Outputable InertSet where
  ppr is = vcat [ ppr $ inert_cans is
                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
373

374 375 376 377 378 379 380 381 382 383
emptyInert :: InertSet
emptyInert
  = IS { inert_cans = IC { inert_count    = 0
                         , inert_eqs      = emptyVarEnv
                         , inert_dicts    = emptyDicts
                         , inert_safehask = emptyDicts
                         , inert_funeqs   = emptyFunEqs
                         , inert_irreds   = emptyCts
                         , inert_insols   = emptyCts
                         , inert_model    = emptyVarEnv }
384
       , inert_flat_cache    = emptyExactFunEqs
385
       , inert_solved_dicts  = emptyDictMap }
386

387

388 389
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
When we apply a top-level instance declararation, we add the "solved"
dictionary to the inert_solved_dicts.  In general, we use it to avoid
creating a new EvVar when we have a new goal that we have solved in
the past.

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

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

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

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

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

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

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

Then we'll use the instance decl to give

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

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

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

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

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

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

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

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

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

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

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

    class Data Maybe a => Foo a

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

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

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

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

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

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

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

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

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

Now, d5 can be solved! d5 := d0

Result
   d1 := dfunData2 d2 d3
   d2 := dfunSat d4
   d3 := d01
   d4 := dfunFoo2 d5
   d5 := d0
Austin Seipp's avatar
Austin Seipp committed
546
-}
547

548 549 550 551 552 553 554 555 556 557 558 559
{- *********************************************************************
*                                                                      *
                InertCans: the canonical inerts
*                                                                      *
*                                                                      *
********************************************************************* -}

data InertCans   -- See Note [Detailed InertCans Invariants] for more
  = IC { inert_model :: InertModel

       , inert_eqs :: TyVarEnv EqualCtList
              -- All Given/Wanted CTyEqCans; index is the LHS tyvar
560

561
       , inert_funeqs :: FunEqMap Ct
562
              -- All CFunEqCans; index is the whole family head type.
563
              -- All Nominal (that's an invarint of all CFunEqCans)
564 565
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
              --     wrt inert_eqs/inert_model
566 567 568
              -- We can get Derived ones from e.g.
              --   (a) flattening derived equalities
              --   (b) emitDerivedShadows
569 570

       , inert_dicts :: DictMap Ct
571
              -- Dictionaries only
572 573
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs/inert_model
574

575 576 577 578 579 580 581 582 583
       , inert_safehask :: DictMap Ct
              -- Failed dictionary resolution due to Safe Haskell overlapping
              -- instances restriction. We keep this seperate from inert_dicts
              -- as it doesn't cause compilation failure, just safe inference
              -- failure.
              --
              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
              -- in TcSimplify

584
       , inert_irreds :: Cts
585 586
              -- Irreducible predicates

587
       , inert_insols :: Cts
588
              -- Frozen errors (as non-canonicals)
589 590 591 592 593 594

       , 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
595
       }
596

597 598 599 600 601
type InertModel  = TyVarEnv Ct
     -- If a -> ct, then ct is a
     --    nominal, Derived, canonical CTyEqCan for [D] (a ~N rhs)
     -- The index of the TyVarEnv is the 'a'
     -- All saturated info for Given, Wanted, Derived is here
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
602

603

604 605 606
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
607

608
  * All canonical
609

610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648
  * 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

Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, of form (ev : F tys ~ ty), live in three places

  * The work-list, of course

  * The inert_flat_cache.  This is used when flattening, to get maximal
    sharing.  It contains lots of things that are still in the work-list.
    E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
        work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
        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!

  * The inert_funeqs are un-solved but fully processed and in the InertCans.

Note [inert_model: the inert model]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Part of the inert set is the “model”
649

650 651 652 653
   * The “Model” is an non-idempotent but no-occurs-check
     substitution, reflecting *all* *Nominal* equalities (a ~N ty)
     that are not immediately soluble by unification.

654 655 656
   * All the constraints in the model are Derived CTyEqCans
     That is if (a -> ty) is in the model, then
     we have an inert constraint [D] a ~N ty.
657 658

   * There are two sources of constraints in the model:
659

660
     - Derived constraints arising from functional dependencies, or
661 662
       decomposing injective arguments of type functions, and
       suchlike.
663

664 665
     - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
       inert_eqs.
666

667 668 669 670 671
   * The principal reason for maintaining the model is to generate
     equalities that tell us how to unify a variable: that is, what
     Mark Jones calls "improvement". The same idea is sometimes also
     called "saturation"; find all the equalities that must hold in
     any solution.
672

673 674
   * Domain of the model = skolems + untouchables.
     A touchable unification variable wouuld have been unified first.
675 676 677 678

   * The inert_eqs are all Given/Wanted.  The Derived ones are in the
     inert_model only.

679 680
   * However inert_dicts, inert_funeqs, inert_irreds
     may well contain derived costraints.
681 682 683 684 685 686 687 688

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
689 690
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716
       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
717
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
718 719 720 721 722 723 724 725 726 727 728

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

732 733 734 735 736 737 738 739 740
----------------------------------------------------------------
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
741 742
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
743 744
Theorem [Stability under extension]
   This is the main theorem!
745 746 747 748 749 750 751 752 753
   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
754 755 756
           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
757 758 759 760 761 762 763

      (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
764 765
      (K3) See Note [K3: completeness of solving]
           If (b -fs-> s) is in S with (fw >= fs), then
766 767 768 769 770 771 772 773
        (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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
774 775 776
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable

777 778 779 780 781
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
782 783
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
784 785 786 787 788 789 790 791 792 793 794

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

795
* Assume we have  G>=G, G>=W and that's all.  Then, when performing
796 797 798 799
  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
800 801
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
802
         and so K1-K3 hold.  Intuitively, since fw can't rewrite anything,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
803 804 805
         adding it cannot cause any loops
  This is a common case, because Wanteds cannot rewrite Wanteds.

806 807 808 809 810 811 812
* 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
813
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843
  - (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
  often, since the substution without the work item is inert; and must
  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
      * or fs>=fw; so by the agument in K2b we can't have a loop

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

844
Also, consider roles more carefully. See Note [Flavours with roles]
845

Simon Peyton Jones's avatar
Simon Peyton Jones committed
846 847 848
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 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
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 [Stability of flattening]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The inert_eqs and inert_model, *considered separately* are each stable;
that is, substituting using them will terminate.  Considered *together*
they are not.  E.g.

  Add: [G] a~[b] to inert set with model  [D] b~[a]

  We add [G] a~[b] to inert_eqs, and emit [D] a~[b]. At this point
  the combination of inert_eqs and inert_model is not stable.

  Then we canonicalise [D] a~[b] to [D] a~[[a]], and add that to
  insolubles as an occurs check.

* When canonicalizing, the flattener respects flavours. In particular,
  when flattening a type variable 'a':
    * Derived:      look up 'a' in the inert_model
    * Given/Wanted: look up 'a' in the inert_eqs


Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
924 925 926 927 928 929 930 931 932
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
set of flavours. In GHC, flavours have three components: the flavour proper,
taken from {Wanted, Derived, Given}; the equality relation (often called
role), taken from {NomEq, ReprEq}; and the levity, taken from {Lifted, Unlifted}.
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
933 934 935 936 937 938 939 940 941

  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
942
substitution means that the proof in Note [The inert equalities] may need
943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046
to be revisited, but we don't think that the end conclusion is wrong.

Note [Examples of how the inert_model helps completeness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

----------- Example 2 (indexed-types/should_fail/T4093a)
  Ambiguity check for f: (Foo e ~ Maybe e) => Foo e

  We get [G] Foo e ~ Maybe e
         [W] Foo e ~ Foo ee      -- ee is a unification variable
         [W] Foo ee ~ Maybe ee

  Flatten: [G] Foo e ~ fsk
           [G] fsk ~ Maybe e   -- (A)

           [W] Foo ee ~ fmv
           [W] fmv ~ fsk       -- (B) From Foo e ~ Foo ee
           [W] fmv ~ Maybe ee

  --> rewrite (B) with (A)
           [W] Foo ee ~ fmv
           [W] fmv ~ Maybe e
           [W] fmv ~ Maybe ee

  But now awe appear to be stuck, since we don't rewrite Wanteds with
  Wanteds. But inert_model to the rescue.  In the model we first added
           fmv -> Maybe e
  Then when adding [W] fmv -> Maybe ee to the inert set, we noticed
  that the model can rewrite the constraint, and so emit [D] fmv ~ Maybe ee.
  That canonicalises to
           [D] Maybe e ~ Maybe ee
  and that soon yields ee := e, and all is well

----------- Example 3 (typecheck/should_compile/Improvement.hs)
    type instance F Int = Bool
    instance (b~Int) => C Bool b

    [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool

  If we rewrote wanteds with wanteds, we could rewrite w1 to
  C Bool alpha, use the instance to get alpha ~ Int, and solve
  the whole thing.

  And that is exactly what happens, in the *Derived* constraints.
  In effect we get

    [D] F alpha ~ fmv
    [D] C fmv alpha
    [D] fmv ~ Bool

  and now we can rewrite (C fmv alpha) with (fmv ~ Bool), ane
  we are off to the races.

----------- Example 4 (Trac #10009, a nasty example):

    f :: (UnF (F b) ~ b) => F b -> ()

    g :: forall a. (UnF (F a) ~ a) => a -> ()
    g _ = f (undefined :: F a)

  For g we get [G] UnF (F a) ~ a
               [W] UnF (F beta) ~ beta
               [W] F a ~ F beta
  Flatten:
      [G] g1: F a ~ fsk1         fsk1 := F a
      [G] g2: UnF fsk1 ~ fsk2    fsk2 := UnF fsk1
      [G] g3: fsk2 ~ a

      [W] w1: F beta ~ fmv1
      [W] w2: UnF fmv1 ~ fmv2
      [W] w3: beta ~ fmv2
      [W] w5: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
                            -- and re-orient to put meta-var on left

  Unify beta := fmv2
      [W] w1: F fmv2 ~ fmv1
      [W] w2: UnF fmv1 ~ fmv2
      [W] w5: fmv1 ~ fsk1

  In the model, we have the shadow Deriveds of w1 and w2
  (I name them for convenience even though they are anonymous)
      [D] d1: F fmv2 ~ fmv1d
      [D] d2: fmv1d ~ fmv1
      [D] d3: UnF fmv1 ~ fmv2d
      [D] d4: fmv2d ~ fmv2

  Now we can rewrite d3 with w5, and match with g2, to get
      fmv2d := fsk2
      [D] d1: F fmv2 ~ fmv1d
      [D] d2: fmv1d ~ fmv1
      [D] d4: fmv2 ~ fsk2

  Use g2 to rewrite fsk2 to a.
      [D] d1: F fmv2 ~ fmv1d
      [D] d2: fmv1d ~ fmv1
      [D] d4: fmv2 ~ a

  Use d4 to rewrite d1, rewrite with g3,
  match with g1, to get
      fmv1d := fsk1
      [D] d2: fmv1 ~ fsk1
      [D] d4: fmv2 ~ a

  At this point we are stuck so we unflatten this set:
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1047
  See Note [Orientation of equalities with fmvs] in TcFlatten
1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060
      [W] w1: F fmv2 ~ fmv1
      [W] w2: UnF fmv1 ~ fmv2
      [W] w5: fmv1 ~ fsk1
      [D] d4: fmv2 ~ a

  Unflattening will discharge w1: fmv1 := F fmv2
  It can't discharge w2, so it is kept.  But we can
  unify fmv2 := fsk2, and that is "progress". Result
      [W] w2: UnF (F a) ~ a
      [W] w5: F a ~ fsk1

  And now both of these are easily proved in the next iteration.  Phew!
-}
1061

1062
instance Outputable InertCans where
1063 1064 1065 1066 1067 1068
  ppr (IC { inert_model = model, inert_eqs = eqs
          , inert_funeqs = funeqs, inert_dicts = dicts
          , inert_safehask = safehask, inert_irreds = irreds
          , inert_insols = insols, inert_count = count })
    = braces $ vcat
      [ ppUnless (isEmptyVarEnv eqs) $
1069
        text "Equalities:"
1070 1071
          <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
      , ppUnless (isEmptyTcAppMap funeqs) $
1072
        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
1073
      , ppUnless (isEmptyTcAppMap dicts) $
1074
        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
1075
      , ppUnless (isEmptyTcAppMap safehask) $
1076
        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1077
      , ppUnless (isEmptyCts irreds) $
1078
        text "Irreds =" <+> pprCts irreds
1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090
      , ppUnless (isEmptyCts insols) $
        text "Insolubles =" <+> pprCts insols
      , ppUnless (isEmptyVarEnv model) $
        text "Model =" <+> pprCts (foldVarEnv consCts emptyCts model)
      , text "Unsolved goals =" <+> int count
      ]

{- *********************************************************************
*                                                                      *
                  Adding an inert
*                                                                      *
************************************************************************
1091

1092 1093 1094
Note [Adding an inert canonical constraint the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
1095

Jan Stolarek's avatar
Jan Stolarek committed
1096 1097
    * If c can be rewritten by model, emit the shadow constraint [D] c
      as NonCanonical.   See Note [Emitting shadow constraints]
1098

1099 1100 1101 1102 1103
    * Reason for non-canonical: a CFunEqCan has a unique fmv on the RHS,
      so we must not duplicate it.

* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).

1104 1105 1106
    * Always (G/W/D) kick out constraints that can be rewritten
      (respecting flavours) by the new constraint. This is done
      by kickOutRewritable.
1107 1108 1109 1110

  Then, when adding:

     * [Derived] a ~N ty
Jan Stolarek's avatar
Jan Stolarek committed
1111 1112 1113
        1. Add (a~ty) to the model
           NB: 'a' cannot be in fv(ty), because the constraint is canonical.

1114
        2. (DShadow) Do emitDerivedShadows
1115
             For every inert G/W constraint c, st
Jan Stolarek's avatar
Jan Stolarek committed
1116 1117 1118
              (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
                  and
              (b) the model cannot rewrite c
1119 1120 1121 1122
             kick out a Derived *copy*, leaving the original unchanged.
             Reason for (b) if the model can rewrite c, then we have already
             generated a shadow copy

Jan Stolarek's avatar
Jan Stolarek committed
1123
     * [Given/Wanted] a ~N ty
1124 1125
          1. Add it to inert_eqs
          2. Emit [D] a~ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1126
       As a result of (2), the current model will rewrite the new [D] a~ty
1127 1128
       during canonicalisation, and then it'll be added to the model using
       the steps of [Derived] above.
Jan Stolarek's avatar
Jan Stolarek committed
1129