TcInteract.hs 78.4 KB
Newer Older
1 2
{-# LANGUAGE CPP #-}

3
module TcInteract (
4 5
     solveSimpleGivens,    -- Solves [EvVar],GivenLoc
     solveSimpleWanteds    -- Solves Cts
6
  ) where
7 8 9

#include "HsVersions.h"

10
import BasicTypes ()
11 12
import HsTypes ( hsIPNameFS )
import FastString
13
import TcCanonical
14
import TcFlatten
15 16
import VarSet
import Type
17
import Kind (isKind, isConstraintKind)
dimitris's avatar
dimitris committed
18
import Unify
19
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
20
import CoAxiom(sfInteractTop, sfInteractInert)
21 22 23

import Var
import TcType
24
import PrelNames ( knownNatClassName, knownSymbolClassName, ipClassNameKey,
25
                   callStackTyConKey, typeableClassName )
26
import Id( idType )
27 28
import Class
import TyCon
29
import FunDeps
30
import FamInst
31
import Inst( tyVarsOfCt )
32

33
import TcEvidence
34 35
import Outputable

36
import TcRnTypes
37
import TcErrors
38
import TcSMonad
39
import Bag
40

Adam Gundry's avatar
Adam Gundry committed
41
import Data.List( partition, foldl', deleteFirstsBy )
42
import SrcLoc
dimitris's avatar
dimitris committed
43 44
import VarEnv

45
import Control.Monad
46
import Maybes( isJust )
47
import Pair (Pair(..))
48
import Unique( hasKey )
49
import DynFlags
50
import Util
51

Austin Seipp's avatar
Austin Seipp committed
52
{-
53
**********************************************************************
54
*                                                                    *
55 56 57 58
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

59
Note [Basic Simplifier Plan]
60
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
61
1. Pick an element from the WorkList if there exists one with depth
62
   less than our context-stack depth.
63

64
2. Run it down the 'stage' pipeline. Stages are:
65 66 67 68
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level intreactions
69
   Each stage returns a StopOrContinue and may have sideffected
70
   the inerts or worklist.
71 72 73 74 75 76

   The threading of the stages is as follows:
      - If (Stop) is returned by a stage then we start again from Step 1.
      - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
        the next stage in the pipeline.
4. If the element has survived (i.e. ContinueWith x) the last stage
77 78
   then we add him in the inerts and jump back to Step 1.

79
If in Step 1 no such element exists, we have exceeded our context-stack
80
depth and will simply fail.
81

82
Note [Unflatten after solving the simple wanteds]
83
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
84
We unflatten after solving the wc_simples of an implication, and before attempting
85 86
to float. This means that

87
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
   need to worry about then across successive passes over the constraint tree.
   (E.g. we don't need the old ic_fsk field of an implication.

 * When floating an equality outwards, we don't need to worry about floating its
   associated flattening constraints.

 * Another tricky case becomes easy: Trac #4935
       type instance F True a b = a
       type instance F False a b = b

       [w] F c a b ~ gamma
       (c ~ True) => a ~ gamma
       (c ~ False) => b ~ gamma

   Obviously this is soluble with gamma := F c a b, and unflattening
103
   will do exactly that after solving the simple constraints and before
104 105 106 107 108 109 110 111 112
   attempting the implications.  Before, when we were not unflattening,
   we had to push Wanted funeqs in as new givens.  Yuk!

   Another example that becomes easy: indexed_types/should_fail/T7786
      [W] BuriedUnder sub k Empty ~ fsk
      [W] Intersect fsk inv ~ s
      [w] xxx[1] ~ s
      [W] forall[2] . (xxx[1] ~ Empty)
                   => Intersect (BuriedUnder sub k Empty) inv ~ Empty
113 114 115

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 117
There is an annoying mismatch between solveSimpleGivens and
solveSimpleWanteds, because the latter needs to fiddle with the inert
118 119 120 121 122 123 124
set, unflatten and and zonk the wanteds.  It passes the zonked wanteds
to runTcPluginsWanteds, which produces a replacement set of wanteds,
some additional insolubles and a flag indicating whether to go round
the loop again.  If so, prepareInertsForImplications is used to remove
the previous wanteds (which will still be in the inert set).  Note
that prepareInertsForImplications will discard the insolubles, so we
must keep track of them separately.
Austin Seipp's avatar
Austin Seipp committed
125
-}
126

127 128
solveSimpleGivens :: CtLoc -> [EvVar] -> TcS ()
solveSimpleGivens loc givens
129
  | null givens  -- Shortcut for common case
130
  = return ()
131
  | otherwise
Adam Gundry's avatar
Adam Gundry committed
132
  = go (map mk_given_ct givens)
133
  where
134
    mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
135 136
                                                , ctev_pred = evVarPred ev_id
                                                , ctev_loc  = loc })
137
    go givens = do { solveSimples (listToBag givens)
Adam Gundry's avatar
Adam Gundry committed
138 139 140
                   ; new_givens <- runTcPluginsGiven
                   ; when (notNull new_givens) (go new_givens)
                   }
141

142 143
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds = go emptyBag
144 145
  where
    go insols0 wanteds
146
      = do { solveSimples wanteds
147 148
           ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
           ; unflattened_eqs <- unflatten tv_eqs fun_eqs
149
              -- See Note [Unflatten after solving the simple wanteds]
150

151 152
           ; zonked <- zonkSimples (others `andCts` unflattened_eqs)
             -- Postcondition is that the wl_simples are zonked
153 154 155 156

           ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
              -- See Note [Running plugins on unflattened wanteds]
           ; let all_insols = insols0 `unionBags` insols `unionBags` insols'
157

158 159
           ; if rerun then do { updInertTcS prepareInertsForImplications
                              ; go all_insols wanteds' }
160 161 162
                      else return (WC { wc_simple = wanteds'
                                      , wc_insol  = all_insols
                                      , wc_impl   = implics }) }
Adam Gundry's avatar
Adam Gundry committed
163

164 165 166

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
167
solveSimples :: Cts -> TcS ()
168 169
-- Returns the final InertSet in TcS
-- Has no effect on work-list or residual-iplications
170 171
-- The constraints are initially examined in left-to-right order

172 173
solveSimples cts
  = {-# SCC "solveSimples" #-}
174 175
    do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
       ; solve_loop }
176
  where
177
    solve_loop
178
      = {-# SCC "solve_loop" #-}
179
        do { sel <- selectNextWorkItem
180
           ; case sel of
181 182
              NoWorkRemaining     -- Done, successfuly (modulo frozen)
                -> return ()
183 184
              MaxDepthExceeded ct -- Failure, depth exceeded
                -> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct)
185
              NextWorkItem ct     -- More work, loop around!
186 187
                -> do { runSolverPipeline thePipeline ct
                      ; solve_loop } }
188

Adam Gundry's avatar
Adam Gundry committed
189 190 191

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
192
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven = do
  (givens,_,_) <- fmap splitInertCans getInertCans
  if null givens
    then return []
    else do
      p <- runTcPlugins (givens,[],[])
      let (solved_givens, _, _) = pluginSolvedCts p
      updInertCans (removeInertCts solved_givens)
      mapM_ emitInsoluble (pluginBadCts p)
      return (pluginNewCts p)

-- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
-- them and produce an updated bag of wanteds (possibly with some new
-- work) and a bag of insolubles.  The boolean indicates whether
209
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
-- main solver.
runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool)
runTcPluginsWanted zonked_wanteds
  | isEmptyBag zonked_wanteds = return (zonked_wanteds, emptyBag, False)
  | otherwise                 = do
    (given,derived,_) <- fmap splitInertCans getInertCans
    p <- runTcPlugins (given, derived, bagToList zonked_wanteds)
    let (solved_givens, solved_deriveds, solved_wanteds) = pluginSolvedCts p
        (_, _, wanteds) = pluginInputCts p
    updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
    mapM_ setEv solved_wanteds
    return ( listToBag $ pluginNewCts p ++ wanteds
           , listToBag $ pluginBadCts p
           , notNull (pluginNewCts p) )
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
227
      CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
Adam Gundry's avatar
Adam Gundry committed
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 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 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
      _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"

-- | A triple of (given, derived, wanted) constraints to pass to plugins
type SplitCts  = ([Ct], [Ct], [Ct])

-- | A solved triple of constraints, with evidence for wanteds
type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])

