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

3
module TcInteract (
4
     solveSimpleGivens,   -- Solves [Ct]
5 6 7
     solveSimpleWanteds,  -- Solves Cts

     solveCallStack,      -- for use in TcSimplify
8
  ) where
9 10 11

#include "HsVersions.h"

12
import BasicTypes ( infinity, IntWithInf, intGtLimit )
13
import HsTypes ( HsIPName(..) )
14
import TcCanonical
15
import TcFlatten
16 17
import VarSet
import Type
18
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
19
import CoAxiom( sfInteractTop, sfInteractInert )
20 21 22

import Var
import TcType
23
import Name
24
import PrelNames ( knownNatClassName, knownSymbolClassName,
25
                   typeableClassName, coercibleTyConKey,
26 27
                   heqTyConKey, ipClassKey )
import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
28 29
                    coercibleDataCon )
import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
30
import Id( idType )
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
31
import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
32 33
import Class
import TyCon
34
import DataCon( dataConWrapId )
35
import FunDeps
36
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
37 38
import FamInstEnv
import Unify ( tcUnifyTyWithTFs )
39

40
import TcEvidence
41 42
import Outputable

43 44
import TcRnTypes
import TcSMonad
45
import Bag
Jan Stolarek's avatar
Jan Stolarek committed
46
import MonadUtils ( concatMapM )
47

Adam Gundry's avatar
Adam Gundry committed
48
import Data.List( partition, foldl', deleteFirstsBy )
49
import SrcLoc
dimitris's avatar
dimitris committed
50 51
import VarEnv

52
import Control.Monad
53
import Maybes( isJust )
54
import Pair (Pair(..))
55
import Unique( hasKey )
56
import DynFlags
57
import Util
58
import qualified GHC.LanguageExtensions as LangExt
59

Austin Seipp's avatar
Austin Seipp committed
60
{-
61
**********************************************************************
62
*                                                                    *
63 64 65 66
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

67
Note [Basic Simplifier Plan]
68
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
69
1. Pick an element from the WorkList if there exists one with depth
70
   less than our context-stack depth.
71

72
2. Run it down the 'stage' pipeline. Stages are:
73 74 75 76
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level intreactions
77
   Each stage returns a StopOrContinue and may have sideffected
78
   the inerts or worklist.
79 80 81 82 83 84

   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
85 86
   then we add him in the inerts and jump back to Step 1.

87
If in Step 1 no such element exists, we have exceeded our context-stack
88
depth and will simply fail.
89

90
Note [Unflatten after solving the simple wanteds]
91
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
92
We unflatten after solving the wc_simples of an implication, and before attempting
93 94
to float. This means that

95
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
Jan Stolarek's avatar
Jan Stolarek committed
96
   need to worry about them across successive passes over the constraint tree.
97 98 99 100 101 102 103 104 105 106 107 108 109 110
   (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
111
   will do exactly that after solving the simple constraints and before
112 113 114 115 116 117 118 119 120
   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
121 122 123

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
124 125
There is an annoying mismatch between solveSimpleGivens and
solveSimpleWanteds, because the latter needs to fiddle with the inert
Jan Stolarek's avatar
Jan Stolarek committed
126
set, unflatten and zonk the wanteds.  It passes the zonked wanteds
127 128 129 130 131 132
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
133
-}
134

135 136
solveSimpleGivens :: [Ct] -> TcS Cts
solveSimpleGivens givens
137
  | null givens  -- Shortcut for common case
138
  = return emptyCts
139
  | otherwise
140 141 142 143 144
  = do { traceTcS "solveSimpleGivens {" (ppr givens)
       ; go givens
       ; given_insols <- takeGivenInsolubles
       ; traceTcS "End solveSimpleGivens }" (text "Insoluble:" <+> pprCts given_insols)
       ; return given_insols }
145
  where
146
    go givens = do { solveSimples (listToBag givens)
Adam Gundry's avatar
Adam Gundry committed
147
                   ; new_givens <- runTcPluginsGiven
148 149
                   ; when (notNull new_givens) $
                     go new_givens }
150

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

172 173
     | isEmptyBag (wc_simple wc)
     = return (n,wc)
174

175 176
     | otherwise
     = do { -- Solve
177
            (unif_count, wc1) <- solve_simple_wanteds wc
178 179

            -- Run plugins
180
          ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
181 182
             -- See Note [Running plugins on unflattened wanteds]

183 184 185 186 187
          ; 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

188

189
solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
190 191 192 193 194 195
-- 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
196 197
       ; (unif_count, unflattened_eqs) <- reportUnifications $
                                          unflatten tv_eqs fun_eqs
198
            -- See Note [Unflatten after solving the simple wanteds]
199
       ; return ( unif_count
200 201 202 203
                , WC { wc_simple = others `andCts` unflattened_eqs
                     , wc_insol  = insols1 `andCts` insols2
                     , wc_impl   = implics1 `unionBags` implics2 }) }

204 205
{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
206 207
Solving a bunch of simple constraints is done in a loop,
(the 'go' loop of 'solveSimpleWanteds'):
208 209 210 211 212 213 214 215 216
  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]
217
-}
218 219 220

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
221
solveSimples :: Cts -> TcS ()
222
-- Returns the final InertSet in TcS
Jan Stolarek's avatar
Jan Stolarek committed
223
-- Has no effect on work-list or residual-implications
224 225
-- The constraints are initially examined in left-to-right order

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

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
241
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
242 243
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
244 245 246 247 248 249 250 251 252 253
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
254 255 256 257

-- | 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
258
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
259
-- main solver.
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
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
285 286 287
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
288
      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
Adam Gundry's avatar
Adam Gundry committed
289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
      _ -> 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
    }

