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

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

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

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

21
    runTcPluginTcS, addUsedDataCons, deferTcSForAllEq,
22

23 24
    -- Tracing etc
    panicTcS, traceTcS,
25
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
26
    wrapErrTcS, wrapWarnTcS,
27

28
    -- Evidence creation and transformation
29
    MaybeNew(..), freshGoals, isFresh, getEvTerm,
30

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

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

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

    -- The Model
    InertModel, kickOutAfterUnification,
62

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

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

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

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

77 78 79
    -- Irreds
    foldIrreds,

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

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

87
    instDFunType,                              -- Instantiation
88 89

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

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

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

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

#include "HsVersions.h"

import HscTypes

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

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

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

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

150
import Unique
151
import UniqFM
152
import UniqDFM
153
import Maybes
154

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

165 166 167
#ifdef DEBUG
import Digraph
#endif
168

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

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

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

191 192 193 194 195 196
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.

197
-}
198

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

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

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

229
extendWorkListEq :: Ct -> WorkList -> WorkList
230 231 232 233
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }

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

235
extendWorkListFunEq :: Ct -> WorkList -> WorkList
236
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
237

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

252
extendWorkListImplic :: Implication -> WorkList -> WorkList
253
extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
254

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

     _ -> extendWorkListNonEq ct wl
267

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

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

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

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

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

312 313 314
       ; try (selectWorkItem wl) $

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

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

339 340

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

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

352
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
353 354 355 356 357 358 359 360 361 362
              -- 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)
363

364 365
              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

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

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

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

389

390 391
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547
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
548
-}
549

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

data InertCans   -- See Note [Detailed InertCans Invariants] for more
  = IC { inert_model :: InertModel
559
              -- See Note [inert_model: the inert model]
560

561
       , inert_eqs :: DTyVarEnv EqualCtList
562
              -- See Note [inert_eqs: the inert equalities]
563
              -- All Given/Wanted CTyEqCans; index is the LHS tyvar
564

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

       , inert_dicts :: DictMap Ct
575
              -- Dictionaries only
576 577
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs/inert_model
578

579 580 581 582 583 584 585 586 587
       , 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

588
       , inert_irreds :: Cts
589 590
              -- Irreducible predicates

591
       , inert_insols :: Cts
592
              -- Frozen errors (as non-canonicals)
593 594 595 596 597 598

       , 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
599
       }
600

601
type InertModel  = DTyVarEnv Ct
602 603 604 605
     -- 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
606

607

608 609 610
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
611

612
  * All canonical
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
  * 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”
653

654 655 656 657
   * 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.

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

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

664
     - Derived constraints arising from functional dependencies, or
665 666
       decomposing injective arguments of type functions, and
       suchlike.
667

668 669
     - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
       inert_eqs.
670

671 672 673 674
   * The model is not subject to "kicking-out". Reason: we make a Derived
     shadow copy of any Given/Wanted (a ~ ty), and that Derived copy will
     be fully rewritten by the model before it is added

675 676 677 678 679
   * The principal reason for maintaining the model is to generate
     equalities that tell us how to unify a variable: that is, what
     Mark Jones calls "improvement". The same idea is sometimes also
     called "saturation"; find all the equalities that must hold in
     any solution.
680

681
   * Domain of the model = skolems + untouchables.
niteria's avatar
niteria committed
682
     A touchable unification variable would have been unified first.
683 684 685 686

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

687
   * However inert_dicts, inert_funeqs, inert_irreds
niteria's avatar
niteria committed
688
     may well contain derived constraints.
689 690 691 692 693 694 695 696

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
697 698
  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
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
       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
725
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
726 727 728 729 730 731 732 733 734 735 736

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

740 741 742 743 744 745 746 747 748
----------------------------------------------------------------
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
749 750
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
751 752
Theorem [Stability under extension]
   This is the main theorem!
753 754 755 756 757 758 759 760 761
   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
762 763 764
           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
765 766 767 768 769 770 771

      (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
772 773
      (K3) See Note [K3: completeness of solving]
           If (b -fs-> s) is in S with (fw >= fs), then
774 775 776 777 778 779 780 781
        (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
782 783 784
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable

785 786 787 788 789
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
790 791
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).
792 793 794 795 796 797 798 799 800 801 802

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

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

814 815 816 817 818 819 820
* 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
821
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
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
  - (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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
854 855 856
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~
932 933
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
934 935 936
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}.
937 938 939 940
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
941 942 943 944 945 946 947 948 949

  inert set: a -G/R-> Int
             b -G/R-> Bool

  type role T nominal representational

and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
T Int Bool. The reason is that T's first parameter has a nominal role, and
thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
Gabor Greif's avatar
Gabor Greif committed
950
substitution means that the proof in Note [The inert equalities] may need
951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054
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
1055
  See Note [Orientation of equalities with fmvs] in TcFlatten
1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068
      [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!
-}
1069

1070
instance Outputable InertCans where
1071 1072 1073 1074 1075
  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
1076
      [ ppUnless (isEmptyDVarEnv eqs) $
1077
        text "Equalities:"
1078
          <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
1079
      , ppUnless (isEmptyTcAppMap funeqs) $
1080
        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
1081
      , ppUnless (isEmptyTcAppMap dicts) $
1082
        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
1083
      , ppUnless (isEmptyTcAppMap safehask) $
1084
        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1085
      , ppUnless (isEmptyCts irreds) $
1086
        text "Irreds =" <+> pprCts irreds
1087 1088
      , ppUnless (isEmptyCts insols) $
        text "Insolubles =" <+> pprCts insols
1089 1090
      , ppUnless (isEmptyDVarEnv model) $
        text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model)
1091 1092 1093 1094 1095 1096 1097 1098
      , text "Unsolved goals =" <+> int count
      ]

{- *********************************************************************
*                                                                      *
                  Adding an inert
*                                                                      *
************************************************************************
1099

1100 1101 1102
Note [Adding an inert canonical constraint the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
1103

Jan Stolarek's avatar
Jan Stolarek committed