TcSMonad.hs 113 KB
Newer Older
1 2
{-# LANGUAGE CPP, TypeFamilies #-}

3
-- Type definitions for the constraint solver
4
module TcSMonad (
5

6
    -- The work list
7
    WorkList(..), isEmptyWorkList, emptyWorkList,
8
    extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
9
    extendWorkListCts, extendWorkListEq, appendWorkList,
10 11
    selectNextWorkItem,
    workListSize, workListWantedCount,
12
    updWorkListTcS,
13

14
    -- The TcS monad
15 16 17
    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, failTcS,
    runTcSEqualities,
    nestTcS, nestImplicTcS,
18

19
    runTcPluginTcS, addUsedDataCons, deferTcSForAllEq,
20

21 22
    -- Tracing etc
    panicTcS, traceTcS,
23
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
24
    wrapErrTcS, wrapWarnTcS,
25

26
    -- Evidence creation and transformation
27
    MaybeNew(..), freshGoals, isFresh, getEvTerm,
28

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

40
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
41 42
    getTopEnv, getGblEnv, getLclEnv,
    getTcEvBinds, getTcEvBindsFromVar, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
43
    getTcEvBindsMap,
44
    tcLookupClass,
45

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

    -- The Model
    InertModel, kickOutAfterUnification,
60

61 62 63 64
    -- Inert Safe Haskell safe-overlap failures
    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
    getSafeOverlapFailures,

65
    -- Inert CDictCans
66 67
    lookupInertDict, findDictsByClass, addDict, addDictsByClass,
    delDict, partitionDicts, foldDicts, filterDicts,
68

69
    -- Inert CTyEqCans
70
    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
71 72 73 74

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

75 76 77
    -- Irreds
    foldIrreds,

78 79 80 81
    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems

    -- Inert CFunEqCans
82
    updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs,
83
    findFunEqsByTyCon, partitionFunEqs, foldFunEqs,
84

85
    instDFunType,                              -- Instantiation
86 87

    -- MetaTyVars
88
    newFlexiTcSTy, instFlexiTcS,
89
    cloneMetaTyVar, demoteUnfilledFmv,
90

91
    TcLevel, isTouchableMetaTyVarTcS,
92
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
93 94
    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
    zonkSimples, zonkWC,
95

96 97
    -- References
    newTcRef, readTcRef, updTcRef,
98

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

#include "HsVersions.h"

import HscTypes

114
import qualified Inst as TcM
115 116
import InstEnv
import FamInst
117 118 119 120
import FamInstEnv

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

130
import TcEvidence
131 132
import Class
import TyCon
133
import TcErrors   ( solverDepthErrorTcS )
134

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

148
import Unique
149
import UniqFM
150
import Maybes
151

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

161 162 163
#ifdef DEBUG
import Digraph
#endif
164

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

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

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

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

193
-}
194

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

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

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

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

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

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

234 235
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
236 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 }
  | otherwise                  = extendWorkListEqs (map mkNonCanonical evs) wl
247

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

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

     _ -> extendWorkListNonEq ct wl
263

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

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

emptyWorkList :: WorkList
274
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
275 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
                   , 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
303

304 305 306
       ; try (selectWorkItem wl) $

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

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

329 330

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

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

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

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

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

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

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

379

380 381
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
382 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
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
538
-}
539

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

553
       , inert_funeqs :: FunEqMap Ct
554
              -- All CFunEqCans; index is the whole family head type.
555 556 557 558
              -- All Nominal (that's an invarint of all CFunEqCans)
              -- We can get Derived ones from e.g.
              --   (a) flattening derived equalities
              --   (b) emitDerivedShadows
559 560

       , inert_dicts :: DictMap Ct
561
              -- Dictionaries only
562

563 564 565 566 567 568 569 570 571
       , 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

572
       , inert_irreds :: Cts
573 574
              -- Irreducible predicates

575
       , inert_insols :: Cts
576
              -- Frozen errors (as non-canonicals)
577 578 579 580 581 582

       , 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
583
       }
584

585 586 587 588 589
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
590

591

592 593 594
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
595

596
  * All canonical
597

