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

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

#include "HsVersions.h"

10
import GhcPrelude
11 12
import BasicTypes ( SwapFlag(..), isSwapped,
                    infinity, IntWithInf, intGtLimit )
13
import TcCanonical
14
import TcFlatten
15
import TcUnify( canSolveByUnification )
16 17
import VarSet
import Type
18
import InstEnv( DFunInstType )
19
import CoAxiom( sfInteractTop, sfInteractInert )
20 21 22

import Var
import TcType
23
import PrelNames ( coercibleTyConKey,
24
                   heqTyConKey, eqTyConKey, ipClassKey )
25
import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
26 27
import Class
import TyCon
28
import FunDeps
29
import FamInst
30
import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap )
Jan Stolarek's avatar
Jan Stolarek committed
31
import FamInstEnv
32
import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
33

34
import TcEvidence
35 36
import Outputable

37 38
import TcRnTypes
import TcSMonad
39
import Bag
40
import MonadUtils ( concatMapM, foldlM )
41

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

46
import Control.Monad
47
import Maybes( isJust )
48
import Pair (Pair(..))
49
import Unique( hasKey )
50
import DynFlags
51
import Util
52
import qualified GHC.LanguageExtensions as LangExt
53

54 55 56
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe

Austin Seipp's avatar
Austin Seipp committed
57
{-
58
**********************************************************************
59
*                                                                    *
60 61 62 63
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

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

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

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

84
If in Step 1 no such element exists, we have exceeded our context-stack
85
depth and will simply fail.
86

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

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

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

132
solveSimpleGivens :: [Ct] -> TcS ()
133
solveSimpleGivens givens
134
  | null givens  -- Shortcut for common case
135
  = return ()
136
  | otherwise
137 138
  = do { traceTcS "solveSimpleGivens {" (ppr givens)
       ; go givens
139
       ; traceTcS "End solveSimpleGivens }" empty }
140
  where
141
    go givens = do { solveSimples (listToBag givens)
Adam Gundry's avatar
Adam Gundry committed
142
                   ; new_givens <- runTcPluginsGiven
143 144
                   ; when (notNull new_givens) $
                     go new_givens }
145

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

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

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

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

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

185

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

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

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

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

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
238
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
239 240
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
241 242 243 244 245 246 247
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
248
             insols                = pluginBadCts p
249
       ; updInertCans (removeInertCts solved_givens)
250
       ; updInertIrreds (\irreds -> extendCtsList irreds insols)
251
       ; 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
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
259
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
260 261 262 263 264 265 266 267 268 269 270 271 272
  | 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
273
             insols                                 = pluginBadCts p
274 275 276 277 278 279

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

       ; mapM_ setEv solved_wanted
       ; return ( notNull (pluginNewCts p)
280 281 282 283
                , WC { wc_simple = listToBag new_wanted       `andCts`
                                   listToBag unsolved_wanted  `andCts`
                                   listToBag unsolved_derived `andCts`
                                   listToBag insols
284
                     , 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
  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
357 358
    eqCt c c' = ctFlavour c == ctFlavour c'
             && ctPred c `tcEqType` ctPred c'
Adam Gundry's avatar
Adam Gundry committed
359 360 361 362 363 364 365 366 367 368 369

    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)


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

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

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

391
       ; case final_res of
392
           Stop ev s       -> do { traceFireTcS ev s
393
                                 ; traceTcS "End solver pipeline (discharged) }" empty
394
                                 ; return () }
395 396
           ContinueWith ct -> do { addInertCan ct
                                 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
397
                                 ; traceTcS "End solver pipeline (kept as inert) }" $
398
                                            (text "final_item =" <+> ppr 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
    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
460
Now, c3 does not interact with 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
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
477 478
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
479

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

492
data InteractResult
493 494 495
   = KeepInert   -- Keep the inert item, and solve the work item from it
                 -- (if the latter is Wanted; just discard it if not)
   | KeepWork    -- Keep the work item, and solve the intert item from it
496

497
instance Outputable InteractResult where
498 499
  ppr KeepInert = text "keep inert"
  ppr KeepWork  = text "keep work-item"
500 501 502

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
503 504 505 506 507 508 509 510
                     -> TcS InteractResult
-- Precondition:
-- * inert and work item represent evidence for the /same/ predicate
--
-- We can always solve one from the other: even if both are wanted,
-- although we don't rewrite wanteds with wanteds, we can combine
-- two wanteds into one by solving one from the other

511
solveOneFromTheOther ev_i ev_w
512
  | isDerived ev_w         -- Work item is Derived; just discard it
513
  = return KeepInert
514

515 516 517
  | isDerived ev_i     -- The inert item is Derived, we can just throw it away,
  = return KeepWork    -- The ev_w is inert wrt earlier inert-set items,
                       -- so it's safe to continue on from this point
518

519 520
  | CtWanted { ctev_loc = loc_w } <- ev_w
  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
521 522 523
  = -- inert must be Given
    do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
       ; return KeepWork }
524

525
  | CtWanted {} <- ev_w
526
       -- Inert is Given or Wanted
527 528 529
  = return KeepInert

  -- From here on the work-item is Given
530

531
  | CtWanted { ctev_loc = loc_i } <- ev_i
532
  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
533
  = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
534 535 536
       ; return KeepInert }      -- Just discard the un-usable Given
                                 -- This never actually happens because
                                 -- Givens get processed first
537

538 539
  | CtWanted {} <- ev_i
  = return KeepWork
540

541
  -- From here on both are Given
542
  -- See Note [Replacement vs keeping]
543

544
  | lvl_i == lvl_w
545 546
  = do { ev_binds_var <- getTcEvBindsVar
       ; binds <- getTcEvBindsMap ev_binds_var
547
       ; return (same_level_strategy binds) }
548

549
  | otherwise   -- Both are Given, levels differ
550
  = return different_level_strategy
551
  where
552 553 554 555 556
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
557 558
     ev_id_i = ctEvEvId ev_i
     ev_id_w = ctEvEvId ev_w
559

560
     different_level_strategy  -- Both Given
561 562 563
       | isIPPred pred, lvl_w > lvl_i = KeepWork
       | lvl_w < lvl_i                = KeepWork
       | otherwise                    = KeepInert
564

565
     same_level_strategy binds -- Both Given
566 567
       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
       = case ctLocOrigin loc_w of
568 569 570
            GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
                                     | otherwise -> KeepInert
            _                                    -> KeepWork
571 572

       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
573
       = KeepInert
574

575 576 577
       | has_binding binds ev_id_w
       , not (has_binding binds ev_id_i)
       , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
578
       = KeepWork
579

580 581
       | otherwise
       = KeepInert
582

583
     has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
584

Austin Seipp's avatar
Austin Seipp committed
585
{-
586 587 588
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
589
we keep?  More subtle than you might think!
590

591
  * Constraints come from different levels (different_level_strategy)
592

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

597 598 599 600
      - 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.
601

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

Gabor Greif's avatar
Gabor Greif committed
606
  * Constraints coming from the same level (i.e. same implication)
607

608 609 610 611
       (a) 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
612

613 614 615 616 617
       (b) Keep the one that has a non-trivial evidence binding.
              Example:  f :: (Eq a, Ord a) => blah
              then we may find [G] d3 :: Eq a
                               [G] d2 :: Eq a
                with bindings  d3 = sc_sel (d1::Ord a)
618 619
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635
            Why? See Note [Tracking redundant constraints] in TcSimplify again.

       (c) But don't do (b) if the evidence binding depends transitively on the
           one without a binding.  Example (with RecursiveSuperClasses)
              class C a => D a
              class D a => C a
           Inert:     d1 :: C a, d2 :: D a
           Binds:     d3 = sc_sel d2, d2 = sc_sel d1
           Work item: d3 :: C a
           Then it'd be ridiculous to replace d1 with d3 in the inert set!
           Hence the findNeedEvVars test.  See Trac #14774.

  * Finally, when there is still a choice, use KeepInert rather than
    KeepWork, for two reasons:
      - to avoid unnecessary munging of the inert set.
      - to cut off superclass loops; see Note [Superclass loops] in TcCanonical
636 637

Doing the depth-check for implicit parameters, rather than making the work item
638
always override, is important.  Consider
639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656

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

657 658 659 660 661
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
662 663 664 665 666 667 668 669 670 671 672 673

Note [Multiple matching irreds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You might think that it's impossible to have multiple irreds all match the
work item; after all, interactIrred looks for matches and solves one from the
other. However, note that interacting insoluble, non-droppable irreds does not
do this matching. We thus might end up with several insoluble, non-droppable,
matching irreds in the inert set. When another irred comes along that we have
not yet labeled insoluble, we can find multiple matches. These multiple matches
cause no harm, but it would be wrong to ASSERT that they aren't there (as we
once had done). This problem can be tickled by typecheck/should_compile/holes.

Austin Seipp's avatar
Austin Seipp committed
674
-}
675

676 677 678 679
-- 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)
680
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
681

682 683 684 685 686
interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
  | insoluble  -- For insolubles, don't allow the constaint to be dropped
               -- which can happen with solveOneFromTheOther, so that
               -- we get distinct error messages with -fdefer-type-errors
               -- See Note [Do not add duplicate derived insolubles]
687
  , not (isDroppableCt workItem)
688 689 690
  = continueWith workItem

  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
691 692
  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
        -- See Note [Multiple matching irreds]
693
  , let ev_i = ctEvidence ct_i
694
  = do { what_next <- solveOneFromTheOther ev_i ev_w
695 696 697 698 699 700 701
       ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
       ; case what_next of
            KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
                            ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
            KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
                            ; updInertIrreds (\_ -> others)
                            ; continueWith workItem } }
