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

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

6
       -- Canonical constraints, definition is now in TcRnTypes
7

8
    WorkList(..), isEmptyWorkList, emptyWorkList,
9
    extendWorkListFunEq,
10
    extendWorkListNonEq, extendWorkListCt,
11 12
    extendWorkListCts, appendWorkList, selectWorkItem,
    workListSize,
13

Adam Gundry's avatar
Adam Gundry committed
14
    updWorkListTcS, updWorkListTcS_return,
15

Adam Gundry's avatar
Adam Gundry committed
16
    updInertTcS, updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
17 18

    Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
19
    emitInsoluble, emitWorkNC,
20

21 22
    isWanted, isDerived,
    isGivenCt, isWantedCt, isDerivedCt,
23

24
    mkGivenLoc,
25

26
    TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
27
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
28
    tryTcS, nestTcS, nestImplicTcS, recoverTcS,
29
    wrapErrTcS, wrapWarnTcS,
Adam Gundry's avatar
Adam Gundry committed
30
    runTcPluginTcS,
31

dimitris's avatar
dimitris committed
32
    -- Getting and setting the flattening cache
Austin Seipp's avatar
Austin Seipp committed
33
    addSolvedDict,
34 35 36

    -- Marking stuff as used
    addUsedRdrNamesTcS,
37 38 39

    deferTcSForAllEq,

dimitris's avatar
dimitris committed
40 41
    setEvBind,
    XEvTerm(..),
42
    Freshness(..), freshGoals, isFresh,
43 44

    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
45

46 47
    xCtEvidence,        -- Transform a CtEvidence during a step
    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
48 49 50
    rewriteEqEvidence,  -- Yet more specialised, for equality coercions
    maybeSym,

Austin Seipp's avatar
Austin Seipp committed
51 52
    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
    newEvVar, newGivenEvVar,
53
    emitNewDerived, emitNewDerivedEq,
54
    instDFunConstraints,
55

56
       -- Creation of evidence variables
57
    setWantedTyBind, reportUnifications,
58

59
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
60
    getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
Austin Seipp's avatar
Austin Seipp committed
61
    getTcEvBindsMap,
62

63
    lookupFlatCache, newFlattenSkolem,            -- Flatten skolems
64

Simon Peyton Jones's avatar
Simon Peyton Jones committed
65 66 67
        -- Deque
    Deque(..), insertDeque, emptyDeque,

68 69
        -- Inerts
    InertSet(..), InertCans(..),
70
    getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
Austin Seipp's avatar
Austin Seipp committed
71
    emptyInert, getTcSInerts, setTcSInerts,
72
    getUnsolvedInerts, checkAllSolved,
Adam Gundry's avatar
Adam Gundry committed
73
    splitInertCans, removeInertCts,
74
    prepareInertsForImplications,
75
    addInertCan, insertInertItemTcS, insertFunEq,
76 77
    EqualCtList,
    lookupSolvedDict, extendFlatCache,
78

79
    lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
80

Adam Gundry's avatar
Adam Gundry committed
81
    findFunEq, findTyEqs,
82 83
    findFunEqsByTyCon, findFunEqs, partitionFunEqs,
    sizeFunEqMap,
84

85
    instDFunType,                              -- Instantiation
86
    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
87
    cloneMetaTyVar, demoteUnfilledFmv,
88

89
    TcLevel, isTouchableMetaTyVarTcS,
90 91
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
92

93
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
94

95
    matchFam,
96
    checkWellStagedDFun,
97
    pprEq                                    -- Smaller utils, re-exported from TcM
98
                                             -- TODO (DV): these are only really used in the
99 100
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
101 102
                                             -- here
) where
103 104 105 106 107 108

#include "HsVersions.h"

import HscTypes

import Inst
109 110
import InstEnv
import FamInst
111 112 113 114
import FamInstEnv

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

123
import TcEvidence
124 125
import Class
import TyCon
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

