TcInteract.hs 118 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
11
import GhcPrelude

12
13
import BasicTypes ( SwapFlag(..), isSwapped,
                    infinity, IntWithInf, intGtLimit )
14
import TcCanonical
15
import TcFlatten
16
import TcUnify( canSolveByUnification )
17
18
import VarSet
import Type
Ben Gamari's avatar
Ben Gamari committed
19
import Kind( isConstraintKind )
20
21
import InstEnv( DFunInstType, lookupInstEnv
              , instanceDFunId, isOverlappable )
22
import CoAxiom( sfInteractTop, sfInteractInert )
23

24
25
import TcMType (newMetaTyVars)

26
27
import Var
import TcType
28
import Name
29
import RdrName ( lookupGRE_FieldLabel )
30
import PrelNames ( knownNatClassName, knownSymbolClassName,
31
                   typeableClassName,
32
                   coercibleTyConKey,
33
                   hasFieldClassName,
34
                   heqTyConKey, eqTyConKey, ipClassKey )
35
import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
Ben Gamari's avatar
Ben Gamari committed
36
                    coercibleDataCon, constraintKindTyCon )
37
import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
38
import Id( idType, isNaughtyRecordSelector )
39
import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
40
41
import Class
import TyCon
42
import DataCon( dataConWrapId )
43
import FieldLabel
44
import FunDeps
45
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
46
47
import FamInstEnv
import Unify ( tcUnifyTyWithTFs )
48

49
import TcEvidence
50
import MkCore ( mkStringExprFS, mkNaturalExpr )
51
52
import Outputable

53
54
import TcRnTypes
import TcSMonad
55
import Bag
Jan Stolarek's avatar
Jan Stolarek committed
56
import MonadUtils ( concatMapM )
57

