TcInteract.hs 77.1 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 ( infinity, IntWithInf, intGtLimit )
11 12
import HsTypes ( hsIPNameFS )
import FastString
13
import TcCanonical
14
import TcFlatten
15 16
import VarSet
import Type
17
import Kind ( isKind )
18
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
19
import CoAxiom(sfInteractTop, sfInteractInert)
20 21 22

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

34
import TcEvidence
35 36
import Outputable

37 38
import TcRnTypes
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 Cts
-- Solves the givens, adding them to the inert set
129 130
-- Returns any insoluble givens, which represent inaccessible code,
-- taking those ones out of the inert set
131
solveSimpleGivens loc givens
132
  | null givens  -- Shortcut for common case
133
  = return emptyCts
134
  | otherwise
135
  = do { go (map mk_given_ct givens)
136
       ; takeGivenInsolubles }
137
  where
138
    mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
139 140
                                                , ctev_pred = evVarPred ev_id
                                                , ctev_loc  = loc })
141
    go givens = do { solveSimples (listToBag givens)
Adam Gundry's avatar
Adam Gundry committed
142 143 144
                   ; new_givens <- runTcPluginsGiven
                   ; when (notNull new_givens) (go new_givens)
                   }
145

146
solveSimpleWanteds :: Cts -> TcS WantedConstraints
147 148 149 150
-- NB: 'simples' may contain /derived/ equalities, floated
--     out from a nested implication. So don't discard deriveds!
solveSimpleWanteds simples
  = do { traceTcS "solveSimples {" (ppr simples)
151 152
       ; dflags <- getDynFlags
       ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
153 154 155 156
       ; traceTcS "solveSimples end }" $
             vcat [ ptext (sLit "iterations =") <+> ppr n
                  , ptext (sLit "residual =") <+> ppr wc ]
       ; return wc }
157
  where
158 159 160 161 162 163 164 165
    go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
    go n limit wc
      | n `intGtLimit` limit
      = failTcS (hang (ptext (sLit "solveSimpleWanteds: too many iterations")
                       <+> parens (ptext (sLit "limit =") <+> ppr limit))
                    2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
                            , ptext (sLit "Simples =") <+> ppr simples
                            , ptext (sLit "WC =")      <+> ppr wc ]))
166

167 168
     | isEmptyBag (wc_simple wc)
     = return (n,wc)
169

170 171
     | otherwise
     = do { -- Solve
172
            (unif_count, wc1) <- solve_simple_wanteds wc
173 174

            -- Run plugins
175
          ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
176 177
             -- See Note [Running plugins on unflattened wanteds]

178 179 180 181 182
          ; if unif_count == 0 && not rerun_plugin
            then return (n, wc2)             -- Done
            else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
                    ; go (n+1) limit wc2 } }      -- Loop

183

184
solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
185 186 187 188 189 190
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
  = nestTcS $
    do { solveSimples simples1
       ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
191 192
       ; (unif_count, unflattened_eqs) <- reportUnifications $
                                          unflatten tv_eqs fun_eqs
193
            -- See Note [Unflatten after solving the simple wanteds]
194
       ; return ( unif_count
195 196 197 198
                , WC { wc_simple = others `andCts` unflattened_eqs
                     , wc_insol  = insols1 `andCts` insols2
                     , wc_impl   = implics1 `unionBags` implics2 }) }

199 200
{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
201 202
Solving a bunch of simple constraints is done in a loop,
(the 'go' loop of 'solveSimpleWanteds'):
203 204 205 206 207 208 209 210 211
  1. Try to solve them; unflattening may lead to improvement that
     was not exploitable during solving
  2. Try the plugin
  3. If step 1 did improvement during unflattening; or if the plugin
     wants to run again, go back to step 1

Non-obviously, improvement can also take place during
the unflattening that takes place in step (1). See TcFlatten,
See Note [Unflattening can force the solver to iterate]
212
-}
213 214 215

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

221 222
solveSimples cts
  = {-# SCC "solveSimples" #-}
223 224
    do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
       ; solve_loop }
225
  where
226
    solve_loop