311 312 313
getTcPlugins :: TcS [TcPluginSolver]
getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }

Adam Gundry's avatar
Adam Gundry committed
314 315 316 317 318 319 320 321 322 323 324 325 326
-- | 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.
327 328 329
runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPlugins plugins all_cts
  = foldM do_plugin initialProgress plugins
Adam Gundry's avatar
Adam Gundry committed
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 368 369 370 371 372
  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)


373
type WorkItem = Ct
374
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
375

376 377 378
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
                  -> WorkItem                   -- The work item
                  -> TcS ()
379
-- Run this item down the pipeline, leaving behind new work and inerts
380
runSolverPipeline pipeline workItem
381
  = do { wl <- getWorkList
382
       ; traceTcS "Start solver pipeline {" $
383 384
                  vcat [ text "work item =" <+> ppr workItem
                       , text "rest of worklist =" <+> ppr wl ]
385

386
       ; bumpStepCountTcS    -- One step for each constraint processed
387 388 389
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

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

Austin Seipp's avatar
Austin Seipp committed
413
{-
414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
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
436
-}
437

438
thePipeline :: [(String,SimplifierStage)]
439
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
440 441
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
442

Austin Seipp's avatar
Austin Seipp committed
443
{-
444
*********************************************************************************
445
*                                                                               *
446 447 448 449
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

450 451 452 453 454
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

455
   If the work-item is Given,
456 457
   then the inert item must Given

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

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

476
-- Interaction result of  WorkItem <~> Ct
477

478
type StopNowFlag = Bool    -- True <=> stop after this interaction
479

480
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
481 482
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
483

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

496 497 498 499 500
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

501
instance Outputable InteractResult where
502 503 504
  ppr IRKeep    = text "keep"
  ppr IRReplace = text "replace"
  ppr IRDelete  = text "delete"
505 506 507 508 509 510

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
                     -> TcS (InteractResult, StopNowFlag)
-- Preconditions:
-- 1) inert and work item represent evidence for the /same/ predicate
511
-- 2) ip/class/irred constraints only; not used for equalities
512
solveOneFromTheOther ev_i ev_w
513
  | isDerived ev_w         -- Work item is Derived; just discard it