137
import FastString
Ian Lynagh's avatar
Ian Lynagh committed
138
import Util
139
import Id
Ian Lynagh's avatar
Ian Lynagh committed
140
import TcRnTypes
141

142
import BasicTypes
143
import Unique
144
import UniqFM
145
import Maybes ( orElse, firstJusts )
146

147
import TrieMap
148 149
import Control.Monad( ap, when, unless )
import MonadUtils
Ian Lynagh's avatar
Ian Lynagh committed
150
import Data.IORef
Adam Gundry's avatar
Adam Gundry committed
151
import Data.List ( partition, foldl' )
152
import Pair
153

154 155 156
#ifdef DEBUG
import Digraph
#endif
157

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

168 169
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
170 171 172
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.
173

174
As a simple form of priority queue, our worklist separates out
175 176 177 178
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.
Austin Seipp's avatar
Austin Seipp committed
179
-}
180

Simon Peyton Jones's avatar
Simon Peyton Jones committed
181 182 183 184
data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
                            -- First to remove is at head of LH field

instance Outputable a => Outputable (Deque a) where
185 186 187 188
  ppr q = ppr (dequeList q)

dequeList :: Deque a -> [a]
dequeList (DQ as bs) = as ++ reverse bs  -- First one to come out at the start
Simon Peyton Jones's avatar
Simon Peyton Jones committed
189 190 191 192 193 194 195

emptyDeque :: Deque a
emptyDeque = DQ [] []

isEmptyDeque :: Deque a -> Bool
isEmptyDeque (DQ as bs) = null as && null bs

196 197 198
dequeSize :: Deque a -> Int
dequeSize (DQ as bs) = length as + length bs

Simon Peyton Jones's avatar
Simon Peyton Jones committed
199 200 201 202 203 204 205 206 207 208 209 210
insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)

appendDeque :: Deque a -> Deque a -> Deque a
appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2

extractDeque :: Deque a -> Maybe (Deque a, a)
extractDeque (DQ [] [])     = Nothing
extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
extractDeque (DQ [] bs)     = case reverse bs of
                                (a:as) -> Just (DQ as [], a)
                                [] -> panic "extractDeque"
211

212
-- See Note [WorkList priorities]
Austin Seipp's avatar
Austin Seipp committed
213
data WorkList
214 215 216 217 218
  = WL { wl_eqs     :: [Ct]
       , wl_funeqs  :: Deque Ct
       , wl_rest    :: [Ct]
       , wl_implics :: Bag Implication  -- See Note [Residual implications]
    }
batterseapower's avatar
batterseapower committed
219

Simon Peyton Jones's avatar
Simon Peyton Jones committed
220
appendWorkList :: WorkList -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
221
appendWorkList
222 223 224 225 226 227
    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
   = WL { wl_eqs     = eqs1     ++            eqs2
        , wl_funeqs  = funeqs1  `appendDeque` funeqs2
        , wl_rest    = rest1    ++            rest2
        , wl_implics = implics1 `unionBags`   implics2 }
228

229

230
workListSize :: WorkList -> Int
231
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
232 233
  = length eqs + dequeSize funeqs + length rest

234
extendWorkListEq :: Ct -> WorkList -> WorkList
Austin Seipp's avatar
Austin Seipp committed
235
extendWorkListEq ct wl
dimitris's avatar
dimitris committed
236
  = wl { wl_eqs = ct : wl_eqs wl }
237

238
extendWorkListFunEq :: Ct -> WorkList -> WorkList
239
extendWorkListFunEq ct wl
240 241
  = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }

242 243
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
244
extendWorkListNonEq ct wl
245
  = wl { wl_rest = ct : wl_rest wl }
246

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

251 252 253
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
254 255 256
 = case classifyPredType (ctPred ct) of
     EqPred ty1 _
       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
257
       , isTypeFamilyTyCon tc