227
      = {-# SCC "solve_loop" #-}
228
        do { sel <- selectNextWorkItem
229
           ; case sel of
230 231 232
              Nothing -> return ()
              Just ct -> do { runSolverPipeline thePipeline ct
                            ; solve_loop } }
Adam Gundry's avatar
Adam Gundry committed
233 234 235

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
236
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
237 238
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
239 240 241 242 243 244 245 246 247 248
runTcPluginsGiven
  = do { plugins <- getTcPlugins
       ; if null plugins then return [] else
    do { givens <- getInertGivens
       ; if null givens then return [] else
    do { p <- runTcPlugins plugins (givens,[],[])
       ; let (solved_givens, _, _) = pluginSolvedCts p
       ; updInertCans (removeInertCts solved_givens)
       ; mapM_ emitInsoluble (pluginBadCts p)
       ; return (pluginNewCts p) } } }
Adam Gundry's avatar
Adam Gundry committed
249 250 251 252

-- | 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
253
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
254
-- main solver.
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
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
  | isEmptyBag simples1
  = return (False, wc)
  | otherwise
  = do { plugins <- getTcPlugins
       ; if null plugins then return (False, wc) else

    do { given <- getInertGivens
       ; simples1 <- zonkSimples simples1    -- Plugin requires zonked inputs
       ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
       ; p <- runTcPlugins plugins (given, derived, wanted)
       ; let (_, _,                solved_wanted)   = pluginSolvedCts p
             (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
             new_wanted                             = pluginNewCts p

-- SLPJ: I'm deeply suspicious of this
--       ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)

       ; mapM_ setEv solved_wanted
       ; return ( notNull (pluginNewCts p)
                , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
                                                        `andCts` listToBag unsolved_derived
                     , wc_insol  = listToBag (pluginBadCts p) `andCts` insols1
                     , wc_impl   = implics1 } ) } }
Adam Gundry's avatar
Adam Gundry committed
280 281 282
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
283
      CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
Adam Gundry's avatar
Adam Gundry committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
      _ -> 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
    }

306 307 308
getTcPlugins :: TcS [TcPluginSolver]
getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }

Adam Gundry's avatar
Adam Gundry committed
309 310 311 312 313 314 315 316 317 318 319 320 321
-- | 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.
322 323 324
runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPlugins plugins all_cts
  = foldM do_plugin initialProgress plugins
Adam Gundry's avatar
Adam Gundry committed
325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
  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)


368
type WorkItem = Ct
369
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
370

371 372 373
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
                  -> WorkItem                   -- The work item
                  -> TcS ()
374
-- Run this item down the pipeline, leaving behind new work and inerts
375 376 377 378
runSolverPipeline pipeline workItem
  = do { initial_is <- getTcSInerts
       ; traceTcS "Start solver pipeline {" $
                  vcat [ ptext (sLit "work item = ") <+> ppr workItem
379 380
                       , ptext (sLit "inerts    = ") <+> ppr initial_is]

381
       ; bumpStepCountTcS    -- One step for each constraint processed
382 383 384
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

       ; final_is <- getTcSInerts
385
       ; case final_res of
386 387 388
           Stop ev s       -> do { traceFireTcS ev s
                                 ; traceTcS "End solver pipeline (discharged) }"
                                       (ptext (sLit "inerts =") <+> ppr final_is)
389
                                 ; return () }
390
           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
391
                                 ; traceTcS "End solver pipeline (kept as inert) }" $
392
                                       vcat [ ptext (sLit "final_item =") <+> ppr ct
393
                                            , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
394
                                            , ptext (sLit "inerts     =") <+> ppr final_is]
395
                                 ; addInertCan ct }
396
       }
Austin Seipp's avatar
Austin Seipp committed
397
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
398 399 400
                     -> TcS (StopOrContinue Ct)
        run_pipeline [] res        = return res
        run_pipeline _ (Stop ev s) = return (Stop ev s)
401 402
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
403 404
                          (text "workitem   = " <+> ppr ct)
               ; res <- stg ct
405
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
406
               ; run_pipeline stgs res }
407

Austin Seipp's avatar
Austin Seipp committed
408
{-
409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430
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
431
-}
432

433
thePipeline :: [(String,SimplifierStage)]
434
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
435 436
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
437

Austin Seipp's avatar
Austin Seipp committed
438
{-
439
*********************************************************************************
440
*                                                                               *
441 442 443 444
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

445 446 447 448 449
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

450
   If the work-item is Given,
451 452
   then the inert item must Given

453
But this isn't quite true.  Suppose we have,
454 455 456 457
    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
458
solve c3, we must re-react it with the inert set.  So we can attempt a
459 460 461
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
462
   If the work-item is Given,
463 464 465
   AND there is a reaction
   then the inert item must Given
or, equivalently,
466
   If the work-item is Given,
467 468
   and the inert item is Wanted/Derived
   then there is no reaction
Austin Seipp's avatar
Austin Seipp committed
469
-}
470

