TcSMonad.hs 106 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 9 10 11
    extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
    extendWorkListCts, appendWorkList,
    selectNextWorkItem,
    workListSize, workListWantedCount,
12
    updWorkListTcS,
13

14 15 16
    -- The TcS monad
    TcS, runTcS, runTcSWithEvBinds,
    failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
17

18
    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
19

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

25
    -- Evidence creation and transformation
26
    Freshness(..), freshGoals, isFresh,
27

Austin Seipp's avatar
Austin Seipp committed
28
    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
29
    unifyTyVar, unflattenFmv, reportUnifications,
30
    setEvBind, setWantedEvBind, setEvBindIfWanted,
31
    newEvVar, newGivenEvVar, newGivenEvVars,
32 33
    emitNewDerived, emitNewDeriveds, emitNewDerivedEq,
    checkReductionDepth,
34

35
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
36
    getTopEnv, getGblEnv, getLclEnv, getTcEvBinds, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
37
    getTcEvBindsMap,
38
    tcLookupClass,
39

40
    -- Inerts
41
    InertSet(..), InertCans(..),
42
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
43 44
    getNoGivenEqs, setInertCans,
    getInertEqs, getInertCans, getInertModel, getInertGivens,
45
    emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
46
    matchableGivens, prohibitedSuperClassSolve,
47
    getUnsolvedInerts,
48
    removeInertCts,
49
    addInertCan, addInertEq, insertFunEq,
50
    emitInsoluble, emitWorkNC, emitWorkCt,
51 52 53

    -- The Model
    InertModel, kickOutAfterUnification,
54

55 56 57 58
    -- Inert Safe Haskell safe-overlap failures
    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
    getSafeOverlapFailures,

59
    -- Inert CDictCans
60 61
    lookupInertDict, findDictsByClass, addDict, addDictsByClass,
    delDict, partitionDicts, foldDicts, filterDicts,
62

63
    -- Inert CTyEqCans
64
    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
65 66 67 68

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

69 70 71
    -- Irreds
    foldIrreds,

72 73 74 75
    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems

    -- Inert CFunEqCans
76 77
    updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs,
    findFunEqsByTyCon, findFunEqs, partitionFunEqs, foldFunEqs,
78

79
    instDFunType,                              -- Instantiation
80 81

    -- MetaTyVars
82
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
83
    cloneMetaTyVar, demoteUnfilledFmv,
84

85
    TcLevel, isTouchableMetaTyVarTcS,
86
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
87
    zonkTyVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkSimples, zonkWC,
88

89 90
    -- References
    newTcRef, readTcRef, updTcRef,
91

92 93
    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
Adam Gundry's avatar
Adam Gundry committed
94
    matchFam, matchFamTcM,
95
    checkWellStagedDFun,
96
    pprEq                                    -- Smaller utils, re-exported from TcM
97
                                             -- TODO (DV): these are only really used in the
98 99
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
100 101
                                             -- here
) where
102 103 104 105 106

#include "HsVersions.h"

import HscTypes

107
import qualified Inst as TcM
108 109
import InstEnv
import FamInst
110 111 112 113
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
114
import qualified TcEnv as TcM
115
       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass )
116
import Kind
117 118
import TcType
import DynFlags
119
import Type
120
import Unify
121

122
import TcEvidence
123 124
import Class
import TyCon
125
import TcErrors   ( solverDepthErrorTcS )
126

127
import Name
128 129
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
130
import Var
131
import VarEnv
132
import VarSet
133 134
import Outputable
import Bag
135
import UniqSupply
136
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
137
import Util
Ian Lynagh's avatar
Ian Lynagh committed
138
import TcRnTypes
139

140
import Unique
141
import UniqFM
142
import Maybes ( orElse, firstJusts )
143