-- | Represents collections of constraints generated by typechecker
-- plugins
data TcPluginProgress = TcPluginProgress
    { pluginInputCts  :: SplitCts
      -- ^ Original inputs to the plugins with solved/bad constraints
      -- removed, but otherwise unmodified
    , pluginSolvedCts :: SolvedCts
      -- ^ Constraints solved by plugins
    , pluginBadCts    :: [Ct]
      -- ^ Constraints reported as insoluble by plugins
    , pluginNewCts    :: [Ct]
      -- ^ New constraints emitted by plugins
    }

-- | Starting from a triple of (given, derived, wanted) constraints,
-- invoke each of the typechecker plugins in turn and return
--
--  * the remaining unmodified constraints,
--  * constraints that have been solved,
--  * constraints that are insoluble, and
--  * new work.
--
-- Note that new work generated by one plugin will not be seen by
-- other plugins on this pass (but the main constraint solver will be
-- re-invoked and they will see it later).  There is no check that new
-- work differs from the original constraints supplied to the plugin:
-- the plugin itself should perform this check if necessary.
runTcPlugins :: SplitCts -> TcS TcPluginProgress
runTcPlugins all_cts = do
    gblEnv <- getGblEnv
    foldM do_plugin initialProgress (tcg_tc_plugins gblEnv)
  where
    do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
    do_plugin p solver = do
        result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
        return $ progress p result

    progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
    progress p (TcPluginContradiction bad_cts) =
       p { pluginInputCts = discard bad_cts (pluginInputCts p)
         , pluginBadCts   = bad_cts ++ pluginBadCts p
         }
    progress p (TcPluginOk solved_cts new_cts) =
      p { pluginInputCts  = discard (map snd solved_cts) (pluginInputCts p)
        , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
        , pluginNewCts    = new_cts ++ pluginNewCts p
        }

    initialProgress = TcPluginProgress all_cts ([], [], []) [] []

    discard :: [Ct] -> SplitCts -> SplitCts
    discard cts (xs, ys, zs) =
        (xs `without` cts, ys `without` cts, zs `without` cts)

    without :: [Ct] -> [Ct] -> [Ct]
    without = deleteFirstsBy eqCt

    eqCt :: Ct -> Ct -> Bool
    eqCt c c' = case (ctEvidence c, ctEvidence c') of
      (CtGiven   pred _ _, CtGiven   pred' _ _) -> pred `eqType` pred'
      (CtWanted  pred _ _, CtWanted  pred' _ _) -> pred `eqType` pred'
      (CtDerived pred _  , CtDerived pred' _  ) -> pred `eqType` pred'
      (_                 , _                  ) -> False

    add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
    add xs scs = foldl' addOne scs xs

    addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
    addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
      CtGiven  {} -> (ct:givens, deriveds, wanteds)
      CtDerived{} -> (givens, ct:deriveds, wanteds)
      CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)


310
type WorkItem = Ct
311
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
312

313
data SelectWorkItem
314
       = NoWorkRemaining      -- No more work left (effectively we're done!)
315
       | MaxDepthExceeded Ct
316
                              -- More work left to do but this constraint has exceeded
317
                              -- the maximum depth and we must stop
318
       | NextWorkItem Ct      -- More work left, here's the next item to look at
319

320 321 322 323
selectNextWorkItem :: TcS SelectWorkItem
selectNextWorkItem
  = do { dflags <- getDynFlags
       ; updWorkListTcS_return (pick_next dflags) }
324
  where
325 326
    pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList)
    pick_next dflags wl
327
      = case selectWorkItem wl of
328
          (Nothing,_)
329
              -> (NoWorkRemaining,wl)           -- No more work
330
          (Just ct, new_wl)
331 332 333 334
              | subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct)) 
              -> (MaxDepthExceeded ct,new_wl)   -- Depth exceeded

              | otherwise