258 259 260 261 262
       -> extendWorkListFunEq ct wl
       | otherwise
       -> extendWorkListEq ct wl

     _ -> extendWorkListNonEq ct wl
263

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

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

emptyWorkList :: WorkList
274 275
emptyWorkList = WL { wl_eqs  = [], wl_rest = []
                   , wl_funeqs = emptyDeque, wl_implics = emptyBag }
dimitris's avatar
dimitris committed
276 277

selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
278
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
dimitris's avatar
dimitris committed
279 280
  = case (eqs,feqs,rest) of
      (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
281 282
      (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
                       -> (Just ct, wl { wl_funeqs = fun_eqs' })
dimitris's avatar
dimitris committed
283 284 285
      (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
      (_,_,_)          -> (Nothing,wl)

286 287
-- Pretty printing
instance Outputable WorkList where
288 289 290
  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
          , wl_rest = rest, wl_implics = implics })
   = text "WL" <+> (braces $
Austin Seipp's avatar
Austin Seipp committed
291
     vcat [ ppUnless (null eqs) $
292 293 294 295
            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
          , ppUnless (isEmptyDeque feqs) $
            ptext (sLit "Funeqs =") <+> vcat (map ppr (dequeList feqs))
          , ppUnless (null rest) $
296
            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
297 298 299
          , ppUnless (isEmptyBag implics) $
            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
          ])
dimitris's avatar
dimitris committed
300

Austin Seipp's avatar
Austin Seipp committed
301 302 303 304 305 306 307
{-
************************************************************************
*                                                                      *
*                            Inert Sets                                *
*                                                                      *
*                                                                      *
************************************************************************
dimitris's avatar
dimitris committed
308 309 310 311

Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
312

313
  * All canonical
314

315 316 317 318 319 320 321 322 323 324 325 326 327 328
  * 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)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
329 330
  * CTyEqCan equalities: see Note [Applying the inert substitution]
                         in TcFlatten
331

332 333
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
334
Type-family equations, of form (ev : F tys ~ ty), live in three places
335 336 337 338 339 340 341

  * 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
342
        list.  Now if we flatten w2 before we get to w3, we still want to
343 344 345
        share that (G a).

    Because it contains work-list things, DO NOT use the flat cache to solve
346 347
    a top-level goal.  Eg in the above example we don't want to solve w3
    using w3 itself!
348

349
  * The inert_funeqs are un-solved but fully processed and in the InertCans.
Austin Seipp's avatar
Austin Seipp committed
350
-}
351 352 353

-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
354
data InertCans
355 356
  = IC { inert_eqs :: TyVarEnv EqualCtList
              -- All CTyEqCans; index is the LHS tyvar
357

358
       , inert_funeqs :: FunEqMap Ct
359 360 361
              -- All CFunEqCans; index is the whole family head type.

       , inert_dicts :: DictMap Ct
362
              -- Dictionaries only, index is the class
363
              -- NB: index is /not/ the whole type because FD reactions
364
              -- need to match the class but not necessarily the whole type.
365

366
       , inert_irreds :: Cts
367 368
              -- Irreducible predicates

369
       , inert_insols :: Cts
370 371
              -- Frozen errors (as non-canonicals)
       }
372

373 374 375 376 377 378 379 380 381 382 383
type EqualCtList = [Ct]
-- EqualCtList invariants:
--    * All are equalities
--    * All these equalities have the same LHS
--    * The list is never empty
--    * No element of the list can rewrite any other
--
-- From the fourth invariant it follows that the list is
--   - A single Given, or
--   - Multiple Wanteds, or
--   - Multiple Deriveds
384

dimitris's avatar
dimitris committed
385 386 387
-- The Inert Set
data InertSet
  = IS { inert_cans :: InertCans
388
              -- Canonical Given, Wanted, Derived (no Solved)
389
              -- Sometimes called "the inert set"
390

391
       , inert_flat_cache :: FunEqMap (TcCoercion, TcTyVar)
392
              -- See Note [Type family equations]
Austin Seipp's avatar
Austin Seipp committed
393
              -- If    F tys :-> (co, fsk),
394
              -- then  co :: F tys ~ fsk
395 396 397 398 399
              -- 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.
400
              -- Not necessarily inert wrt top-level equations (or inert_cans)
401

402
       , inert_solved_dicts   :: DictMap CtEvidence
403
              -- Of form ev :: C t1 .. tn
404
              -- Always the result of using a top-level instance declaration
405
              -- See Note [Solved constraints]
406 407 408 409
              -- - Used to avoid creating a new EvVar when we have a new goal
              --   that we have solved in the past
              -- - Stored not necessarily as fully rewritten
              --   (ToDo: rewrite lazily when we lookup)
dimitris's avatar
dimitris committed
410
       }
411

412 413
instance Outputable InertCans where
  ppr ics = vcat [ ptext (sLit "Equalities:")
414 415
                   <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
                                          emptyCts (inert_eqs ics))
416
                 , ptext (sLit "Type-function equalities:")
417
                   <+> pprCts (funEqsToBag (inert_funeqs ics))
418
                 , ptext (sLit "Dictionaries:")
419
                   <+> pprCts (dictsToBag (inert_dicts ics))
420
                 , ptext (sLit "Irreds:")
421
                   <+> pprCts (inert_irreds ics)
422 423
                 , text "Insolubles =" <+> -- Clearly print frozen errors
                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
dimitris's avatar
dimitris committed
424
                 ]
425 426

instance Outputable InertSet where
dimitris's avatar
dimitris committed
427
  ppr is = vcat [ ppr $ inert_cans is
428
                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
429

dimitris's avatar
dimitris committed
430 431
emptyInert :: InertSet
emptyInert
432 433 434 435 436 437 438 439
  = IS { inert_cans = IC { inert_eqs     = emptyVarEnv
                         , inert_dicts   = emptyDicts
                         , inert_funeqs  = emptyFunEqs
                         , inert_irreds  = emptyCts
                         , inert_insols  = emptyCts
                         }
       , inert_flat_cache    = emptyFunEqs
       , inert_solved_dicts  = emptyDictMap }
440

441 442 443
---------------
addInertCan :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
444
addInertCan ics item@(CTyEqCan {})
445 446
  = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
                              (inert_eqs ics)
447
                              (cc_tyvar item) [item] }
448

449 450
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
451 452

addInertCan ics item@(CIrredEvCan {})
453
  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
454 455 456 457 458
       -- 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
459 460 461

addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
  = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
462

463 464 465 466 467 468
addInertCan _ item
  = pprPanic "upd_inert set: can't happen! Inserting " $
    ppr item   -- Can't be CNonCanonical, CHoleCan,
               -- because they only land in inert_insols

--------------
469
insertInertItemTcS :: Ct -> TcS ()
470
-- Add a new item in the inerts of the monad
471
insertInertItemTcS item
472
  = do { traceTcS "insertInertItemTcS {" $
473 474
         text "Trying to insert new inert item:" <+> ppr item

475
       ; updInertCans (\ics -> addInertCan ics item)
476

477
       ; traceTcS "insertInertItemTcS }" $ empty }
478

479
addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
480
-- Add a new item in the solved set of the monad
481
addSolvedDict item cls tys
482
  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
483
  = return ()
484
  | otherwise
485
  = do { traceTcS "updSolvedSetTcs:" $ ppr item
486 487
       ; updInertTcS $ \ ics ->
             ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
488

489
updInertTcS :: (InertSet -> InertSet) -> TcS ()
490
-- Modify the inert set with the supplied function
491
updInertTcS upd_fn
492
  = do { is_var <- getTcSInertsRef
493
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
494
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
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
getInertCans :: TcS InertCans
getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }

setInertCans :: InertCans -> TcS ()
setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }

updInertCans :: (InertCans -> InertCans) -> TcS ()
-- Modify the inert set with the supplied function
updInertCans upd_fn
  = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }

updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertDicts upd_fn
  = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }

updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertFunEqs upd_fn
  = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }

updInertIrreds :: (Cts -> Cts) -> TcS ()
-- Modify the inert set with the supplied function
updInertIrreds upd_fn
  = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }


prepareInertsForImplications :: InertSet -> (InertSet)
524
-- See Note [Preparing inert set for implications]
525 526 527
prepareInertsForImplications is@(IS { inert_cans = cans })
  = is { inert_cans       = getGivens cans
       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
528
  where
529
    getGivens (IC { inert_eqs    = eqs
530
                  , inert_irreds = irreds
531
                  , inert_funeqs = funeqs
532
                  , inert_dicts  = dicts })
533 534
      = IC { inert_eqs     = filterVarEnv  is_given_ecl eqs
           , inert_funeqs  = filterFunEqs  isGivenCt funeqs
535
           , inert_irreds  = Bag.filterBag isGivenCt irreds
536 537
           , inert_dicts   = filterDicts   isGivenCt dicts
           , inert_insols  = emptyCts }
538

539 540 541
    is_given_ecl :: EqualCtList -> Bool
    is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
    is_given_ecl _                        = False
542

Austin Seipp's avatar
Austin Seipp committed
543
{-
544 545 546 547 548 549 550
Note [Do not inherit the flat cache]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do not want to inherit the flat cache when processing nested
implications.  Consider
   a ~ F b, forall c. b~Int => blah
If we have F b ~ fsk in the flat-cache, and we push that into the
nested implication, we might miss that F b can be rewritten to F Int,
Austin Seipp's avatar
Austin Seipp committed
551 552
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
553 554
do that flattening recursively.

555 556 557
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we trim the inert set,
558
retaining only Givens.  These givens can be used when solving
559
the inner implications.
dimitris's avatar
dimitris committed
560

561 562
There might be cases where interactions between wanteds at different levels
could help to solve a constraint. For example
563

564 565
        class C a b | a -> b
        (C Int alpha), (forall d. C d blah => C Int a)
566

567
If we pushed the (C Int alpha) inwards, as a given, it can produce a
568 569 570
fundep (alpha~a) and this can float out again and be used to fix
alpha.  (In general we can't float class constraints out just in case
(C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
571

572 573
For Derived constraints we don't have evidence, so we do not turn
them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
Austin Seipp's avatar
Austin Seipp committed
574
-}
575

576
getInertEqs :: TcS (TyVarEnv EqualCtList)
577
getInertEqs = do { inert <- getTcSInerts
578
                 ; return (inert_eqs (inert_cans inert)) }
579

580 581
getUnsolvedInerts :: TcS ( Bag Implication
                         , Cts     -- Tyvar eqs: a ~ ty
582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
                         , Cts     -- Fun eqs:   F a ~ ty
                         , Cts     -- Insoluble
                         , Cts )   -- All others
getUnsolvedInerts
 = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs
           , inert_irreds = irreds, inert_dicts = idicts
           , inert_insols = insols } <- getInertCans

      ; let unsolved_tv_eqs  = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts)
                                          emptyCts tv_eqs
            unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
            unsolved_irreds  = Bag.filterBag is_unsolved irreds
            unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
            others = unsolved_irreds `unionBags` unsolved_dicts

597 598 599
      ; implics <- getWorkListImplics

      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
600 601
              -- Keep even the given insolubles
              -- so that we can report dead GADT pattern match branches
602
  where
603
    add_if_unsolved :: Ct -> Cts -> Cts
604
    add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
605 606
                           | otherwise      = cts

607 608
    is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived

609
getNoGivenEqs :: TcLevel     -- TcLevel of this implication
610 611 612
               -> [TcTyVar]       -- Skolems of this implication
               -> TcS Bool        -- True <=> definitely no residual given equalities
-- See Note [When does an implication have given equalities?]
613
getNoGivenEqs tclvl skol_tvs
614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634
  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
             <- getInertCans
       ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet

             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence)  False iirreds
                          || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs

       ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
       ; return (not has_given_eqs) }
  where
    eqs_given_here :: VarSet -> EqualCtList -> Bool
    eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
                              -- Givens are always a sigleton
      = not (skolem_bound_here local_fsks tv) && ev_given_here ev
    eqs_given_here _ _ = False

    ev_given_here :: CtEvidence -> Bool
    -- True for a Given bound by the curent implication,
    -- i.e. the current level
    ev_given_here ev
      =  isGiven ev