514 515
  = return (IRKeep, True)

516 517 518
  | 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
519

520 521 522 523
  | CtWanted { ctev_loc = loc_w } <- ev_w
  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
  = return (IRDelete, False)

524 525 526
  | CtWanted { ctev_dest = dest } <- ev_w
       -- Inert is Given or Wanted
  = do { setWantedEvTerm dest (ctEvTerm ev_i)
527 528
       ; return (IRKeep, True) }

529 530 531 532 533 534
  | 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

535 536
  | CtWanted { ctev_dest = dest } <- ev_i
  = do { setWantedEvTerm dest (ctEvTerm ev_w)
537 538
       ; return (IRReplace, True) }

539 540 541 542
  -- So they are both Given
  -- See Note [Replacement vs keeping]
  | lvl_i == lvl_w
  = do { binds <- getTcEvBindsMap
543
       ; return (same_level_strategy binds, True) }
544

545 546 547
  | otherwise   -- Both are Given, levels differ
  = return (different_level_strategy, True)
  where
548 549 550 551 552
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
553

554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574
     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

575
     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
576

Austin Seipp's avatar
Austin Seipp committed
577
{-
578 579 580
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
581
we keep?  More subtle than you might think!
582

583
  * Constraints come from different levels (different_level_strategy)
584

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

589 590 591 592
      - 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.
593

594 595 596 597
        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.

Gabor Greif's avatar
Gabor Greif committed
598
  * Constraints coming from the same level (i.e. same implication)
599 600 601 602 603 604 605 606

       - 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.
            Example:  f :: (Eq a, Ord a) => blah
Simon Peyton Jones's avatar
Simon Peyton Jones committed
607
            then we may find [G] d3 :: Eq a
608
                             [G] d2 :: Eq a
Simon Peyton Jones's avatar
Simon Peyton Jones committed
609
              with bindings  d3 = sc_sel (d1::Ord a)
610 611
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
612
         Why? See Note [Tracking redundant constraints] in TcSimplify again.
613

614
  * Finally, when there is still a choice, use IRKeep rather than
Gabor Greif's avatar
Gabor Greif committed
615
    IRReplace, to avoid unnecessary munging of the inert set.
616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636

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

637 638 639 640 641
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
642
-}
643

644 645 646 647
-- 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)
648
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
649 650 651

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
652 653 654
        (matching_irreds, others)
          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
                         (inert_irreds inerts)
655 656 657 658
  , (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
659 660 661 662 663 664 665
       ; 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
666
            return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
667 668
       ; else
            continueWith workItem }
669

670
  | otherwise
671
  = continueWith workItem
672

673
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
674

Austin Seipp's avatar
Austin Seipp committed
675
{-
676 677 678 679 680
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
681
-}
682

683
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
684
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
685
  | isWanted ev_w
Eric Seidel's avatar
Eric Seidel committed
686
  , Just ip_name      <- isCallStackPred (ctPred workItem)
687 688 689 690
  , OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
  -- If we're given a CallStack constraint that arose from a function
  -- call, we need to push the current call-site onto the stack instead
  -- of solving it directly from a given.
691
  -- See Note [Overview of implicit CallStacks]
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708
  = do { let loc = ctEvLoc ev_w

         -- First we emit a new constraint that will capture the
         -- given CallStack.
       ; let new_loc      = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
                            -- We change the origin to IPOccOrigin so
                            -- this rule does not fire again.
                            -- See Note [Overview of implicit CallStacks]

       ; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
       ; emitWorkNC (freshGoals [mb_new])

         -- Then we solve the wanted by pushing the call-site onto the
         -- newly emitted CallStack.
       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
       ; solveCallStack ev_w ev_cs
       ; stopWith ev_w "Wanted CallStack IP" }