335
              -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
336

337 338 339
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
                  -> WorkItem                   -- The work item
                  -> TcS ()
340
-- Run this item down the pipeline, leaving behind new work and inerts
341 342 343 344
runSolverPipeline pipeline workItem
  = do { initial_is <- getTcSInerts
       ; traceTcS "Start solver pipeline {" $
                  vcat [ ptext (sLit "work item = ") <+> ppr workItem
345 346
                       , ptext (sLit "inerts    = ") <+> ppr initial_is]

347
       ; bumpStepCountTcS    -- One step for each constraint processed
348 349 350
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

       ; final_is <- getTcSInerts
351
       ; case final_res of
352 353 354
           Stop ev s       -> do { traceFireTcS ev s
                                 ; traceTcS "End solver pipeline (discharged) }"
                                       (ptext (sLit "inerts =") <+> ppr final_is)
355
                                 ; return () }
356
           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
357
                                 ; traceTcS "End solver pipeline (not discharged) }" $
358
                                       vcat [ ptext (sLit "final_item =") <+> ppr ct
359
                                            , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
360
                                            , ptext (sLit "inerts     =") <+> ppr final_is]
361
                                 ; insertInertItemTcS ct }
362
       }
Austin Seipp's avatar
Austin Seipp committed
363
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
364 365 366
                     -> TcS (StopOrContinue Ct)
        run_pipeline [] res        = return res
        run_pipeline _ (Stop ev s) = return (Stop ev s)