635
      && tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
636 637 638 639 640 641 642 643 644 645 646 647 648

    add_fsk :: Ct -> VarSet -> VarSet
    add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
                    , isGiven ev = extendVarSet fsks tv
                    | otherwise  = fsks

    skol_tv_set = mkVarSet skol_tvs
    skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
      = case tcTyVarDetails tv of
          SkolemTv {} -> tv `elemVarSet` skol_tv_set
          FlatSkol {} -> not (tv `elemVarSet` local_fsks)
          _           -> False

Austin Seipp's avatar
Austin Seipp committed
649
{-
650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
   beta => alpha ~ Int
where beta is a unification variable that has already been unified
to () in an outer scope.  Then we can float the (alpha ~ Int) out
just fine. So when deciding whether the givens contain an equality,
we should canonicalise first, rather than just looking at the original
givens (Trac #8644).

So we simply look at the inert, canonical Givens and see if there are
any equalities among them, the calculation of has_given_eqs.  There
are some wrinkles:

 * We must know which ones are bound in *this* implication and which
665 666
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
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
   of the TcLclEnv stored in the Given (ev_given_here).

   What about interactions between inner and outer givens?
      - Outer given is rewritten by an inner given, then there must
        have been an inner given equality, hence the “given-eq” flag
        will be true anyway.

      - Inner given rewritten by outer, retains its level (ie. The inner one)

 * We must take account of *potential* equalities, like the one above:
      beta => ...blah...
   If we still don't know what beta is, we conservatively treat it as potentially
   becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.

 * When flattening givens, we generate Given equalities like
     <F [a]> : F [a] ~ f,
   with Refl evidence, and we *don't* want those to count as an equality
   in the givens!  After all, the entire flattening business is just an
   internal matter, and the evidence does not mention any of the 'givens'
   of this implication.  So we do not treat inert_funeqs as a 'given equality'.

 * See Note [Let-bound skolems] for another wrinkle

Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and  * 'a' is a skolem bound in this very implication, b

then:
a) The Given is pretty much a let-binding, like
      f :: (a ~ b->c) => a -> a
   Here the equality constraint is like saying
      let a = b->c in ...
   It is not adding any new, local equality  information,
   and hence can be ignored by has_given_eqs

b) 'a' will have been completely substituted out in the inert set,
   so we can safely discard it.  Notably, it doesn't need to be
   returned as part of 'fsks'