702

703
  | otherwise
704
  = continueWith workItem
705

706
  where
707
    swap_me :: SwapFlag -> CtEvidence -> EvTerm
708 709
    swap_me swap ev
      = case swap of
710 711
           NotSwapped -> ctEvTerm ev
           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
712

713
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
714

715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805
findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
findMatchingIrreds irreds ev
  | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
    -- See Note [Solving irreducible equalities]
  = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
  | otherwise
  = partitionBagWith match_non_eq irreds
  where
    pred = ctEvPred ev
    match_non_eq ct
      | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
      | otherwise                            = Right ct

    match_eq eq_rel1 lty1 rty1 ct
      | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
      , eq_rel1 == eq_rel2
      , Just swap <- match_eq_help lty1 rty1 lty2 rty2
      = Left (ct, swap)
      | otherwise
      = Right ct

    match_eq_help lty1 rty1 lty2 rty2
      | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
      = Just NotSwapped
      | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
      = Just IsSwapped
      | otherwise
      = Nothing

{- Note [Solving irreducible equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #14333)
  [G] a b ~R# c d
  [W] c d ~R# a b
Clearly we should be able to solve this! Even though the constraints are
not decomposable. We solve this when looking up the work-item in the
irreducible constraints to look for an identical one.  When doing this
lookup, findMatchingIrreds spots the equality case, and matches either
way around. It has to return a swap-flag so we can generate evidence
that is the right way round too.

Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we *must* add an insoluble (Int ~ Bool) even if there is
one such there already, because they may come from distinct call
sites.  Not only do we want an error message for each, but with
-fdefer-type-errors we must generate evidence for each.  But for
*derived* insolubles, we only want to report each one once.  Why?

(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
    equality many times, as the original constraint is successively rewritten.

(b) Ditto the successive iterations of the main solver itself, as it traverses
    the constraint tree. See example below.

Also for *given* insolubles we may get repeated errors, as we
repeatedly traverse the constraint tree.  These are relatively rare
anyway, so removing duplicates seems ok.  (Alternatively we could take
the SrcLoc into account.)

Note that the test does not need to be particularly efficient because
it is only used if the program has a type error anyway.

Example of (b): assume a top-level class and instance declaration:

  class D a b | a -> b
  instance D [a] [a]

Assume we have started with an implication:

  forall c. Eq c => { wc_simple = D [c] c [W] }

which we have simplified to:

  forall c. Eq c => { wc_simple = D [c] c [W]
                                  (c ~ [c]) [D] }

For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
dropDerivedWC, then we will end up trying to solve the following
constraints the second time:

  (D [c] c) [W]
  (c ~ [c]) [D]

which will result in two Deriveds to end up in the insoluble set:

  wc_simple   = D [c] c [W]
               (c ~ [c]) [D], (c ~ [c]) [D]
-}

Austin Seipp's avatar
Austin Seipp committed
806
{-
807 808 809 810 811
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
812

813 814
Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837
When we interact a [W] constraint with a [G] constraint that solves it, there is
a possibility that we could produce better code if instead we solved from a
top-level instance declaration (See #12791, #5835). For example:

    class M a b where m :: a -> b

    type C a b = (Num a, M a b)

    f :: C Int b => b -> Int -> Int
    f _ x = x + 1

The body of `f` requires a [W] `Num Int` instance. We could solve this
constraint from the givens because we have `C Int b` and that provides us a
solution for `Num Int`. This would let us produce core like the following
(with -O2):

    f :: forall b. C Int b => b -> Int -> Int
    f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) ->
        + @ Int
          (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%))
          eta1
          A.f1

838 839
This is bad! We could do /much/ better if we solved [W] `Num Int` directly
from the instance that we have in scope:
840 841 842 843 844

    f :: forall b. C Int b => b -> Int -> Int
    f = \ (@ b) _ _ (x :: Int) ->
        case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }

845 846 847 848 849 850 851 852 853 854
** NB: It is important to emphasize that all this is purely an optimization:
** exactly the same programs should typecheck with or without this
** procedure.

Solving fully
~~~~~~~~~~~~~
There is a reason why the solver does not simply try to solve such
constraints with top-level instances. If the solver finds a relevant
instance declaration in scope, that instance may require a context
that can't be solved for. A good example of this is:
855 856 857 858 859 860 861

    f :: Ord [a] => ...
    f x = ..Need Eq [a]...

If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
be left with the obligation to solve the constraint Eq a, which we cannot. So we
must be conservative in our attempt to use an instance declaration to solve the
862 863 864 865 866 867 868 869
[W] constraint we're interested in.

Our rule is that we try to solve all of the instance's subgoals
recursively all at once. Precisely: We only attempt to solve
constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci
are themselves class constraints of the form `C1', ... Cm' => C' t1'
... tn'` and we only succeed if the entire tree of constraints is
solvable from instances.
870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904

An example that succeeds:

    class Eq a => C a b | b -> a where
      m :: b -> a

    f :: C [Int] b => b -> Bool
    f x = m x == []

We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This
produces the following core:

    f :: forall b. C [Int] b => b -> Bool
    f = \ (@ b) ($dC :: C [Int] b) (x :: b) ->
        GHC.Classes.$fEq[]_$s$c==
          (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int)

An example that fails:

    class Eq a => C a b | b -> a where
      m :: b -> a

    f :: C [a] b => b -> Bool
    f x = m x == []

Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:

    f :: forall a b. C [a] b => b -> Bool
    f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) ->
        ==
          @ [a]
          (A.$p1C @ [a] @ b $dC)
          (m @ [a] @ b $dC eta)
          (GHC.Types.[] @ a)