367 368
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
369 370
                          (text "workitem   = " <+> ppr ct)
               ; res <- stg ct
371
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
372
               ; run_pipeline stgs res }
373

Austin Seipp's avatar
Austin Seipp committed
374
{-
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396
Example 1:
  Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
  Reagent: a ~ [b] (given)

React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []

Example 2:
  Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
  Reagent: a ~w [b]

React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
etc.

Example 3:
  Inert:  {a ~ Int, F Int ~ b} (given)
  Reagent: F a ~ b (wanted)

React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
Austin Seipp's avatar
Austin Seipp committed
397
-}
398

399
thePipeline :: [(String,SimplifierStage)]
400
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
401 402
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
403

Austin Seipp's avatar
Austin Seipp committed
404
{-
405
*********************************************************************************
406
*                                                                               *
407 408 409 410
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

411 412 413 414 415
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

416
   If the work-item is Given,
417 418
   then the inert item must Given

419
But this isn't quite true.  Suppose we have,
420 421 422 423
    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
     c1: [G] beta ~ [alpha], c2 : [W] blah
Now, c3 does not interact with the the given c1, so when we spontaneously
424
solve c3, we must re-react it with the inert set.  So we can attempt a
425 426 427
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
428
   If the work-item is Given,
429 430 431
   AND there is a reaction
   then the inert item must Given
or, equivalently,
432
   If the work-item is Given,
433 434
   and the inert item is Wanted/Derived
   then there is no reaction
Austin Seipp's avatar
Austin Seipp committed
435
-}
436

437
-- Interaction result of  WorkItem <~> Ct
438

439
type StopNowFlag = Bool    -- True <=> stop after this interaction
440

441
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
442 443
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
444

445
interactWithInertsStage wi
446 447
  = do { inerts <- getTcSInerts
       ; let ics = inert_cans inerts
448
       ; case wi of
449 450 451 452
             CTyEqCan    {} -> interactTyVarEq ics wi
             CFunEqCan   {} -> interactFunEq   ics wi
             CIrredEvCan {} -> interactIrred   ics wi
             CDictCan    {} -> interactDict    ics wi
453
             _ -> pprPanic "interactWithInerts" (ppr wi) }
454 455
                -- CHoleCan are put straight into inert_frozen, so never get here
                -- CNonCanonical have been canonicalised
456

457 458 459 460 461
data InteractResult
   = IRKeep      -- Keep the existing inert constraint in the inert set
   | IRReplace   -- Replace the existing inert constraint with the work item
   | IRDelete    -- Delete the existing inert constraint from the inert set

462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482
instance Outputable InteractResult where
  ppr IRKeep    = ptext (sLit "keep")
  ppr IRReplace = ptext (sLit "replace")
  ppr IRDelete  = ptext (sLit "delete")

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
                     -> TcS (InteractResult, StopNowFlag)
-- Preconditions:
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
solveOneFromTheOther ev_i ev_w
  | isDerived ev_w
  = return (IRKeep, True)

  | isDerived ev_i -- The inert item is Derived, we can just throw it away,
                   -- The ev_w is inert wrt earlier inert-set items,
                   -- so it's safe to continue on from this point
  = return (IRDelete, False)

  | CtWanted { ctev_evar = ev_id } <- ev_w