Adam Gundry's avatar
Adam Gundry committed
58
import Data.List( partition, foldl', deleteFirstsBy )
59
import SrcLoc
dimitris's avatar
dimitris committed
60
61
import VarEnv

62
import Control.Monad
63
import Maybes( isJust )
64
import Pair (Pair(..))
65
import Unique( hasKey )
66
import DynFlags
67
import Util
68
import qualified GHC.LanguageExtensions as LangExt
69

70
71
72
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe

Austin Seipp's avatar
Austin Seipp committed
73
{-
74
**********************************************************************
75
*                                                                    *
76
77
78
79
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

80
Note [Basic Simplifier Plan]
81
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
82
1. Pick an element from the WorkList if there exists one with depth
83
   less than our context-stack depth.
84

85
2. Run it down the 'stage' pipeline. Stages are:
86
87
88
89
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level intreactions
90
   Each stage returns a StopOrContinue and may have sideffected
91
   the inerts or worklist.
92
93
94
95
96
97

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

100
If in Step 1 no such element exists, we have exceeded our context-stack
101
depth and will simply fail.
102

103
Note [Unflatten after solving the simple wanteds]
104
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
105
We unflatten after solving the wc_simples of an implication, and before attempting
106
107
to float. This means that

108
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
Jan Stolarek's avatar
Jan Stolarek committed
109
   need to worry about them across successive passes over the constraint tree.
110
111
112
113
114
115
116
117
118
119
120
121
122
123
   (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
124
   will do exactly that after solving the simple constraints and before
125
126
127
128
129
130
131
132
133
   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
134
135
136

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137
138
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
139
set, unflatten and zonk the wanteds.  It passes the zonked wanteds
140
141
142
143
144
145
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
146
-}
147

148
solveSimpleGivens :: [Ct] -> TcS ()
149
solveSimpleGivens givens
150
  | null givens  -- Shortcut for common case
151
  = return ()
152
  | otherwise
153
154
  = do { traceTcS "solveSimpleGivens {" (ppr givens)
       ; go givens
155
       ; traceTcS "End solveSimpleGivens }" empty }
156
  where
157
    go givens = do { solveSimples (listToBag givens)
Adam Gundry's avatar
Adam Gundry committed
158
                   ; new_givens <- runTcPluginsGiven
159
160
                   ; when (notNull new_givens) $
                     go new_givens }
161

162
solveSimpleWanteds :: Cts -> TcS WantedConstraints
163
164
-- NB: 'simples' may contain /derived/ equalities, floated
--     out from a nested implication. So don't discard deriveds!
165
-- The result is not necessarily zonked
166
solveSimpleWanteds simples
167
  = do { traceTcS "solveSimpleWanteds {" (ppr simples)
168
169
       ; dflags <- getDynFlags
       ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
170
       ; traceTcS "solveSimpleWanteds end }" $
171
172
             vcat [ text "iterations =" <+> ppr n
                  , text "residual =" <+> ppr wc ]
173
       ; return wc }
174
  where
175
176
177
    go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
    go n limit wc
      | n `intGtLimit` limit
178
179
      = failTcS (hang (text "solveSimpleWanteds: too many iterations"
                       <+> parens (text "limit =" <+> ppr limit))
180
                    2 (vcat [ text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
181
182
                            , text "Simples =" <+> ppr simples
                            , text "WC ="      <+> ppr wc ]))
183

184
185
     | isEmptyBag (wc_simple wc)
     = return (n,wc)
186

187
188
     | otherwise
     = do { -- Solve
189
            (unif_count, wc1) <- solve_simple_wanteds wc
190
191

            -- Run plugins
192
          ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
193
194
             -- See Note [Running plugins on unflattened wanteds]

195
196
          ; if unif_count == 0 && not rerun_plugin
            then return (n, wc2)             -- Done
197
198
            else do { traceTcS "solveSimple going round again:" $
                      ppr unif_count $$ ppr rerun_plugin
199
200
                    ; go (n+1) limit wc2 } }      -- Loop

201

202
solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
203
204
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
205
-- The result is not necessarily zonked
206
solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
207
208
  = nestTcS $
    do { solveSimples simples1
209
       ; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
210
       ; (unif_count, unflattened_eqs) <- reportUnifications $
211
                                          unflattenWanteds tv_eqs fun_eqs
212
            -- See Note [Unflatten after solving the simple wanteds]
213
       ; return ( unif_count
214
215
216
                , WC { wc_simple = others `andCts` unflattened_eqs
                     , wc_impl   = implics1 `unionBags` implics2 }) }

217
218
{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
219
220
Solving a bunch of simple constraints is done in a loop,
(the 'go' loop of 'solveSimpleWanteds'):
221
222
223
224
225
226
227
228
229
  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]
230
-}
231
232
233

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

239
240
solveSimples cts
  = {-# SCC "solveSimples" #-}
241
242
    do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
       ; solve_loop }
243
  where
244
    solve_loop
245
      = {-# SCC "solve_loop" #-}
246
        do { sel <- selectNextWorkItem
247
           ; case sel of
248
249
250
              Nothing -> return ()
              Just ct -> do { runSolverPipeline thePipeline ct
                            ; solve_loop } }
Adam Gundry's avatar
Adam Gundry committed
251
252
253

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
254
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
255
256
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
257
258
259
260
261
262
263
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
264
             insols                = pluginBadCts p
265
       ; updInertCans (removeInertCts solved_givens)
266
       ; updInertIrreds (\irreds -> extendCtsList irreds insols)
267
       ; return (pluginNewCts p) } } }
Adam Gundry's avatar
Adam Gundry committed
268
269
270
271

-- | 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
272
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
273
-- main solver.
274
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
275
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
276
277
278
279
280
281
282
283
284
285
286
287
288
  | 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
289
             insols                                 = pluginBadCts p
290
291
292
293
294
295

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

       ; mapM_ setEv solved_wanted
       ; return ( notNull (pluginNewCts p)
296
297
298
299
                , WC { wc_simple = listToBag new_wanted       `andCts`
                                   listToBag unsolved_wanted  `andCts`
                                   listToBag unsolved_derived `andCts`
                                   listToBag insols
300
                     , wc_impl   = implics1 } ) } }
Adam Gundry's avatar
Adam Gundry committed
301
302
303
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
304
      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
Adam Gundry's avatar
Adam Gundry committed
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
      _ -> 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
    }

327
328
329
getTcPlugins :: TcS [TcPluginSolver]
getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }

Adam Gundry's avatar
Adam Gundry committed
330
331
332
333
334
335
336
337
338
339
340
341
342
-- | 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.
343
344
345
runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPlugins plugins all_cts
  = foldM do_plugin initialProgress plugins
Adam Gundry's avatar
Adam Gundry committed
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
  where
    do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
    do_plugin p solver = do
        result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
        return $ progress p result

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

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

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

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

    eqCt :: Ct -> Ct -> Bool
373
374
    eqCt c c' = ctFlavour c == ctFlavour c'
             && ctPred c `tcEqType` ctPred c'
