TcInteract.hs 102 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
David Eichmann's avatar
David Eichmann committed
30
import ClsInst( 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

42
import CoreSyn
David Eichmann's avatar
David Eichmann committed
43
import Data.List( partition, deleteFirstsBy )
44
import SrcLoc
dimitris's avatar
dimitris committed
45
46
import VarEnv

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

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

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

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

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

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

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

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

93
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
Jan Stolarek's avatar
Jan Stolarek committed
94
   need to worry about them across successive passes over the constraint tree.
95
96
97
98
99
   (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.

100
 * Another tricky case becomes easy: #4935
101
102
103
104
105
106
107
108
       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
109
   will do exactly that after solving the simple constraints and before
110
111
112
113
114
115
116
117
118
   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
119
120
121

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

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

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

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

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

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

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

186

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

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

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

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

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

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

-- | 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
257
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
258
-- main solver.
259
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
260
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
261
262
263
264
265
266
267
268
269
270
271
272
273
  | 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
274
             insols                                 = pluginBadCts p
275
276
277
278
279
280

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

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

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

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

    add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
    add xs scs = foldl' addOne scs xs

    addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
    addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
      CtGiven  {} -> (ct:givens, deriveds, wanteds)
      CtDerived{} -> (givens, ct:deriveds, wanteds)
      CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)


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

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

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

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

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

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

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

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

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

457
But this isn't quite true.  Suppose we have,
458
459
460
    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
     c1: [G] beta ~ [alpha], c2 : [W] blah
461
Now, c3 does not interact with the given c1, so when we spontaneously
462
solve c3, we must re-react it with the inert set.  So we can attempt a
463
464
465
reaction between inert c2 [W] and work-item c3 [G].

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

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

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

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

493
data InteractResult
494
495
496
   = 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
497

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

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
504
505
506
507
508
509
510
511
                     -> 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

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

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

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

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

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

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

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

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

545
  | lvl_i == lvl_w
Simon Peyton Jones's avatar
Simon Peyton Jones committed
546
547
  = do { ev_binds_var <- getTcEvBindsVar
       ; binds <- getTcEvBindsMap ev_binds_var
548
       ; return (same_level_strategy binds) }
549

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

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

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

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

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

581
582
       | otherwise
       = KeepInert
583

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

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

592
  * Constraints come from different levels (different_level_strategy)
593

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

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

603
604
605
606
        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
607
  * Constraints coming from the same level (i.e. same implication)
608

609
610
611
612
       (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
613

614
615
616
617
618
       (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)
619
620
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
621
622
623
624
625
626
627
628
629
630
            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!
631
           Hence the findNeedEvVars test.  See #14774.
632
633
634
635
636

  * 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
637
638

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

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

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

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
675
-}
676

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

683
684
685
686
687
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]
688
  , not (isDroppableCt workItem)
689
690
691
  = continueWith workItem

  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
692
693
  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
        -- See Note [Multiple matching irreds]
694
  , let ev_i = ctEvidence ct_i
695
  = do { what_next <- solveOneFromTheOther ev_i ev_w
696
697
698
699
700
701
702
       ; 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 } }
703

704
  | otherwise
705
  = continueWith workItem
706

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

714
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
747
Consider (#14333)
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
  [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
807
{-
808
809
810
811
812
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
813

814
815
Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
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

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

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

846
847
848
849
850
851
852
853
854
855
** 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:
856
857
858
859
860
861
862

    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
863
864
865
866
867
868
869
870
[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.
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
905

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)

906
907
Note [Shortcut solving: type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
908
Suppose we have (#13943)
909
910
911
912
913
914
915
916
917
918
  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
919
InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a
920
921
922
923
unique match on the (Take n) instance.  That leads immediately to an
infinite loop.  Hence the check that 'preds' have no type families
(isTyFamFree).

924
925
Note [Shortcut solving: incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926
927
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
928
can change the behavior of the user's code.
929
930
931
932
933
934
935
936
937
938
939
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

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`.
984
985
986
987

Note [Shortcut try_solve_from_instance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The workhorse of the short-cut solver is
988
    try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
989
990
991
992
                            -> CtEvidence       -- Solve this
                            -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
Note that:

993
* The CtEvidence is the goal to be solved
994
995
996
997
998
999
1000

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