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
    updWorkListTcS,
14

15
    -- The TcS monad
16 17
    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
    failTcS, warnTcS,
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, isPendingScDict,
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 TrieMap
154
import Control.Monad
quchen's avatar
quchen committed
155 156 157
#if __GLASGOW_HASKELL__ > 710
import qualified Control.Monad.Fail as MonadFail
#endif
158
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
159
import Data.IORef
160
import Data.List ( foldl', partition )
161

162 163 164
#ifdef DEBUG
import Digraph
#endif
165

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

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

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

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

194
-}
195

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

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

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

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

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

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

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

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

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

     _ -> extendWorkListNonEq ct wl
264

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

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

emptyWorkList :: WorkList
275
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303
                   , 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

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
304

305 306 307
       ; try (selectWorkItem wl) $

    do { ics <- getInertCans
308 309
       ; solve_deriveds <- keepSolvingDeriveds
       ; if inert_count ics == 0 && not solve_deriveds
310 311
         then return Nothing
         else try (selectDerivedWorkItem wl) (return Nothing) } }
dimitris's avatar
dimitris committed
312

313 314
-- Pretty printing
instance Outputable WorkList where
315
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
316
          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
317
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
318
     vcat [ ppUnless (null eqs) $
319
            text "Eqs =" <+> vcat (map ppr eqs)
320
          , ppUnless (null feqs) $
321
            text "Funeqs =" <+> vcat (map ppr feqs)
322
          , ppUnless (null rest) $
323
            text "Non-eqs =" <+> vcat (map ppr rest)
324
          , ppUnless (null ders) $
325
            text "Derived =" <+> vcat (map ppr ders)
326
          , ppUnless (isEmptyBag implics) $
327
            text "Implics =" <+> vcat (map ppr (bagToList implics))
328
          ])
dimitris's avatar
dimitris committed
329

330 331

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
332
*                                                                      *
333
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
334 335
*                                                                      *
*                                                                      *
336
********************************************************************* -}
337

338 339 340 341
data InertSet
  = IS { inert_cans :: InertCans
              -- Canonical Given, Wanted, Derived (no Solved)
              -- Sometimes called "the inert set"
342

343
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
344 345 346 347 348 349 350 351 352 353
              -- 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)
354

355 356
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

357 358 359 360 361
       , inert_solved_dicts   :: DictMap CtEvidence
              -- Of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }
362

363 364 365
instance Outputable InertSet where
  ppr is = vcat [ ppr $ inert_cans is
                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
366

367 368 369 370 371 372 373 374 375 376
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 }
377
       , inert_flat_cache    = emptyExactFunEqs
378
       , inert_solved_dicts  = emptyDictMap }
379

380

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

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

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

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

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

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

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

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

Then we'll use the instance decl to give

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

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

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

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

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

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

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

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

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

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

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

    class Data Maybe a => Foo a

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

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

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

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

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

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

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

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

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

Now, d5 can be solved! d5 := d0

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

541 542 543 544 545 546 547 548 549 550 551 552
{- *********************************************************************
*                                                                      *
                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
553

554
       , inert_funeqs :: FunEqMap Ct
555
              -- All CFunEqCans; index is the whole family head type.
556
              -- All Nominal (that's an invarint of all CFunEqCans)
557 558
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
              --     wrt inert_eqs/inert_model
559 560 561
              -- We can get Derived ones from e.g.
              --   (a) flattening derived equalities
              --   (b) emitDerivedShadows
562 563

       , inert_dicts :: DictMap Ct
564
              -- Dictionaries only
565 566
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs/inert_model
567

568 569 570 571 572 573 574 575 576
       , 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

577
       , inert_irreds :: Cts
578 579
              -- Irreducible predicates

580
       , inert_insols :: Cts
581
              -- Frozen errors (as non-canonicals)
582 583 584 585 586 587

       , 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
588
       }
589

590 591 592 593 594
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
595

596

597 598 599
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
600

601
  * All canonical
602

603 604 605 606 607 608 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
  * 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”
642

643 644 645 646
   * 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.

647 648 649
   * 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.
650 651

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

653
     - Derived constraints arising from functional dependencies, or
654 655
       decomposing injective arguments of type functions, and
       suchlike.
656

657 658
     - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
       inert_eqs.
659

660 661 662 663 664
   * 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.
665

666 667
   * Domain of the model = skolems + untouchables.
     A touchable unification variable wouuld have been unified first.
668 669 670 671

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

672 673
   * However inert_dicts, inert_funeqs, inert_irreds
     may well contain derived costraints.
674 675 676 677 678 679 680 681

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

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

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

      (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
757 758
      (K3) See Note [K3: completeness of solving]
           If (b -fs-> s) is in S with (fw >= fs), then
759 760 761 762 763 764 765 766
        (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
767 768 769
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable

770 771 772 773 774
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
775 776
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
777 778 779 780 781 782 783 784 785 786 787

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

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

799 800 801 802 803 804 805
* 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
806
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836
  - (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

837
Also, consider roles more carefully. See Note [Flavours with roles]
838

Simon Peyton Jones's avatar
Simon Peyton Jones committed
839 840 841
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
842 843 844 845 846 847 848 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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~
917 918 919 920 921 922 923 924 925
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
926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 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

  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
subsitution means that the proof in Note [The inert equalities] may need
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
1040
  See Note [Orientation of equalities with fmvs] in TcFlatten
1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053
      [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!
-}
1054

1055
instance Outputable InertCans where
1056 1057 1058 1059 1060 1061
  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) $
1062
        text "Equalities:"
1063 1064
          <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
      , ppUnless (isEmptyTcAppMap funeqs) $
1065
        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
1066
      , ppUnless (isEmptyTcAppMap dicts) $
1067
        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
1068
      , ppUnless (isEmptyTcAppMap safehask) $
1069
        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1070
      , ppUnless (isEmptyCts irreds) $
1071
        text "Irreds =" <+> pprCts irreds
1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083
      , 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
*                                                                      *
************************************************************************
1084

1085 1086 1087
Note [Adding an inert canonical constraint the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
1088

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

1092 1093 1094 1095 1096
    * 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).

1097 1098 1099
    * Always (G/W/D) kick out constraints that can be rewritten
      (respecting flavours) by the new constraint. This is done
      by kickOutRewritable.
1100 1101 1102 1103

  Then, when adding:

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

1107
        2. (DShadow) Do emitDerivedShadows
1108
             For every inert G/W constraint c, st
Jan Stolarek's avatar
Jan Stolarek committed
1109 1110 1111
              (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
                  and
              (b) the model cannot rewrite c
1112 1113 1114 1115
             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
1116
     * [Given/Wanted] a ~N ty
1117 1118
          1. Add it to inert_eqs
          2. Emit [D] a~ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1119
       As a result of (2), the current model will rewrite the new [D] a~ty
1120 1121
       during canonicalisation, and then it'll be added to the model using
       the steps of [Derived] above.
Jan Stolarek's avatar
Jan Stolarek committed
1122

1123
     * [Representational equalities] a ~R ty: just add it to inert_eqs
Jan Stolarek's avatar
Jan Stolarek committed
1124

1125

1126 1127 1128
* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
  a~ty, as in step (1) of the [G/W] case above.  So instead, do
  kickOutAfterUnification:
1129 1130 1131 1132
    - Kick out from the model any equality (b~ty2) that mentions 'a'
      (i.e. a=b or a in ty2).  Example:
            [G] a ~ [b],    model [D] b ~ [a]