144
import TrieMap
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
145
import Control.Arrow ( first )
146
import Control.Monad( ap, when, unless, MonadPlus(..) )
147
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
148
import Data.IORef
149
import Data.List ( foldl', partition )
150

151 152 153
#ifdef DEBUG
import Digraph
#endif
154

Austin Seipp's avatar
Austin Seipp committed
155 156 157 158 159 160 161 162 163
{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************
164

165 166
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
167 168 169
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.
170

171
As a simple form of priority queue, our worklist separates out
172 173 174 175
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
176

177 178 179 180 181 182
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.

183
-}
184

185
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
186
data WorkList
187
  = WL { wl_eqs     :: [Ct]
188
       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
189
       , wl_rest    :: [Ct]
190 191
       , wl_deriv   :: [CtEvidence]  -- Implicitly non-canonical
                                     -- See Note [Process derived items last]
192 193
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
194

Simon Peyton Jones's avatar
Simon Peyton Jones committed
195
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
196
appendWorkList
197 198 199 200
    (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 })
201 202 203
   = WL { wl_eqs     = eqs1     ++ eqs2
        , wl_funeqs  = funeqs1  ++ funeqs2
        , wl_rest    = rest1    ++ rest2
204
        , wl_deriv   = ders1    ++ ders2
205
        , wl_implics = implics1 `unionBags`   implics2 }
206

207
workListSize :: WorkList -> Int
208 209 210 211 212 213
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
214

215
extendWorkListEq :: Ct -> WorkList -> WorkList
216 217 218 219
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

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

221
extendWorkListFunEq :: Ct -> WorkList -> WorkList
222
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
223

224 225
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
226 227 228 229 230 231 232 233 234 235 236
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
237

238
extendWorkListImplic :: Implication -> WorkList -> WorkList
239
extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
240

241 242 243
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
244
 = case classifyPredType (ctPred ct) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
245
     EqPred NomEq ty1 _
246
       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
247
       , isTypeFamilyTyCon tc
248
       -> extendWorkListFunEq ct wl
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
249
     EqPred {}
250 251 252
       -> extendWorkListEq ct wl

     _ -> extendWorkListNonEq ct wl
253

Simon Peyton Jones's avatar
Simon Peyton Jones committed
254
extendWorkListCts :: [Ct] -> WorkList -> WorkList
255
-- Agnostic
Simon Peyton Jones's avatar
Simon Peyton Jones committed
256
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
257 258

isEmptyWorkList :: WorkList -> Bool
259
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
260 261
                    , wl_rest = rest, wl_deriv = ders, wl_implics = implics })
  = null eqs && null rest && null funeqs && isEmptyBag implics && null ders
262 263

emptyWorkList :: WorkList
264
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
                   , 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
293

294 295 296 297 298 299
       ; try (selectWorkItem wl) $

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

301 302
-- Pretty printing
instance Outputable WorkList where
303
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
304
          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
305
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
306
     vcat [ ppUnless (null eqs) $
307
            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
308 309
          , ppUnless (null feqs) $
            ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
310
          , ppUnless (null rest) $
311
            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
312 313
          , ppUnless (null ders) $
            ptext (sLit "Derived =") <+> vcat (map ppr ders)
314 315 316
          , ppUnless (isEmptyBag implics) $
            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
          ])
dimitris's avatar
dimitris committed
317

318 319

{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
320
*                                                                      *
321
                InertSet: the inert set
Austin Seipp's avatar
Austin Seipp committed
322 323
*                                                                      *
*                                                                      *
324
********************************************************************* -}
325

326 327 328 329
data InertSet
  = IS { inert_cans :: InertCans
              -- Canonical Given, Wanted, Derived (no Solved)
              -- Sometimes called "the inert set"
330

331 332 333 334 335 336 337 338 339 340 341
       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
              -- 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)
342

343 344 345 346 347
       , inert_solved_dicts   :: DictMap CtEvidence
              -- Of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }
348

349 350 351
instance Outputable InertSet where
  ppr is = vcat [ ppr $ inert_cans is
                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
352

353 354 355 356 357 358 359 360 361 362 363 364
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 }
       , inert_flat_cache    = emptyFunEqs
       , inert_solved_dicts  = emptyDictMap }
365

366