709

710
  | Just ctev_i <- lookupInertDict inerts cls tys
711
  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
712 713 714 715 716
       ; 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
717
            return (Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect)))
Austin Seipp's avatar
Austin Seipp committed
718
         else
719
            continueWith workItem }
720

721
  | cls `hasKey` ipClassKey
722 723 724 725
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
726 727 728 729 730 731 732 733 734
  = 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)
735 736
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
737 738
               -- Importantly we don't throw workitem back in the
               -- worklist because this can cause loops (see #5236)
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
  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 }
754

755
{-
756 757
**********************************************************************
*                                                                    *
758
                   Implicit parameters
759 760
*                                                                    *
**********************************************************************
761
-}
762

763
interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
764 765
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
766 767 768 769
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" }
770 771 772 773 774 775 776 777
  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':_ })
778
       = isGiven ev && ip_str `tcEqType` ip_str'
779 780 781 782
    is_this_ip _ = False

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

783

Austin Seipp's avatar
Austin Seipp committed
784
{-
785 786 787
Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
788

789 790
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
791

792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834
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.


835 836
**********************************************************************
*                                                                    *
837
                   interactFunEq
838 839
*                                                                    *
**********************************************************************
Austin Seipp's avatar
Austin Seipp committed
840
-}
841

842 843
interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- Try interacting the work item with the inert set
844
interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
845
                                         , cc_tyargs = args, cc_fsk = fsk })
846 847
  | Just (CFunEqCan { cc_ev = ev_i
                    , cc_fsk = fsk_i }) <- matching_inerts
848
  = if ev_i `funEqCanDischarge` ev
849 850 851 852 853 854
    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" }
855
    else  -- Rewrite inert using work-item
856
      ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
857 858 859 860 861 862 863 864 865
      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" }

Jan Stolarek's avatar
Jan Stolarek committed
866 867 868 869 870 871
  | otherwise   -- Try improvement
  = do { improveLocalFunEqs loc inerts tc args fsk
       ; continueWith workItem }
  where
    loc             = ctEvLoc ev
    funeqs          = inert_funeqs inerts
872
    matching_inerts = findFunEq funeqs tc args
873

Jan Stolarek's avatar
Jan Stolarek committed
874 875 876 877 878 879 880 881 882 883
interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)

improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
                   -> TcS ()
-- Generate derived improvement equalities, by comparing
-- the current work item with inert CFunEqs
-- E.g.   x + y ~ z,   x + y' ~ z   =>   [D] y ~ y'
improveLocalFunEqs loc inerts fam_tc args fsk
  | not (null improvement_eqns)
  = do { traceTcS "interactFunEq improvements: " $
884 885 886
         vcat [ text "Eqns:" <+> ppr improvement_eqns
              , text "Candidates:" <+> ppr funeqs_for_tc
              , text "Model:" <+> ppr model ]
Jan Stolarek's avatar
Jan Stolarek committed
887
       ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
888
  | otherwise
Jan Stolarek's avatar
Jan Stolarek committed
889
  = return ()
890
  where
891
    model         = inert_model inerts
Jan Stolarek's avatar
Jan Stolarek committed
892 893
    funeqs        = inert_funeqs inerts
    funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
894
    rhs           = lookupFlattenTyVar model fsk
Jan Stolarek's avatar
Jan Stolarek committed
895 896 897 898 899 900

    --------------------
    improvement_eqns
      | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
      =    -- Try built-in families, notably for arithmethic
         concatMap (do_one_built_in ops) funeqs_for_tc
901

Jan Stolarek's avatar
Jan Stolarek committed
902 903 904
      | Injective injective_args <- familyTyConInjectivityInfo fam_tc
      =    -- Try improvement from type families with injectivity annotations
         concatMap (do_one_injective injective_args) funeqs_for_tc
905

Jan Stolarek's avatar
Jan Stolarek committed
906 907 908 909 910
      | otherwise
      = []

    --------------------
    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
911
      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
Jan Stolarek's avatar
Jan Stolarek committed
912 913 914 915 916 917
    do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)

    --------------------
    -- See Note [Type inference for type families with injectivity]
    do_one_injective injective_args
                    (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
918
      | rhs `tcEqType` lookupFlattenTyVar model ifsk
Jan Stolarek's avatar
Jan Stolarek committed
919 920 921 922 923 924 925 926
      = [Pair arg iarg | (arg, iarg, True)
                           <- zip3 args iargs injective_args ]
      | otherwise
      = []
    do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)