Adam Gundry's avatar
Adam Gundry committed
375
376
377
378
379
380
381
382
383
384
385

    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)


386
type WorkItem = Ct
387
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
388

389
390
391
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
                  -> WorkItem                   -- The work item
                  -> TcS ()
392
-- Run this item down the pipeline, leaving behind new work and inerts
393
runSolverPipeline pipeline workItem
394
  = do { wl <- getWorkList
395
       ; inerts <- getTcSInerts
396
       ; tclevel <- getTcLevel
397
       ; traceTcS "----------------------------- " empty
398
       ; traceTcS "Start solver pipeline {" $
399
400
                  vcat [ text "tclevel =" <+> ppr tclevel
                       , text "work item =" <+> ppr workItem
401
                       , text "inerts =" <+> ppr inerts
402
                       , text "rest of worklist =" <+> ppr wl ]
403

404
       ; bumpStepCountTcS    -- One step for each constraint processed
405
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
406

407
       ; case final_res of
408
           Stop ev s       -> do { traceFireTcS ev s
409
                                 ; traceTcS "End solver pipeline (discharged) }" empty
410
                                 ; return () }
411
412
           ContinueWith ct -> do { addInertCan ct
                                 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
413
                                 ; traceTcS "End solver pipeline (kept as inert) }" $
414
                                            (text "final_item =" <+> ppr ct) }
415
       }
Austin Seipp's avatar
Austin Seipp committed
416
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
417
418
419
                     -> TcS (StopOrContinue Ct)
        run_pipeline [] res        = return res
        run_pipeline _ (Stop ev s) = return (Stop ev s)
420
421
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
422
423
                          (text "workitem   = " <+> ppr ct)
               ; res <- stg ct
424
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
425
               ; run_pipeline stgs res }
426

Austin Seipp's avatar
Austin Seipp committed
427
{-
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
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
450
-}
451

452
thePipeline :: [(String,SimplifierStage)]
453
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
454
455
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
456

Austin Seipp's avatar
Austin Seipp committed
457
{-
458
*********************************************************************************
459
*                                                                               *
460
461
462
463
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

464
465
466
467
468
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

469
   If the work-item is Given,
470
471
   then the inert item must Given

472
But this isn't quite true.  Suppose we have,
473
474
475
    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
476
Now, c3 does not interact with the given c1, so when we spontaneously
477
solve c3, we must re-react it with the inert set.  So we can attempt a
478
479
480
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
481
   If the work-item is Given,
482
483
484
   AND there is a reaction
   then the inert item must Given
or, equivalently,
485
   If the work-item is Given,
486
487
   and the inert item is Wanted/Derived
   then there is no reaction
Austin Seipp's avatar
Austin Seipp committed
488
-}
489

490
-- Interaction result of  WorkItem <~> Ct
491

492
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
493
494
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
495

496
interactWithInertsStage wi
497
498
  = do { inerts <- getTcSInerts
       ; let ics = inert_cans inerts
499
       ; case wi of
500
501
502
503
             CTyEqCan  {} -> interactTyVarEq ics wi
             CFunEqCan {} -> interactFunEq   ics wi
             CIrredCan {} -> interactIrred   ics wi
             CDictCan  {} -> interactDict    ics wi
504
             _ -> pprPanic "interactWithInerts" (ppr wi) }
505
506
                -- CHoleCan are put straight into inert_frozen, so never get here
                -- CNonCanonical have been canonicalised
507

508
data InteractResult
509
510
511
   = 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
512

513
instance Outputable InteractResult where
514
515
  ppr KeepInert = text "keep inert"
  ppr KeepWork  = text "keep work-item"
516
517
518

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
519
520
521
522
523
524
525
526
                     -> 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

527
solveOneFromTheOther ev_i ev_w
528
  | isDerived ev_w         -- Work item is Derived; just discard it
529
  = return KeepInert
530

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

535
536
  | CtWanted { ctev_loc = loc_w } <- ev_w
  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
537
538
539
  = -- inert must be Given
    do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
       ; return KeepWork }
540

541
  | CtWanted {} <- ev_w
542
       -- Inert is Given or Wanted
543
544
545
  = return KeepInert

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

547
  | CtWanted { ctev_loc = loc_i } <- ev_i
548
  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
549
  = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
550
551
552
       ; return KeepInert }      -- Just discard the un-usable Given
                                 -- This never actually happens because
                                 -- Givens get processed first