598 599 600 601 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 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672
  * 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”
   * 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.

   * The principal reason for maintaining the model is to generate equalities
     that tell us how 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.

   * There are two sources of constraints in the model:
     - Derived constraints arising from functional dependencies, or
       decomposing injective arguments of type functions, and suchlike.

     - A "shadow copy" for every Given or Wanted (a ~N ty) in
       inert_eqs.  We imagine that every G/W immediately generates its shadow
       constraint, but we refrain from actually generating the constraint itself
       until necessary.  See (DShadow) and (GWShadow) in
       Note [Adding an inert canonical constraint the InertCans]

   * If (a -> ty) is in the model, then it is
     as if we had an inert constraint [D] a ~N ty.

   * Domain of the model = skolems + untouchables

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

   * However inert_dicts, inert_irreds may well contain derived costraints.

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
673 674
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700
       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
701
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
702 703 704 705 706 707 708 709 710 711 712

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

716 717 718 719 720 721 722 723 724
----------------------------------------------------------------
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
725 726
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
727 728
Theorem [Stability under extension]
   This is the main theorem!
729 730 731 732 733 734 735 736 737
   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
738 739 740
           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
741 742 743 744 745 746 747

      (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
748 749
      (K3) See Note [K3: completeness of solving]
           If (b -fs-> s) is in S with (fw >= fs), then
750 751 752 753 754 755 756 757
        (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
758 759 760
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable

761 762 763 764 765
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
766 767
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
768 769 770 771 772 773 774 775 776 777 778

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

779
* Assume we have  G>=G, G>=W and that's all.  Then, when performing
780 781 782 783
  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
784 785 786 787 788 789
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
         and so K1-K3 hold.  Intuitivel, since fw can't rewrite anything,
         adding it cannot cause any loops
  This is a common case, because Wanteds cannot rewrite Wanteds.

790 791 792 793 794 795 796
* 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
797
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827
  - (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

828
Also, consider roles more carefully. See Note [Flavours with roles]
829

Simon Peyton Jones's avatar
Simon Peyton Jones committed
830 831 832
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
833 834 835 836 837 838 839 840 841 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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~
908 909 910 911 912 913 914 915 916
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
917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 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

  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
1031
  See Note [Orientation of equalities with fmvs] in TcFlatten
1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044
      [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!
-}
1045

1046
instance Outputable InertCans where
1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074
  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) $
        ptext (sLit "Equalities:")
          <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
      , ppUnless (isEmptyTcAppMap funeqs) $
        ptext (sLit "Type-function equalities =") <+> pprCts (funEqsToBag funeqs)
      , ppUnless (isEmptyTcAppMap dicts) $
        ptext (sLit "Dictionaries =") <+> pprCts (dictsToBag dicts)
      , ppUnless (isEmptyTcAppMap safehask) $
        ptext (sLit "Safe Haskell unsafe overlap =") <+> pprCts (dictsToBag safehask)
      , ppUnless (isEmptyCts irreds) $
        ptext (sLit "Irreds =") <+> pprCts irreds
      , 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
*                                                                      *
************************************************************************
1075

1076 1077 1078
Note [Adding an inert canonical constraint the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
1079

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

1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098
    * 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).

    * We always (G/W/D) kick out constraints that can be rewritten
      (respecting flavours) by the new constraint.
        - This is done by kickOutRewritable;
          see Note [inert_eqs: the inert equalities].

        - We do not need to kick anything out from the model; we only
          add [D] constraints to the model (in effect) and they are
          fully rewritten by the model, so (K2b) holds

        - A Derived equality can kick out [D] constraints in inert_dicts,
          inert_irreds etc.  Nothing in inert_eqs because there are no
Jan Stolarek's avatar
Jan Stolarek committed
1099
          Derived constraints in inert_eqs (they are in the model)
1100 1101 1102 1103

  Then, when adding:

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

        2. (DShadow) Emit shadow-copies (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 1117 1118 1119 1120 1121 1122 1123 1124 1125
     * [Given/Wanted] a ~N ty
        1. Add it to inert_eqs
        2. If the model can rewrite (a~ty)
           then (GWShadow) emit [D] a~ty
           else (GWModel)  Use emitDerivedShadows just like (DShadow)
                           and add a~ty to the model
                           (Reason:[D] a~ty is inert wrt model, and (K2b) holds)

     * [Given/Wanted] a ~R ty: just add it to inert_eqs

1126 1127 1128 1129 1130 1131 1132

* 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:
    - 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]

Jan Stolarek's avatar
Jan Stolarek committed
1133 1134 1135 1136 1137 1138 1139 1140
Note [Emitting shadow constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * Given a new model element [D] a ~ ty, we want to emit shadow
   [D] constraints for any inert constraints 'c' that can be
   rewritten [D] a-> ty

 * And similarly given a new Given/Wanted 'c', we want to emit a
   shadow 'c' if the model can rewrite [D] c
1141

Jan Stolarek's avatar
Jan Stolarek committed
1142 1143
See modelCanRewrite.

1144
NB the use of rewritableTyVars. You might wonder whether, given the new
Jan Stolarek's avatar
Jan Stolarek committed
1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168
constraint [D] fmv ~ ty and the inert [W] F alpha ~ fmv, do we want to
emit a shadow constraint [D] F alpha ~ fmv?  No, we don't, because
it'll literally be a duplicate (since we do not rewrite the RHS of a
CFunEqCan) and hence immediately eliminated again.  Insetad we simply
want to *kick-out* the [W] F alpha ~ fmv, so that it is reconsidered
from a fudep point of view.  See Note [Kicking out CFunEqCan for
fundeps]

Note [Kicking out CFunEqCan for fundeps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider:
   New:    [D] fmv1 ~ fmv2
   Inert:  [W] F alpha ~ fmv1
           [W] F beta  ~ fmv2

The new (derived) equality certainly can't rewrite the inerts. But we
*must* kick out the first one, to get:

   New:   [W] F alpha ~ fmv1
   Inert: [W] F beta ~ fmv2
   Model: [D] fmv1 ~ fmv2

and now improvement will discover [D] alpha ~ beta. This is important;
eg in Trac #9587.
1169 1170 1171
-}

addInertEq :: Ct -> TcS ()
Jan Stolarek's avatar
Jan Stolarek committed
1172
-- This is a key function, because of the kick-out stuff
1173
-- Precondition: item /is/ canonical
1174
addInertEq ct@(CTyEqCan { cc_tyvar = tv })
1175 1176 1177 1178
  = do { traceTcS "addInertEq {" $
         text "Adding new inert equality:" <+> ppr ct
       ; ics <- getInertCans

1179
       ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics
1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197
       ; ics2 <- add_inert_eq ics1 ct

       ; setInertCans ics2

       ; unless (isEmptyWorkList kicked_out) $
         do { updWorkListTcS (appendWorkList kicked_out)
            ; csTraceTcS $
               hang (ptext (sLit "Kick out, tv =") <+> ppr tv)
                  2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
                          , ppr kicked_out ]) }

       ; traceTcS "addInertEq }" $ empty }