483
  = do { setWantedEvBind ev_id (ctEvTerm ev_i)
484 485 486
       ; return (IRKeep, True) }

  | CtWanted { ctev_evar = ev_id } <- ev_i
487
  = do { setWantedEvBind ev_id (ctEvTerm ev_w)
488 489
       ; return (IRReplace, True) }

490 491 492 493 494 495 496
  -- So they are both Given
  -- See Note [Replacement vs keeping]
  | lvl_i == lvl_w
  = do { binds <- getTcEvBindsMap
       ; if has_binding binds ev_w && not (has_binding binds ev_i)
         then return (IRReplace, True)
         else return (IRKeep,    True) }
497

498 499 500 501 502 503 504 505
   | otherwise   -- Both are Given
   = return (if use_replacement then IRReplace else IRKeep, True)
   where
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
506

507
     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
508 509 510 511

     use_replacement
       | isIPPred pred = lvl_w > lvl_i
       | otherwise     = lvl_w < lvl_i
512

Austin Seipp's avatar
Austin Seipp committed
513
{-
514 515 516 517 518 519 520 521 522 523 524
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
we keep?

  * For implicit parameters we want to keep the innermost (deepest)
    one, so that it overrides the outer one.
    See Note [Shadowing of Implicit Parameters]

  * For everything else, we want to keep the outermost one.  Reason: that
    makes it more likely that the inner one will turn out to be unused,
525 526 527 528 529 530 531 532 533 534 535 536 537 538
    and can be reported as redundant.  See Note [Tracking redundant constraints]
    in TcSimplify.

    It transpires that using the outermost one is reponsible for an
    8% performance improvement in nofib cryptarithm2, compared to
    just rolling the dice.  I didn't investigate why.

  * If there is no "outermost" one, we keep the one that has a non-trivial
    evidence binding.  Note [Tracking redundant constraints] again.
    Example:  f :: (Eq a, Ord a) => blah
    then we may find [G] sc_sel (d1::Ord a) :: Eq a
                     [G] d2 :: Eq a
    We want to discard d2 in favour of the superclass selection from
    the Ord dictionary.
539

540 541
  * Finally, when there is still a choice, use IRKeep rather than
    IRReplace, to avoid unnecesary munging of the inert set.
542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562

Doing the depth-check for implicit parameters, rather than making the work item
always overrride, is important.  Consider

    data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }

    f :: (?x::a) => T a -> Int
    f T1 = ?x
    f T2 = 3

We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
two new givens in the work-list:  [G] (?x::Int)
                                  [G] (a ~ Int)
Now consider these steps
  - process a~Int, kicking out (?x::a)
  - process (?x::Int), the inner given, adding to inert set
  - process (?x::a), the outer given, overriding the inner given
Wrong!  The depth-check ensures that the inner implicit parameter wins.
(Actually I think that the order in which the work-list is processed means
that this chain of events won't happen, but that's very fragile.)

563 564 565 566 567
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
568
-}
569

570 571 572 573
-- Two pieces of irreducible evidence: if their types are *exactly identical*
-- we can rewrite them. We can never improve using this:
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
574
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
575 576 577

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
578
        (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
579 580 581 582 583
                                                 (inert_irreds inerts)
  , (ct_i : rest) <- bagToList matching_irreds
  , let ctev_i = ctEvidence ct_i
  = ASSERT( null rest )
    do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
584 585 586 587 588 589 590 591 592 593
       ; case inert_effect of
            IRKeep    -> return ()
            IRDelete  -> updInertIrreds (\_ -> others)
            IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
                         -- These const upd's assume that solveOneFromTheOther
                         -- has no side effects on InertCans
       ; if stop_now then
            return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
       ; else
            continueWith workItem }
594

595
  | otherwise
596
  = continueWith workItem
597

598
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
599

Austin Seipp's avatar
Austin Seipp committed
600
{-
601 602 603 604 605
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
606
-}
607

608
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
609
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
610 611 612 613 614 615 616
  -- don't ever try to solve CallStack IPs directly from other dicts,
  -- we always build new dicts instead.
  -- See Note [Overview of implicit CallStacks]
  | [_ip, ty] <- tys
  , isWanted ev_w
  , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
  = do let ev_cs =