For an example, see Trac #9211.
Austin Seipp's avatar
Austin Seipp committed
708
-}
709

Adam Gundry's avatar
Adam Gundry committed
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
splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
-- ^ Extract the (given, derived, wanted) inert constraints
splitInertCans iCans = (given,derived,wanted)
  where
    allCts   = foldDicts  (:) (inert_dicts iCans)
             $ foldFunEqs (:) (inert_funeqs iCans)
             $ concat (varEnvElts (inert_eqs iCans))

    (derived,other) = partition isDerivedCt allCts
    (wanted,given)  = partition isWantedCt  other

removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
-- typechecker plugin wishes to discard a given.
removeInertCts cts icans = foldl' removeInertCt icans cts

removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
  case ct of

    CDictCan  { cc_class = cl, cc_tyargs = tys } ->
      is { inert_dicts = delDict (inert_dicts is) cl tys }

    CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
      is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }

    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
      is { inert_eqs = delTyEq (inert_eqs is) x ty }

    CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
    CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
    CHoleCan {}      -> panic "removeInertCt: CHoleCan"


744 745 746 747 748 749 750 751
checkAllSolved :: TcS Bool
-- True if there are no unsolved wanteds
-- Ignore Derived for this purpose, unless in insolubles
checkAllSolved
 = do { is <- getTcSInerts

      ; let icans = inert_cans is
            unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
752 753
            unsolved_dicts  = foldDicts ((||)  . isWantedCt) (inert_dicts icans)  False
            unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False
754
            unsolved_eqs    = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans)