553

554
555
  | CtWanted {} <- ev_i
  = return KeepWork
556

557
  -- From here on both are Given
558
  -- See Note [Replacement vs keeping]
559

560
  | lvl_i == lvl_w
Simon Peyton Jones's avatar
Simon Peyton Jones committed
561
562
  = do { ev_binds_var <- getTcEvBindsVar
       ; binds <- getTcEvBindsMap ev_binds_var
563
       ; return (same_level_strategy binds) }
564

565
  | otherwise   -- Both are Given, levels differ
566
  = return (different_level_strategy)
567
  where
568
569
570
571
572
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
573
574
     ev_id_i = ctEvEvId ev_i
     ev_id_w = ctEvEvId ev_w
575

576
     different_level_strategy
577
578
579
       | isIPPred pred, lvl_w > lvl_i = KeepWork
       | lvl_w < lvl_i                = KeepWork
       | otherwise                    = KeepInert
580
581
582
583

     same_level_strategy binds        -- Both Given
       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
       = case ctLocOrigin loc_w of
584
585
586
            GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
                                     | otherwise -> KeepInert
            _                                    -> KeepWork
587
588

       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
589
       = KeepInert
590

591
592
593
       | has_binding binds ev_id_w
       , not (has_binding binds ev_id_i)
       , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
594
       = KeepWork
595

596
597
       | otherwise
       = KeepInert
598

599
     has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
600

Austin Seipp's avatar
Austin Seipp committed
601
{-
602
603
604
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
605
we keep?  More subtle than you might think!
606

607
  * Constraints come from different levels (different_level_strategy)
608

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

613
614
615
616
      - 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.
617

618
619
620
621
        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
622
  * Constraints coming from the same level (i.e. same implication)
623

624
625
626
627
       (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
628

629
630
631
632
633
       (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)
634
635
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
            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
652
653

Doing the depth-check for implicit parameters, rather than making the work item
Gabor Greif's avatar
Gabor Greif committed
654
always override, is important.  Consider
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672

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

673
674
675
676
677
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
678
679
680
681
682
683
684
685
686
687
688
689

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
690
-}
691

692
693
694
695
-- 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)
696
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
697

698
699
700
701
702
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]
703
  , not (isDroppableCt workItem)
704
705
706
  = continueWith workItem

  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
707
708
  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
        -- See Note [Multiple matching irreds]
709
  , let ev_i = ctEvidence ct_i
710
  = do { what_next <- solveOneFromTheOther ev_i ev_w
711
712
713
714
715
716
717
       ; 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 } }
718

719
  | otherwise
720
  = continueWith workItem
721

722
  where
723
    swap_me :: SwapFlag -> CtEvidence -> EvExpr
724
725
    swap_me swap ev
      = case swap of
726
727
           NotSwapped -> ctEvExpr ev
           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (EvExpr (ctEvExpr ev))))
728