-------------
lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
927
-- See Note [lookupFlattenTyVar]
Jan Stolarek's avatar
Jan Stolarek committed
928
lookupFlattenTyVar model ftv
929
  = case lookupDVarEnv model ftv of
Jan Stolarek's avatar
Jan Stolarek committed
930 931
      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
      _                                                   -> mkTyVarTy ftv
932

933 934
reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
           -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
935
           -> TcS ()
936 937 938 939
reactFunEq from_this fsk1 solve_this fsk2
  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
                         ctEvCoercion from_this
940
                         -- :: fsk2 ~ fsk1
941 942 943
             fsk_eq_pred = mkTcEqPredLikeEv solve_this
                             (mkTyVarTy fsk2) (mkTyVarTy fsk1)

944 945 946
       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
       ; emitWorkNC [new_ev] }

947 948 949 950 951 952
  | otherwise
  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
                                ppr solve_this $$ ppr fsk2)
       ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
       ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                     ppr solve_this $$ ppr fsk2) }
953

954 955 956 957 958 959 960 961 962 963 964 965
{- Note [lookupFlattenTyVar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Supppose we have an injective function F and
  inert_funeqs:   F t1 ~ fsk1
                  F t2 ~ fsk2
  model           fsk1 ~ fsk2

We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
cc_fsk of CFunEqCans in the model when trying to find derived
equalities arising from injectivity.

Jan Stolarek's avatar
Jan Stolarek committed
966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003
Note [Type inference for type families with injectivity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a type family with an injectivity annotation:
    type family F a b = r | r -> b

Then if we have two CFunEqCan constraints for F with the same RHS
   F s1 t1 ~ rhs
   F s2 t2 ~ rhs
then we can use the injectivity to get a new Derived constraint on
the injective argument
  [D] t1 ~ t2

That in turn can help GHC solve constraints that would otherwise require
guessing.  For example, consider the ambiguity check for
   f :: F Int b -> Int
We get the constraint
   [W] F Int b ~ F Int beta
where beta is a unification variable.  Injectivity lets us pick beta ~ b.

Injectivity information is also used at the call sites. For example:
   g = f True
gives rise to
   [W] F Int b ~ Bool
from which we can derive b.  This requires looking at the defining equations of
a type family, ie. finding equation with a matching RHS (Bool in this example)
and infering values of type variables (b in this example) from the LHS patterns
of the matching equation.  For closed type families we have to perform
additional apartness check for the selected equation to check that the selected
is guaranteed to fire for given LHS arguments.

These new constraints are simply *Derived* constraints; they have no evidence.
We could go further and offer evidence from decomposing injective type-function
applications, but that would require new evidence forms, and an extension to
FC, so we don't do that right now (Dec 14).

See also Note [Injective type families] in TyCon


1004 1005 1006
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1007
solved cache (which is the default behaviour or xCtEvidence), because the interaction
1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035
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.


1036
Note [Efficient Orientation]
1037 1038
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
1039 1040
          (inert)  ci :: (F ty ~ xi_i)
          (work)   cw :: (F ty ~ xi_w)
1041 1042
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
1043
will (a) discharge 'cw'
1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057
     (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).

1058 1059
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1060
   ---- OLD COMMENT, NOW NOT NEEDED