617
             case lookupInertDict inerts cls tys of
618 619 620 621 622 623 624 625 626 627 628 629
               Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
               _ -> mkEvCs (EvCallStack EvCsEmpty)

       -- now we have ev_cs :: CallStack, but the evidence term should
       -- be a dictionary, so we have to coerce ev_cs to a
       -- dictionary for `IP ip CallStack`
       let ip_ty = mkClassPred cls tys
       let ev_tm = mkEvCast (EvCallStack ev_cs) (TcCoercion $ wrapIP ip_ty)
       addSolvedDict ev_w cls tys
       setWantedEvBind (ctEvId ev_w) ev_tm
       stopWith ev_w "Wanted CallStack IP"

630
  | Just ctev_i <- lookupInertDict inerts cls tys
631
  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
632 633 634 635 636 637
       ; case inert_effect of
           IRKeep    -> return ()
           IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
           IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
       ; if stop_now then
            return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
Austin Seipp's avatar
Austin Seipp committed
638
         else
639
            continueWith workItem }
640 641 642 643 644 645

  | cls `hasKey` ipClassNameKey
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
646 647 648 649 650 651 652
  = do { mapBagM_ (addFunDepWork workItem) 
                  (findDictsByClass (inert_dicts inerts) cls)
               -- Create derived fds and keep on going.
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
               -- Importantly we don't throw workitem back in the 
               -- worklist bebcause this can cause loops (see #5236)
653
       ; continueWith workItem  }
654 655 656

interactDict _ wi = pprPanic "interactDict" (ppr wi)

657
interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
658 659
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
660 661 662 663
interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
                                          , cc_tyargs = tys@(ip_str:_) })
  = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
       ; stopWith ev "Given IP" }
664 665 666 667 668 669 670 671
  where
    dicts           = inert_dicts inerts
    ip_dicts        = findDictsByClass dicts cls
    other_ip_dicts  = filterBag (not . is_this_ip) ip_dicts
    filtered_dicts  = addDictsByClass dicts cls other_ip_dicts

    -- Pick out any Given constraints for the same implicit parameter
    is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
672
       = isGiven ev && ip_str `tcEqType` ip_str'
673 674 675 676 677
    is_this_ip _ = False

interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)

addFunDepWork :: Ct -> Ct -> TcS ()
678
-- Add derived constraints from type-class functional dependencies.
679
addFunDepWork work_ct inert_ct
680 681
  = emitFunDepDeriveds $
    improveFromAnother derived_loc inert_pred work_pred
682 683 684 685 686
                -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                -- NB: We do create FDs for given to report insoluble equations that arise
                -- from pairs of Givens, and also because of floating when we approximate
                -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
                -- Also see Note [When improvement happens]
687 688 689 690 691 692 693 694
  where
    work_pred  = ctPred work_ct
    inert_pred = ctPred inert_ct
    work_loc   = ctLoc work_ct
    inert_loc  = ctLoc inert_ct
    derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
                                                        inert_pred inert_loc }

Austin Seipp's avatar
Austin Seipp committed
695
{-
696 697 698
Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
699

700 701
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
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
The "let ?x = ..." generates an implication constraint of the form:

?x :: Char => ?x :: Char

Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:

?x :: Char => (?x :: Char => ?x :: Char)

Note that the wanted (?x :: Char) constraint may be solved in
two incompatible ways:  either by using the parameter from the
signature, or by using the local definition.  Our intention is
that the local definition should "shadow" the parameter of the
signature, and we implement this as follows: when we add a new
*given* implicit parameter to the inert set, it replaces any existing
givens for the same implicit parameter.

This works for the normal cases but it has an odd side effect
in some pathological programs like this:

-- This is accepted, the second parameter shadows
f1 :: (?x :: Int, ?x :: Char) => Char
f1 = ?x

-- This is rejected, the second parameter shadows
f2 :: (?x :: Int, ?x :: Char) => Int
f2 = ?x

Both of these are actually wrong:  when we try to use either one,
we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
which would lead to an error.

I can think of two ways to fix this:

  1. Simply disallow multiple constratits for the same implicit
    parameter---this is never useful, and it can be detected completely
    syntactically.

  2. Move the shadowing machinery to the location where we nest
     implications, and add some code here that will produce an
     error if we get multiple givens for the same implicit parameter.


*********************************************************************************
*                                                                               *
                   interactFunEq
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
751
-}
752

