TcInteract.hs 86.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 FastString
15
import TcCanonical
16
import TcFlatten
17 18
import VarSet
import Type
19
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
20
import CoAxiom( sfInteractTop, sfInteractInert )
21 22 23

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

41
import TcEvidence
42 43
import Outputable

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

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

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

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

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

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

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

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

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

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

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
125 126
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
127
set, unflatten and zonk the wanteds.  It passes the zonked wanteds
128 129 130 131 132 133
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
134
-}
135

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

149
solveSimpleWanteds :: Cts -> TcS WantedConstraints
150 151 152 153
-- NB: 'simples' may contain /derived/ equalities, floated
--     out from a nested implication. So don't discard deriveds!
solveSimpleWanteds simples
  = do { traceTcS "solveSimples {" (ppr simples)
154 155
       ; dflags <- getDynFlags
       ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
156 157 158 159
       ; traceTcS "solveSimples end }" $
             vcat [ ptext (sLit "iterations =") <+> ppr n
                  , ptext (sLit "residual =") <+> ppr wc ]
       ; return wc }
160
  where
161 162 163 164 165 166 167 168
    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 ]))
169

170 171
     | isEmptyBag (wc_simple wc)
     = return (n,wc)
172

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

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

181 182 183 184 185
          ; 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

186

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

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

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

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

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

-- | 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
256
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
257
-- main solver.
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
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
283 284 285
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
286
      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
Adam Gundry's avatar
Adam Gundry committed
287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
      _ -> 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
    }

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

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


371
type WorkItem = Ct
372
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
373

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

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

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

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

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

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

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

453
   If the work-item is Given,
454 455
   then the inert item must Given

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

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

474
-- Interaction result of  WorkItem <~> Ct
475

476
type StopNowFlag = Bool    -- True <=> stop after this interaction
477

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

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

494 495 496 497 498
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

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

514 515 516
  | 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
517

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

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

527 528 529 530 531 532
  | 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

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

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

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

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

573
     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
574

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

581
  * Constraints come from different levels (different_level_strategy)
582

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

587 588 589 590
      - 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.
591

592 593 594 595
        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
596
  * Constraints coming from the same level (i.e. same implication)
597 598 599 600 601 602 603 604

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

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

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

635 636 637 638 639
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
640
-}
641

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

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
650 651 652
        (matching_irreds, others)
          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
                         (inert_irreds inerts)
653 654 655 656
  , (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
657 658 659 660 661 662 663 664 665 666
       ; 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 }
667

668
  | otherwise
669
  = continueWith workItem
670

671
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
672

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

681
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
682
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
683 684 685 686 687 688
  | isWanted ev_w
  , Just ip_name      <- isCallStackCt workItem
  , 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.
689
  -- See Note [Overview of implicit CallStacks]
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
  = 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" }
707

708
  | Just ctev_i <- lookupInertDict inerts cls tys
709
  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
710 711 712 713 714 715
       ; 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
716
         else
717
            continueWith workItem }
718

719
  | cls == ipClass
720 721 722 723
  , isGiven ev_w
  = interactGivenIP inerts workItem

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

753
{-
754 755
**********************************************************************
*                                                                    *
756
                   Implicit parameters
757 758
*                                                                    *
**********************************************************************
759
-}
760

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

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

781

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

787 788
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
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 825 826 827 828 829 830 831 832
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.


833 834
**********************************************************************
*                                                                    *
835
                   interactFunEq
836 837
*                                                                    *
**********************************************************************
Austin Seipp's avatar
Austin Seipp committed
838
-}
839

840 841
interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- Try interacting the work item with the inert set
842
interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
843
                                         , cc_tyargs = args, cc_fsk = fsk })
844 845
  | Just (CFunEqCan { cc_ev = ev_i
                    , cc_fsk = fsk_i }) <- matching_inerts
846
  = if ev_i `canDischarge` ev
847 848 849 850 851 852
    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" }
853
    else  -- Rewrite inert using work-item
854
      ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i )
855 856 857 858 859 860 861 862 863
      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
864 865 866 867 868 869
  | otherwise   -- Try improvement
  = do { improveLocalFunEqs loc inerts tc args fsk
       ; continueWith workItem }
  where
    loc             = ctEvLoc ev
    funeqs          = inert_funeqs inerts
870
    matching_inerts = findFunEq funeqs tc args
871

Jan Stolarek's avatar
Jan Stolarek committed
872 873 874 875 876 877 878 879 880 881 882 883 884 885
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: " $
         vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns
              , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc
              , ptext (sLit "TvEqs:") <+> ppr tv_eqs ]
       ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
886
  | otherwise
Jan Stolarek's avatar
Jan Stolarek committed
887
  = return ()
888
  where
Jan Stolarek's avatar
Jan Stolarek committed
889 890 891 892 893 894 895 896 897 898
    tv_eqs        = inert_model inerts
    funeqs        = inert_funeqs inerts
    funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
    rhs           = lookupFlattenTyVar tv_eqs fsk

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

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

Jan Stolarek's avatar
Jan Stolarek committed
904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924
      | otherwise
      = []

    --------------------
    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk)
    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 })
      | rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk
      = [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
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
925 926
-- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
-- this is used only when dealing with a CFunEqCan
Jan Stolarek's avatar
Jan Stolarek committed
927 928 929 930
lookupFlattenTyVar model ftv
  = case lookupVarEnv model ftv of
      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
      _                                                   -> mkTyVarTy ftv
931

932 933
reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
           -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
934
           -> TcS ()
935 936 937 938
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
939
                         -- :: fsk2 ~ fsk1
940 941 942
             fsk_eq_pred = mkTcEqPredLikeEv solve_this
                             (mkTyVarTy fsk2) (mkTyVarTy fsk1)

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

946 947 948 949 950 951
  | 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) }
952

Austin Seipp's avatar
Austin Seipp committed
953
{-
Jan Stolarek's avatar
Jan Stolarek committed
954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991
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


992 993 994
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
995
solved cache (which is the default behaviour or xCtEvidence), because the interaction
996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023
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.


1024
Note [Efficient Orientation]
1025 1026
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
1027 1028
          (inert)  ci :: (F ty ~ xi_i)
          (work)   cw :: (F ty ~ xi_w)
1029 1030
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
1031
will (a) discharge 'cw'
1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045
     (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).

1046 1047
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1048
   ---- OLD COMMENT, NOW NOT NEEDED
Gabor Greif's avatar
Gabor Greif committed
1049
   ---- because we now allow multiple
1050
   ---- wanted FunEqs with the same head