729
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
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
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
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
822
{-
823
824
825
826
827
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
828

829
830
Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
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

854
855
This is bad! We could do /much/ better if we solved [W] `Num Int` directly
from the instance that we have in scope:
856
857
858
859
860

    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#) }

861
862
863
864
865
866
867
868
869
870
** 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:
871
872
873
874
875
876
877

    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
878
879
880
881
882
883
884
885
[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.
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920

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)

921
922
Note [Shortcut solving: type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
923
924
925
926
927
928
929
930
931
932
933
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
934
InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a
935
936
937
938
unique match on the (Take n) instance.  That leads immediately to an
infinite loop.  Hence the check that 'preds' have no type families
(isTyFamFree).

939
940
941
942
943
944
945
946
947
948
949
950
951
952
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
953
954
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
955
can change the behavior of the user's code.
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
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010

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`.
Austin Seipp's avatar
Austin Seipp committed
1011
-}
1012

1013
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1014
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
1015
  | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
1016
  = -- There is a matching dictionary in the inert set
1017
1018
    do { -- First to try to solve it /completely/ from top level instances
         -- See Note [Shortcut solving]
1019
         dflags <- getDynFlags
1020
       ; try_inst_res <- shortCutSolver dflags ev_w ev_i
1021
       ; case try_inst_res of
1022
           Just evs -> do { flip mapM_ evs $ \ (ev_t, ct_ev, cls, typ) ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1023
                               do { setWantedEvBind (ctEvEvId ct_ev) ev_t
1024
1025
                                  ; addSolvedDict ct_ev cls typ }
                          ; stopWith ev_w "interactDict/solved from instance" }
1026
1027
1028
1029

           -- We were unable to solve the [W] constraint from in-scope instances
           -- so we solve it from the matching inert we found
           Nothing ->  do
1030
1031
1032
             { what_next <- solveOneFromTheOther ev_i ev_w
             ; traceTcS "lookupInertDict" (ppr what_next)
             ; case what_next of
1033
                 KeepInert -> do { setEvBindIfWanted ev_w (ctEvExpr ev_i)
1034
                                 ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
1035
                 KeepWork  -> do { setEvBindIfWanted ev_i (ctEvExpr ev_w)
1036
1037
                                 ; updInertDicts $ \ ds -> delDict ds cls tys
                                 ; continueWith workItem } } }
1038

1039
  | cls `hasKey` ipClassKey
1040
1041
1042
1043
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
1044
1045
1046
1047
1048
  = do { addFunDepWork inerts ev_w cls
       ; continueWith workItem  }

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

1049
1050
1051
1052
1053
1054
1055
-- See Note [Shortcut solving]
shortCutSolver :: DynFlags
               -> CtEvidence -- Work item
               -> CtEvidence -- Inert we want to try to replace
               -> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
                      -- Everything we need to bind a solution for the work item
                      -- and add the solved Dict to the cache in the main solver.
1056
shortCutSolver dflags ev_w ev_i
1057
  | isWanted ev_w
1058
 && isGiven ev_i
1059
1060
1061
1062
 -- 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
1063
1064
 -- not. See Note [Shortcut solving]

1065
1066
1067
1068
 && 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.
1069
 -- See Note [Shortcut solving: incoherence]
1070

1071
1072
 && gopt Opt_SolveConstantDicts dflags
 -- Enabled by the -fsolve-constant-dicts flag
1073
  = runMaybeT $ try_solve_from_instance loc_w emptyDictMap ev_w
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087

  | otherwise = return Nothing
  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

    -- 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.
    new_wanted_cached :: DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
    new_wanted_cached cache pty
      | ClassPred cls tys <- classifyPredType pty
1088
      = lift $ case findDict cache loc_w cls tys of
1089
          Just ctev -> return $ Cached (ctEvExpr ctev)
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
          Nothing -> Fresh <$> newWantedNC loc_w pty
      | otherwise = mzero

    -- MaybeT manages early failure if we find a subgoal that cannot be solved
    -- from instances.
    -- Why do we need a local cache here?
    -- 1. We can't use the global cache because it contains givens that
    --    we specifically don't want to use to solve.
    -- 2. We need to be able to handle recursive super classes. The
    --    cache ensures that we remember what we have already tried to
    --    solve to avoid looping.
    try_solve_from_instance
1102
      :: CtLoc -> DictMap CtEvidence -> CtEvidence
1103
      -> MaybeT TcS [(EvTerm, CtEvidence, Class, [TcPredType])]
1104
1105
1106
    try_solve_from_instance loc cache ev
      | let pred = ctEvPred ev
      , ClassPred cls tys <- classifyPredType pred
1107
1108
      -- 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.
1109
1110
      = do { let cache' = addDict cache cls tys ev
                 loc'   = bumpCtLocDepth loc
1111
           ; inst_res <- lift $ match_class_inst dflags True cls tys loc_w
1112
1113
1114
1115
1116
           ; case inst_res of
               GenInst { lir_new_theta = preds
                       , lir_mk_ev = mk_ev
                       , lir_safe_over = safeOverlap }
                 | safeOverlap
1117
                 , all isTyFamFree preds  -- Note [Shortcut solving: type families]
1118
1119
1120
1121
1122
1123
1124
                 -> do { lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
                       ; lift $ checkReductionDepth loc' pred
                       ; evc_vs <- mapM (new_wanted_cached cache') preds
                                  -- Emit work for subgoals but use our local cache
                                  -- so we can solve recursive dictionaries.
                       ; subgoalBinds <- mapM (try_solve_from_instance loc' cache')
                                              (freshGoals evc_vs)
1125
                       ; return $ (mk_ev (map getEvExpr evc_vs), ev, cls, preds)
1126
1127
1128
1129
                                : concat subgoalBinds }

                 | otherwise -> mzero
               _ -> mzero }
1130
1131
      | otherwise = mzero