755 756 757

      ; return (not (unsolved_eqs || unsolved_irreds
                     || unsolved_dicts || unsolved_funeqs
758
                     || not (isEmptyBag (inert_insols icans)))) }
759

760 761 762
lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcTyVar))
lookupFlatCache fam_tc tys
  = do { IS { inert_flat_cache = flat_cache
763
            , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
764 765
       ; return (firstJusts [lookup_inerts inert_funeqs,
                             lookup_flats flat_cache]) }
766
  where
767
    lookup_inerts inert_funeqs
768 769 770 771 772 773 774
      | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
           <- findFunEqs inert_funeqs fam_tc tys
      = Just (ctEvCoercion ctev, fsk)
      | otherwise = Nothing

    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys

775

776
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
777
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
778 779
lookupInInerts loc pty
  = do { inerts <- getTcSInerts
780 781
       ; return $ case (classifyPredType pty) of
           ClassPred cls tys
782 783 784 785
              | Just ev <- lookupSolvedDict inerts loc cls tys
              -> Just ev
              | otherwise
              -> lookupInertDict (inert_cans inerts) loc cls tys
786

787
           _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
788 789
      }

790 791 792 793 794 795 796 797 798
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
  = case findDict dicts cls tys of
      Just ct | let ev = ctEvidence ct
              , ctEvCheckDepth cls loc ev
              -> Just ev
      _       -> Nothing

lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
799
-- Returns just if exactly this predicate type exists in the solved.
800 801 802 803
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
  = case findDict solved cls tys of
      Just ev | ctEvCheckDepth cls loc ev -> Just ev
      _                                   -> Nothing
804

Austin Seipp's avatar
Austin Seipp committed
805 806 807
{-
************************************************************************
*                                                                      *
808
                   TyEqMap
Austin Seipp's avatar
Austin Seipp committed
809 810 811
*                                                                      *
************************************************************************
-}
812 813 814 815 816

type TyEqMap a = TyVarEnv a

findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
findTyEqs m tv = lookupVarEnv m tv `orElse` []
Adam Gundry's avatar
Adam Gundry committed
817 818 819 820 821

delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
        isThisOne _                          = False
822

Austin Seipp's avatar
Austin Seipp committed
823 824 825
{-
************************************************************************
*                                                                      *
826
                   TcAppMap, DictMap, FunEqMap
Austin Seipp's avatar
Austin Seipp committed
827 828 829
*                                                                      *
************************************************************************
-}
830

831 832 833
type TcAppMap a = UniqFM (ListMap TypeMap a)
    -- Indexed by tycon then the arg types
    -- Used for types and classes; hence UniqFM
834 835 836 837 838 839 840 841 842 843 844

emptyTcAppMap :: TcAppMap a
emptyTcAppMap = emptyUFM

findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
findTcApp m u tys = do { tys_map <- lookupUFM m u
                       ; lookupTM tys tys_map }

delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
delTcApp m cls tys = adjustUFM (deleteTM tys) m cls

845 846
insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
insertTcApp m cls tys ct = alterUFM alter_tm m cls
847 848 849
  where
    alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))

850 851 852 853 854 855 856 857 858 859 860