905 906
Note [Shortcut solving: type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907 908 909 910 911 912 913 914 915 916 917
Suppose we have (Trac #13943)
  class Take (n :: Nat) where ...
  instance {-# OVERLAPPING #-}                    Take 0 where ..
  instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..

And we have [W] Take 3.  That only matches one instance so we get
[W] Take (3-1).  Really we should now flatten to reduce the (3-1) to 2, and
so on -- but that is reproducing yet more of the solver.  Sigh.  For now,
we just give up (remember all this is just an optimisation).

But we must not just naively try to lookup (Take (3-1)) in the
918
InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a
919 920 921 922
unique match on the (Take n) instance.  That leads immediately to an
infinite loop.  Hence the check that 'preds' have no type families
(isTyFamFree).

923 924 925 926 927 928 929 930 931 932 933 934 935 936
Note [Shortcut solving: overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
  instance {-# OVERLAPPABLE #-} C a where ...
and we are typechecking
  f :: C a => a -> a
  f = e  -- Gives rise to [W] C a

We don't want to solve the wanted constraint with the overlappable
instance; rather we want to use the supplied (C a)! That was the whole
point of it being overlappable!  Trac #14434 wwas an example.

Note [Shortcut solving: incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 938
This optimization relies on coherence of dictionaries to be correct. When we
cannot assume coherence because of IncoherentInstances then this optimization
Gabor Greif's avatar
Gabor Greif committed
939
can change the behavior of the user's code.
940 941 942 943 944 945 946 947 948 949 950 951 952 953 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 992 993 994

The following four modules produce a program whose output would change depending
on whether we apply this optimization when IncoherentInstances is in effect:

#########
    {-# LANGUAGE MultiParamTypeClasses #-}
    module A where

    class A a where
      int :: a -> Int

    class A a => C a b where
      m :: b -> a -> a

#########
    {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
    module B where

    import A

    instance A a where
      int _ = 1

    instance C a [b] where
      m _ = id

#########
    {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
    {-# LANGUAGE IncoherentInstances #-}
    module C where

    import A

    instance A Int where
      int _ = 2

    instance C Int [Int] where
      m _ = id

    intC :: C Int a => a -> Int -> Int
    intC _ x = int x

#########
    module Main where

    import A
    import B
    import C

    main :: IO ()
    main = print (intC [] (0::Int))

The output of `main` if we avoid the optimization under the effect of
IncoherentInstances is `1`. If we were to do the optimization, the output of
`main` would be `2`.
995 996 997 998

Note [Shortcut try_solve_from_instance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The workhorse of the short-cut solver is
999
    try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026
                            -> CtEvidence       -- Solve this
                            -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
Note that:

* The CtEvidence is teh goal to be solved

* The MaybeT anages early failure if we find a subgoal that
  cannot be solved from instances.

* The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional
  state that allows try_solve_from_instance to augmennt the evidence
  bindings and inert_solved_dicts as it goes.

  If it succeeds, we commit all these bindings and solved dicts to the
  main TcS InertSet.  If not, we abandon it all entirely.

Passing along the solved_dicts important for two reasons:

* We need to be able to handle recursive super classes. The
  solved_dicts state  ensures that we remember what we have already
  tried to solve to avoid looping.

* As Trac #15164 showed, it can be important to exploit sharing between
  goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H;
  and to solve G2 we may need H. If we don't spot this sharing we may
  solve H twice; and if this pattern repeats we may get exponentially bad
  behaviour.
Austin Seipp's avatar
Austin Seipp committed
1027
-}
1028

1029
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1030
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
1031
  | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
1032
  = -- There is a matching dictionary in the inert set
1033 1034
    do { -- First to try to solve it /completely/ from top level instances
         -- See Note [Shortcut solving]
1035
         dflags <- getDynFlags
1036 1037 1038 1039 1040
       ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
       ; if short_cut_worked
         then stopWith ev_w "interactDict/solved from instance"
         else

1041 1042
    do { -- Ths short-cut solver didn't fire, so we
         -- solve ev_w from the matching inert ev_i we found
1043 1044 1045
         what_next <- solveOneFromTheOther ev_i ev_w
       ; traceTcS "lookupInertDict" (ppr what_next)
       ; case what_next of
1046
           KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
1047
                           ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
1048
           KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
1049 1050
                           ; updInertDicts $ \ ds -> delDict ds cls tys
                           ; continueWith workItem } } }
1051

1052
  | cls `hasKey` ipClassKey
1053 1054 1055 1056
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
1057 1058 1059 1060 1061
  = do { addFunDepWork inerts ev_w cls
       ; continueWith workItem  }

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

1062 1063 1064 1065
-- See Note [Shortcut solving]
shortCutSolver :: DynFlags
               -> CtEvidence -- Work item
               -> CtEvidence -- Inert we want to try to replace
1066
               -> TcS Bool   -- True <=> success
1067
shortCutSolver dflags ev_w ev_i
1068
  | isWanted ev_w
1069
 && isGiven ev_i
1070 1071 1072 1073
 -- We are about to solve a [W] constraint from a [G] constraint. We take
 -- a moment to see if we can get a better solution using an instance.
 -- Note that we only do this for the sake of performance. Exactly the same
 -- programs should typecheck regardless of whether we take this step or
1074 1075
 -- not. See Note [Shortcut solving]

1076 1077 1078 1079
 && not (xopt LangExt.IncoherentInstances dflags)
 -- If IncoherentInstances is on then we cannot rely on coherence of proofs
 -- in order to justify this optimization: The proof provided by the
 -- [G] constraint's superclass may be different from the top-level proof.
1080
 -- See Note [Shortcut solving: incoherence]
1081

1082 1083
 && gopt Opt_SolveConstantDicts dflags
 -- Enabled by the -fsolve-constant-dicts flag
1084
  = do { ev_binds_var <- getTcEvBindsVar
1085
       ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
1086 1087
                     getTcEvBindsMap ev_binds_var
       ; solved_dicts <- getSolvedDicts
1088

1089
       ; mb_stuff <- runMaybeT $ try_solve_from_instance
1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100
                                   (ev_binds, solved_dicts) ev_w

       ; case mb_stuff of
           Nothing -> return False
           Just (ev_binds', solved_dicts')
              -> do { setTcEvBindsMap ev_binds_var ev_binds'
                    ; setSolvedDicts solved_dicts'
                    ; return True } }

  | otherwise
  = return False
1101 1102 1103 1104 1105 1106
  where
    -- This `CtLoc` is used only to check the well-staged condition of any
    -- candidate DFun. Our subgoals all have the same stage as our root
    -- [W] constraint so it is safe to use this while solving them.
    loc_w = ctEvLoc ev_w

1107
    try_solve_from_instance   -- See Note [Shortcut try_solve_from_instance]
1108
      :: (EvBindMap, DictMap CtEvidence) -> CtEvidence
1109
      -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
1110
    try_solve_from_instance (ev_binds, solved_dicts) ev
1111
      | let pred = ctEvPred ev
1112
            loc  = ctEvLoc  ev
1113
      , ClassPred cls tys <- classifyPredType pred
1114
      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
1115
           ; case inst_res of
1116 1117 1118 1119
               OneInst { cir_new_theta = preds
                       , cir_mk_ev     = mk_ev
                       , cir_what      = what }
                 | safeOverlap what
1120
                 , all isTyFamFree preds  -- Note [Shortcut solving: type families]
1121 1122 1123 1124 1125 1126
                 -> do { let solved_dicts' = addDict solved_dicts cls tys ev
                             -- solved_dicts': it is important that we add our goal
                             -- to the cache before we solve! Otherwise we may end
                             -- up in a loop while solving recursive dictionaries.

                       ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
1127
                       ; loc' <- lift $ checkInstanceOK loc what pred
1128

1129
                       ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
1130 1131 1132
                                  -- Emit work for subgoals but use our local cache
                                  -- so we can solve recursive dictionaries.

1133 1134 1135 1136
                       ; let ev_tm     = mk_ev (map getEvExpr evc_vs)
                             ev_binds' = extendEvBinds ev_binds $
                                         mkWantedEvBind (ctEvEvId ev) ev_tm

1137
                       ; foldlM try_solve_from_instance
1138 1139 1140
                                (ev_binds', solved_dicts')
                                (freshGoals evc_vs) }

1141
               _ -> mzero }
1142 1143
      | otherwise = mzero

1144 1145 1146 1147

    -- Use a local cache of solved dicts while emitting EvVars for new work
    -- We bail out of the entire computation if we need to emit an EvVar for
    -- a subgoal that isn't a ClassPred.
1148 1149
    new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
    new_wanted_cached loc cache pty
1150 1151 1152
      | ClassPred cls tys <- classifyPredType pty
      = lift $ case findDict cache loc_w cls tys of
          Just ctev -> return $ Cached (ctEvExpr ctev)
1153
          Nothing   -> Fresh <$> newWantedNC loc pty
1154 1155
      | otherwise = mzero

1156 1157 1158
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
-- Add derived constraints from type-class functional dependencies.
addFunDepWork inerts work_ev cls
1159
  | isImprovable work_ev
1160
  = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
1161 1162
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
1163 1164
               -- Importantly we don't throw workitem back in the
               -- worklist because this can cause loops (see #5236)
1165 1166
  | otherwise
  = return ()
1167 1168 1169
  where
    work_pred = ctEvPred work_ev
    work_loc  = ctEvLoc work_ev
1170

1171
    add_fds inert_ct
1172
      | isImprovable inert_ev
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1173 1174 1175 1176 1177 1178 1179
      = do { traceTcS "addFunDepWork" (vcat
                [ ppr work_ev
                , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
                , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
                , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) ;

        emitFunDepDeriveds $
1180 1181 1182 1183 1184
        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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1185
        }
1186 1187
      | otherwise
      = return ()
1188
      where
1189 1190 1191
        inert_ev   = ctEvidence inert_ct
        inert_pred = ctEvPred inert_ev
        inert_loc  = ctEvLoc inert_ev
1192 1193 1194
        derived_loc = work_loc { ctl_depth  = ctl_depth work_loc `maxSubGoalDepth`
                                              ctl_depth inert_loc
                               , ctl_origin = FunDepOrigin1 work_pred  work_loc