753 754
interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- Try interacting the work item with the inert set
755
interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
                                         , cc_tyargs = args, cc_fsk = fsk })
  | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
  = if ev_i `canRewriteOrSame` ev
    then  -- Rewrite work-item using inert
      do { traceTcS "reactFunEq (discharge work item):" $
           vcat [ text "workItem =" <+> ppr workItem
                , text "inertItem=" <+> ppr ev_i ]
         ; reactFunEq ev_i fsk_i ev fsk
         ; stopWith ev "Inert rewrites work item" }
    else  -- Rewrite intert using work-item
      do { traceTcS "reactFunEq (rewrite inert item):" $
           vcat [ text "workItem =" <+> ppr workItem
                , text "inertItem=" <+> ppr ev_i ]
         ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
               -- Do the updInertFunEqs before the reactFunEq, so that
               -- we don't kick out the inertItem as well as consuming it!
         ; reactFunEq ev fsk ev_i fsk_i
         ; stopWith ev "Work item rewrites inert" }

  | Just ops <- isBuiltInSynFamTyCon_maybe tc
  = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
       ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
             do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
779
                = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
780 781 782 783 784 785
                        (interact iargs (lookupFlattenTyVar eqs ifsk))
             do_one ct = pprPanic "interactFunEq" (ppr ct)
       ; mapM_ do_one matching_funeqs
       ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
                                                 , ptext (sLit "TvEqs:") <+> ppr eqs ]
       ; return (ContinueWith workItem) }
786 787

  | otherwise
788
  = return (ContinueWith workItem)
789
  where
790
    eqs    = inert_eqs inerts
791 792 793 794 795
    funeqs = inert_funeqs inerts
    matching_inerts = findFunEqs funeqs tc args

interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)

796
lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
797 798
-- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
-- this is used only when dealing with a CFunEqCan
Austin Seipp's avatar
Austin Seipp committed
799
lookupFlattenTyVar inert_eqs ftv
800
  = case lookupVarEnv inert_eqs ftv of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
801 802
      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
      _                                                       -> mkTyVarTy ftv
803

804 805
reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
           -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
806
           -> TcS ()
807 808
reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
809 810 811 812 813 814 815 816 817 818 819
                         `mkTcTransCo` ctEvCoercion from_this
                         -- :: fsk2 ~ fsk1
             fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
       ; emitWorkNC [new_ev] }

reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
  = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)

reactFunEq _ _ solve_this@(CtDerived {}) _
  = pprPanic "reactFunEq" (ppr solve_this)
820

Austin Seipp's avatar
Austin Seipp committed
821
{-
822 823 824
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
825
solved cache (which is the default behaviour or xCtEvidence), because the interaction
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
may not be contributing towards a solution. Here is an example:

Initial inert set:
  [W] g1 : F a ~ beta1
Work item:
  [W] g2 : F a ~ beta2
The work item will react with the inert yielding the _same_ inert set plus:
    i)   Will set g2 := g1 `cast` g3
    ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
    iii) Will emit [W] g3 : beta1 ~ beta2
Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
will set
      g1 := g ; sym g3
and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
remember that we have this in our solved cache, and it is ... g2! In short we
created the evidence loop:

        g2 := g1 ; g3
        g3 := refl
        g1 := g2 ; sym g3

To avoid this situation we do not cache as solved any workitems (or inert)
which did not really made a 'step' towards proving some goal. Solved's are
just an optimization so we don't lose anything in terms of completeness of
solving.


854
Note [Efficient Orientation]
855 856
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
857 858
          (inert)  ci :: (F ty ~ xi_i)
          (work)   cw :: (F ty ~ xi_w)
859 860
We prefer to keep the inert (else we pass the work item on down
the pipeline, which is a bit silly).  If we keep the inert, we
861
will (a) discharge 'cw'
862 863 864 865 866 867 868 869 870 871 872 873 874 875
     (b) produce a new equality work-item (xi_w ~ xi_i)
Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
    new_work :: xi_w ~ xi_i
    cw := ci ; sym new_work