367 368
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
369 370 371 372 373 374 375 376 377 378 379 380 381 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
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
525
-}
526

527 528 529 530 531 532 533 534 535 536 537 538
{- *********************************************************************
*                                                                      *
                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
539

540
       , inert_funeqs :: FunEqMap Ct
541
              -- All CFunEqCans; index is the whole family head type.
542 543
              -- Hence (by CFunEqCan invariants),
              -- all Nominal, and all Given/Wanted (no Derived)
544 545

       , inert_dicts :: DictMap Ct
546
              -- Dictionaries only, index is the class
547
              -- NB: index is /not/ the whole type because FD reactions
548
              -- need to match the class but not necessarily the whole type.
549

550 551 552 553 554 555 556 557 558
       , 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

559
       , inert_irreds :: Cts
560 561
              -- Irreducible predicates

562
       , inert_insols :: Cts
563
              -- Frozen errors (as non-canonicals)
564 565 566 567 568 569

       , 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
570
       }
571

572 573 574 575 576
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
577

578

579 580 581
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
582

583
  * All canonical
584

585 586 587 588 589 590 591 592 593 594 595 596 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 673 674 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 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
  * 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

  R1.  >= is transitive
  R2.  If f1 >= f, and f2 >= f,
       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
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)

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)

  (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
        that is, each individual binding is "self-stable"

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

---------- The main theorem --------------
   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)

      (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

      (K3) If (b -fs-> s) is in S with (fw >= fs), then
        (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.

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.

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

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

* 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
766
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 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 828 829 830 831 832 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 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 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
  - (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

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

Completeness
~~~~~~~~~~~~~
K3: completeness.  (K3) is not necessary for the extended substitution
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~
The system described in Note [The inert equalities] discusses an abstract
set of flavours. In GHC, flavours have two components: the flavour proper,
taken from {Wanted, Derived, Given}; and the equality relation (often called
role), taken from {NomEq, ReprEq}. When substituting w.r.t. the inert set,
as described in Note [The inert equalities], we must be careful to respect
roles. For example, if we have

  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:
  See Note [Orientation of equalities with fmvs]
      [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!
-}
1011

1012
instance Outputable InertCans where
1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040
  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
*                                                                      *
************************************************************************
1041

1042 1043 1044
Note [Adding an inert canonical constraint the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
1045

1046 1047
    * If c can be rewritten by model, emit [D] c, as NonCanonical.
      See Note [Can be rewritten by model]
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 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106
    * 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
          Derived constraints in inert_eqs.

  Then, when adding:

     * [Given/Wanted] a ~N ty
        1. (GWShadow) If the model can rewrite (a~ty), then emit [D] a~ty
           (GWModel)  Otherwise just add a~ty to the model
                      (Reason: [D] a~ty is inert wrt model, and (K2b) holds)

        2. Add it to inert_eqs

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

     * [Derived] a ~N ty
        1. (DShadow) Emit shadow-copies (emitDerivedShadows):
             For every inert G/W constraint c, st
               (a) (a~ty) can rewrite c (see Note [Can be rewritten]), and
               (b) the model cannot rewrite c
             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

        2. Add (a~ty) to the model
           NB: 'a' cannot be in fv(ty), because the constraint is canonical.

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

Note [Can be rewritten]
~~~~~~~~~~~~~~~~~~~~~~~
What does it mean to say "Constraint c can be rewritten by the model".
See modelCanRewrite, rewritableTyVars.

Basically it means fvs(c) intersects dom(model).  But can the model
   [fmv -> ty]  rewrite  CFunEqCan   F Int ~ fmv ?
No: we just look at the LHS of a CFunEqCan.
-}

addInertEq :: Ct -> TcS ()
1107
-- Precondition: item /is/ canonical
1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149
addInertEq ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
  = do { traceTcS "addInertEq {" $
         text "Adding new inert equality:" <+> ppr ct
       ; ics <- getInertCans

       ; let (kicked_out, ics1) = kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
       ; 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 })
             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
  | isDerived ev
  = do { emitDerivedShadows ics tv
       ; return (ics { inert_model = extendVarEnv old_model tv ct }) }

  | ReprEq <- eq_rel
  = return new_ics

  -- Nominal equality, Given/Wanted
  | modelCanRewrite old_model rw_tvs  -- Shadow of new constraint is
  = do { emitNewDerivedEq loc pred    -- not inert, so emit it
       ; 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
1150
  where
1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199
    loc     = ctEvLoc ev
    pred    = ctEvPred ev
    rw_tvs  = tyVarsOfType pred
    new_ics = ics { inert_eqs   = addTyEq old_eqs tv ct
                  , inert_count = bumpUnsolvedCount ev n }
    new_model = extendVarEnv old_model tv derived_ct
    derived_ct = ct { cc_ev = CtDerived { ctev_loc = loc, ctev_pred = pred } }

add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)

emitDerivedShadows :: InertCans -> TcTyVar -> TcS ()
emitDerivedShadows IC { inert_eqs      = tv_eqs
                      , inert_dicts    = dicts
                      , inert_safehask = safehask
                      , inert_funeqs   = funeqs
                      , inert_irreds   = irreds
                      , inert_model    = model } new_tv
  = mapM_ emit_shadow shadows
  where
    emit_shadow ct = emitNewDerived loc pred
      where
        ev = ctEvidence ct
        pred = ctEvPred ev
        loc  = ctEvLoc  ev

    shadows = foldDicts  get_ct dicts    $
              foldDicts  get_ct safehask $
              foldFunEqs get_ct funeqs   $
              foldIrreds get_ct irreds   $
              foldTyEqs  get_ct tv_eqs []
      -- Ignore insolubles

    get_ct ct cts | want_shadow ct = ct:cts
                  | otherwise      = cts

    want_shadow ct
      =  not (isDerivedCt ct)               -- No need for a shadow of a Derived!
      && (new_tv `elemVarSet` rw_tvs)       -- New tv can rewrite ct
      && not (modelCanRewrite model rw_tvs) -- We have not alrady created a shadow
      where
        rw_tvs = rewritableTyVars ct

modelCanRewrite :: InertModel -> TcTyVarSet -> Bool
-- True if there is any intersection between dom(model) and pred
modelCanRewrite model tvs = foldVarSet ((||) . (`elemVarEnv` model)) False tvs

rewritableTyVars :: Ct -> TcTyVarSet
rewritableTyVars (CFunEqCan { cc_tyargs = tys }) = tyVarsOfTypes tys
rewritableTyVars ct                              = tyVarsOfType (ctPred ct)
1200

1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222
--------------
addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
addInertCan ct
  = do { traceTcS "insertInertCan {" $
         text "Trying to insert new inert item:" <+> ppr ct

       ; ics <- getInertCans
       ; let ics' = add_item ics ct
       ; setInertCans ics'

       -- Emit shadow derived if necessary
       ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs)
              (emitNewDerived (ctEvLoc ev) pred)

       ; traceTcS "addInertCan }" $ empty }
  where
    rw_tvs = rewritableTyVars ct
    ev     = ctEvidence ct
    pred   = ctEvPred ev

add_item :: InertCans -> Ct -> InertCans
add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
1223
  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
1224

1225 1226 1227
add_item ics item@(CIrredEvCan { cc_ev = ev })
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
        , inert_count = bumpUnsolvedCount ev (inert_count ics) }
1228 1229 1230 1231 1232
       -- The 'False' is because the irreducible constraint might later instantiate
       -- to an equality.
       -- But since we try to simplify first, if there's a constraint function FC with
       --    type instance FC Int = Show
       -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
1233

1234 1235 1236
add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
  = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
        , inert_count = bumpUnsolvedCount ev (inert_count ics) }
1237

1238
add_item _ item
1239
  = pprPanic "upd_inert set: can't happen! Inserting " $
1240 1241
    ppr item   -- CTyEqCan is dealt with by addInertEq
               -- Can't be CNonCanonical, CHoleCan,
1242 1243
               -- because they only land in inert_insols

1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418