addInertEq ct = pprPanic "addInertEq" (ppr ct)

add_inert_eq :: InertCans -> Ct -> TcS InertCans
add_inert_eq ics@(IC { inert_count = n
                     , inert_eqs = old_eqs
                     , inert_model = old_model })
1198 1199
             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv
                          , cc_rhs = rhs })
1200 1201 1202 1203 1204 1205 1206
  | isDerived ev
  = do { emitDerivedShadows ics tv
       ; return (ics { inert_model = extendVarEnv old_model tv ct }) }

  | ReprEq <- eq_rel
  = return new_ics

Jan Stolarek's avatar
Jan Stolarek committed
1207 1208
  -- Nominal equality (tv ~N ty), Given/Wanted
  -- See Note [Emitting shadow constraints]
1209 1210
  | modelCanRewrite old_model rw_tvs   -- Shadow of new ct isn't inert; emit it
  = do { emitNewDerivedEq loc (eqRelRole eq_rel) (mkTyVarTy tv) rhs
1211 1212 1213 1214 1215 1216 1217
       ; return new_ics }

  | otherwise   -- Shadow of new constraint is inert wrt model
                -- so extend model, and create shadows it can now rewrite
  = do { emitDerivedShadows ics tv
       ; return (new_ics { inert_model = new_model }) }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1218
  where