471
-- Interaction result of  WorkItem <~> Ct
472

473
type StopNowFlag = Bool    -- True <=> stop after this interaction
474

475
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
476 477
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
478

479
interactWithInertsStage wi
480 481
  = do { inerts <- getTcSInerts
       ; let ics = inert_cans inerts
482
       ; case wi of
483 484 485 486
             CTyEqCan    {} -> interactTyVarEq ics wi
             CFunEqCan   {} -> interactFunEq   ics wi
             CIrredEvCan {} -> interactIrred   ics wi
             CDictCan    {} -> interactDict    ics wi
487
             _ -> pprPanic "interactWithInerts" (ppr wi) }
488 489
                -- CHoleCan are put straight into inert_frozen, so never get here
                -- CNonCanonical have been canonicalised
490

491 492 493 494 495
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

496 497 498 499 500 501 502 503 504 505 506 507
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
508
  | isDerived ev_w         -- Work item is Derived; just discard it
509 510
  = return (IRKeep, True)

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

515 516 517 518 519
  | CtWanted { ctev_loc = loc_w } <- ev_w
  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
  = return (IRDelete, False)

  | CtWanted { ctev_evar = ev_id } <- ev_w   -- Inert is Given or Wanted
520
  = do { setWantedEvBind ev_id (ctEvTerm ev_i)
521 522
       ; return (IRKeep, True) }

523 524 525 526 527 528 529
  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
  = return (IRKeep, False)  -- Just discard the un-usable Given
                            -- This never actually happens because
                            -- Givens get processed first

  | CtWanted { ctev_evar = ev_id } <- ev_i   -- Work item is Given
530
  = do { setWantedEvBind ev_id (ctEvTerm ev_w)
531 532
       ; return (IRReplace, True) }

533 534 535 536
  -- So they are both Given
  -- See Note [Replacement vs keeping]
  | lvl_i == lvl_w
  = do { binds <- getTcEvBindsMap
537
       ; return (same_level_strategy binds, True) }
538

539 540 541
  | otherwise   -- Both are Given, levels differ
  = return (different_level_strategy, True)
  where
542 543 544 545 546
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
547

548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568
     different_level_strategy
       | isIPPred pred, lvl_w > lvl_i = IRReplace
       | lvl_w < lvl_i                = IRReplace
       | otherwise                    = IRKeep

     same_level_strategy binds        -- Both Given
       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
       = case ctLocOrigin loc_w of
            GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
                                     | otherwise -> IRKeep
            _                                    -> IRReplace

       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
       = IRKeep

       | has_binding binds ev_w
       , not (has_binding binds ev_i)
       = IRReplace

       | otherwise = IRKeep

569
     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
570

Austin Seipp's avatar
Austin Seipp committed
571
{-
572 573 574
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
575
we keep?  More subtle than you might think!
576

577
  * Constraints come from different levels (different_level_strategy)
578

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

583 584 585 586
      - 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,
        and can be reported as redundant.  See Note [Tracking redundant constraints]
        in TcSimplify.
587

588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
        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.

  * Constaints coming from the same level (i.e. same implication)

       - Always get rid of InstSC ones if possible, since they are less
         useful for solving.  If both are InstSC, choose the one with
         the smallest TypeSize
         See Note [Solving superclass constraints] in TcInstDcls

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

607 608
  * Finally, when there is still a choice, use IRKeep rather than
    IRReplace, to avoid unnecesary munging of the inert set.
609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629

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

630 631 632 633 634
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
635
-}
636

637 638 639 640
-- 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)
641
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
642 643 644

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
645
        (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
646 647 648 649 650
                                                 (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
651 652 653 654 655 656 657 658 659 660
       ; 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 }
661

662
  | otherwise
663
  = continueWith workItem
664

665
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
666

Austin Seipp's avatar
Austin Seipp committed
667
{-
668 669 670 671 672
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
673
-}
674

675
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
676
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
677 678 679
  -- don't ever try to solve CallStack IPs directly from other dicts,
  -- we always build new dicts instead.
  -- See Note [Overview of implicit CallStacks]
680
  | Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls tys
681 682
  , isWanted ev_w
  = do let ev_cs =
683
             case lookupInertDict inerts cls tys of
684 685 686 687 688 689 690 691 692 693 694 695
               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"

696
  | Just ctev_i <- lookupInertDict inerts cls tys
697
  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
698 699 700 701 702 703
       ; 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
704
         else
705
            continueWith workItem }