Why?  Consider the simplest case when xi1 is a type variable.  If
we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
If we generate xi2~xi1, there is less chance of that happening.
Of course it can and should still happen if xi1=a, xi1=Int, say.
But we want to avoid it happening needlessly.

Similarly, if we *can't* keep the inert item (because inert is Wanted,
and work is Given, say), we prefer to orient the new equality (xi_i ~
xi_w).

876 877
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
878
   ---- OLD COMMENT, NOW NOT NEEDED
Gabor Greif's avatar
Gabor Greif committed
879
   ---- because we now allow multiple
880
   ---- wanted FunEqs with the same head
881 882 883
Consider the constraints
  c1 :: F Int ~ a      -- Arising from an application line 5
  c2 :: F Int ~ Bool   -- Arising from an application line 10
884
Suppose that 'a' is a unification variable, arising only from
885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901
flattening.  So there is no error on line 5; it's just a flattening
variable.  But there is (or might be) an error on line 10.

Two ways to combine them, leaving either (Plan A)
  c1 :: F Int ~ a      -- Arising from an application line 5
  c3 :: a ~ Bool       -- Arising from an application line 10
or (Plan B)
  c2 :: F Int ~ Bool   -- Arising from an application line 10
  c4 :: a ~ Bool       -- Arising from an application line 5

Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
on the *totally innocent* line 5.  An example is test SimpleFail16
where the expected/actual message comes out backwards if we use
the wrong plan.

The second is the right thing to do.  Hence the isMetaTyVarTy
test when solving pairwise CFunEqCan.
902 903


904 905 906 907 908
*********************************************************************************
*                                                                               *
                   interactTyVarEq
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
909
-}
910

911 912
interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- CTyEqCans are always consumed, so always returns Stop
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
913 914 915 916
interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                          , cc_rhs = rhs
                                          , cc_ev = ev
                                          , cc_eq_rel = eq_rel })
917
  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
918
                             <- findTyEqs inerts tv
919
                         , ev_i `canRewriteOrSame` ev
920
                         , rhs_i `tcEqType` rhs ]
921 922
  =  -- Inert:     a ~ b
     -- Work item: a ~ b
923
    do { setEvBindIfWanted ev (ctEvTerm ev_i)
924
       ; stopWith ev "Solved from inert" }
925 926 927

  | Just tv_rhs <- getTyVar_maybe rhs
  , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
928
                             <- findTyEqs inerts tv_rhs
929
                         , ev_i `canRewriteOrSame` ev
930
                         , rhs_i `tcEqType` mkTyVarTy tv ]
931 932
  =  -- Inert:     a ~ b
     -- Work item: b ~ a
933
    do { setEvBindIfWanted ev
934 935
                   (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
       ; stopWith ev "Solved from inert (r)" }
936

937
  | otherwise
938
  = do { tclvl <- getTcLevel
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
939
       ; if canSolveByUnification tclvl ev eq_rel tv rhs
940
         then do { solveByUnification ev tv rhs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
941 942 943 944
                 ; n_kicked <- kickOutRewritable Given NomEq tv
                               -- Given because the tv := xi is given
                               -- NomEq because only nom. equalities are solved
                               -- by unification
945 946 947 948 949
                 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }

         else do { traceTcS "Can't solve tyvar equality"
                       (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
                             , ppWhen (isMetaTyVar tv) $
950 951
                               nest 4 (text "TcLevel of" <+> ppr tv
                                       <+> text "is" <+> ppr (metaTyVarTcLevel tv))
952
                             , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
953
                             , text "TcLevel =" <+> ppr tclvl ])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
954 955 956
                 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
                                                 (ctEvEqRel ev)
                                                 tv
957 958
                 ; updInertCans (\ ics -> addInertCan ics workItem)
                 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
959

960
interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
961

962 963 964
-- @trySpontaneousSolve wi@ solves equalities where one side is a
-- touchable unification variable.
-- Returns True <=> spontaneous solve happened
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
965 966 967 968 969 970
canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
                      -> TcTyVar -> Xi -> Bool
canSolveByUnification tclvl gw eq_rel tv xi
  | ReprEq <- eq_rel   -- we never solve representational equalities this way.
  = False

971 972 973
  | isGiven gw   -- See Note [Touchables and givens]
  = False

974
  | isTouchableMetaTyVar tclvl tv
975 976 977 978 979 980