706 707 708 709 710 711

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

  | otherwise
712 713 714 715 716 717 718 719 720
  = do { addFunDepWork inerts ev_w cls
       ; continueWith workItem  }

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

addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
-- Add derived constraints from type-class functional dependencies.
addFunDepWork inerts work_ev cls
  = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
721 722
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
723 724
               -- Importantly we don't throw workitem back in the
               -- worklist because this can cause loops (see #5236)
725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
  where
    work_pred = ctEvPred work_ev
    work_loc  = ctEvLoc work_ev
    add_fds inert_ct
      = emitFunDepDeriveds $
        improveFromAnother derived_loc inert_pred work_pred
               -- 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
      where
        inert_pred = ctPred inert_ct
        inert_loc  = ctLoc inert_ct
        derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
                                                            inert_pred inert_loc }
740

741 742 743 744 745 746 747
{-
*********************************************************************************
*                                                                               *
                   Implicit parameters
*                                                                               *
*********************************************************************************
-}
748

749
interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
750 751
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
752 753 754 755
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" }
756 757 758 759 760 761 762 763
  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':_ })
764
       = isGiven ev && ip_str `tcEqType` ip_str'
765 766 767 768
    is_this_ip _ = False

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

Austin Seipp's avatar
Austin Seipp committed
769
{-
770 771 772
Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
773

774 775
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
776

777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824
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
825
-}
826

827 828
interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- Try interacting the work item with the inert set
829
interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
830 831
                                         , cc_tyargs = args, cc_fsk = fsk })
  | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
832
  = if ev_i `canDischarge` ev
833 834 835 836 837 838
    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" }
839
    else  -- Rewrite inert using work-item
840
      ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i )
841 842 843 844 845 846 847 848 849
      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" }

850
  | Just ops <- isBuiltInSynFamTyCon_maybe tc
851 852 853
  = 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
854
                = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
855 856 857 858 859 860
                        (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) }
861 862

  | otherwise
863
  = return (ContinueWith workItem)
864
  where
865
    eqs    = inert_eqs inerts
866 867 868 869 870
    funeqs = inert_funeqs inerts
    matching_inerts = findFunEqs funeqs tc args

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

871
lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
872 873
-- ^ 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
874
lookupFlattenTyVar inert_eqs ftv
875
  = case lookupVarEnv inert_eqs ftv of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
876 877
      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
      _                                                       -> mkTyVarTy ftv
878

879 880
reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
           -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
881
           -> TcS ()
882 883
reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
884 885 886 887 888 889
                         `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] }

890 891 892 893
reactFunEq from_this fuv1 ev fuv2
  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2)
       ; dischargeFmv ev fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
       ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2) }
894

Austin Seipp's avatar
Austin Seipp committed
895
{-
896 897 898
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
899
solved cache (which is the default behaviour or xCtEvidence), because the interaction
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
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.


928
Note [Efficient Orientation]
929 930
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
931 932
          (inert)  ci :: (F ty ~ xi_i)
          (work)   cw :: (F ty ~ xi_w)
933 934
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
935
will (a) discharge 'cw'
936 937 938 939 940 941 942 943 944 945 946 947 948 949
     (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).

950 951
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
952
   ---- OLD COMMENT, NOW NOT NEEDED
Gabor Greif's avatar
Gabor Greif committed
953
   ---- because we now allow multiple
954
   ---- wanted FunEqs with the same head
955 956 957
Consider the constraints
  c1 :: F Int ~ a      -- Arising from an application line 5
  c2 :: F Int ~ Bool   -- Arising from an application line 10
958
Suppose that 'a' is a unification variable, arising only from
959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975
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.
976 977


978 979 980 981 982
*********************************************************************************
*                                                                               *
                   interactTyVarEq
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
983
-}
984

985 986
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
987 988 989 990
interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                          , cc_rhs = rhs
                                          , cc_ev = ev
                                          , cc_eq_rel = eq_rel })
991
  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }