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

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

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

#include "HsVersions.h"

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

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

41
import TcEvidence
42
43
import Outputable

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

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

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

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

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

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

   The threading of the stages is as follows:
      - If (Stop) is returned by a stage then we start again from Step 1.
      - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
        the next stage in the pipeline.
4. If the element has survived (i.e. ContinueWith x) the last stage
86
87
   then we add him in the inerts and jump back to Step 1.

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

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

96
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
Jan Stolarek's avatar
Jan Stolarek committed
97
   need to worry about them across successive passes over the constraint tree.
98
99
100
101
102
103
104
105
106
107
108
109
110
111
   (E.g. we don't need the old ic_fsk field of an implication.

 * When floating an equality outwards, we don't need to worry about floating its
   associated flattening constraints.

 * Another tricky case becomes easy: Trac #4935
       type instance F True a b = a
       type instance F False a b = b

       [w] F c a b ~ gamma
       (c ~ True) => a ~ gamma
       (c ~ False) => b ~ gamma

   Obviously this is soluble with gamma := F c a b, and unflattening
112
   will do exactly that after solving the simple constraints and before
113
114
115
116
117
118
119
120
121
   attempting the implications.  Before, when we were not unflattening,
   we had to push Wanted funeqs in as new givens.  Yuk!

   Another example that becomes easy: indexed_types/should_fail/T7786
      [W] BuriedUnder sub k Empty ~ fsk
      [W] Intersect fsk inv ~ s
      [w] xxx[1] ~ s
      [W] forall[2] . (xxx[1] ~ Empty)
                   => Intersect (BuriedUnder sub k Empty) inv ~ Empty
122
123
124

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
125
126
There is an annoying mismatch between solveSimpleGivens and
solveSimpleWanteds, because the latter needs to fiddle with the inert
Jan Stolarek's avatar
Jan Stolarek committed
127
set, unflatten and zonk the wanteds.  It passes the zonked wanteds
128
129
130
131
132
133
to runTcPluginsWanteds, which produces a replacement set of wanteds,
some additional insolubles and a flag indicating whether to go round
the loop again.  If so, prepareInertsForImplications is used to remove
the previous wanteds (which will still be in the inert set).  Note
that prepareInertsForImplications will discard the insolubles, so we
must keep track of them separately.
Austin Seipp's avatar
Austin Seipp committed
134
-}
135

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

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

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

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

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

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

186

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

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

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

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

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

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
239
-- return new work produced so that 'solveSimpleGivens' can feed it back
Adam Gundry's avatar
Adam Gundry committed
240
241
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
242
243
244
245
246
247
248
249
250
251
runTcPluginsGiven
  = do { plugins <- getTcPlugins
       ; if null plugins then return [] else
    do { givens <- getInertGivens
       ; if null givens then return [] else
    do { p <- runTcPlugins plugins (givens,[],[])
       ; let (solved_givens, _, _) = pluginSolvedCts p
       ; updInertCans (removeInertCts solved_givens)
       ; mapM_ emitInsoluble (pluginBadCts p)
       ; return (pluginNewCts p) } } }
Adam Gundry's avatar
Adam Gundry committed
252
253
254
255

-- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
-- them and produce an updated bag of wanteds (possibly with some new
-- work) and a bag of insolubles.  The boolean indicates whether
256
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
257
-- main solver.
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
  | isEmptyBag simples1
  = return (False, wc)
  | otherwise
  = do { plugins <- getTcPlugins
       ; if null plugins then return (False, wc) else

    do { given <- getInertGivens
       ; simples1 <- zonkSimples simples1    -- Plugin requires zonked inputs
       ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
       ; p <- runTcPlugins plugins (given, derived, wanted)
       ; let (_, _,                solved_wanted)   = pluginSolvedCts p
             (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
             new_wanted                             = pluginNewCts p

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

       ; mapM_ setEv solved_wanted
       ; return ( notNull (pluginNewCts p)
                , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
                                                        `andCts` listToBag unsolved_derived
                     , wc_insol  = listToBag (pluginBadCts p) `andCts` insols1
                     , wc_impl   = implics1 } ) } }
Adam Gundry's avatar
Adam Gundry committed
283
284
285
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
286
      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
Adam Gundry's avatar
Adam Gundry committed
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
      _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"

-- | A triple of (given, derived, wanted) constraints to pass to plugins
type SplitCts  = ([Ct], [Ct], [Ct])

-- | A solved triple of constraints, with evidence for wanteds
type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])

-- | Represents collections of constraints generated by typechecker
-- plugins
data TcPluginProgress = TcPluginProgress
    { pluginInputCts  :: SplitCts
      -- ^ Original inputs to the plugins with solved/bad constraints
      -- removed, but otherwise unmodified
    , pluginSolvedCts :: SolvedCts
      -- ^ Constraints solved by plugins
    , pluginBadCts    :: [Ct]
      -- ^ Constraints reported as insoluble by plugins
    , pluginNewCts    :: [Ct]
      -- ^ New constraints emitted by plugins
    }

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

Adam Gundry's avatar
Adam Gundry committed
312
313
314
315
316
317
318
319
320
321
322
323
324
-- | Starting from a triple of (given, derived, wanted) constraints,
-- invoke each of the typechecker plugins in turn and return
--
--  * the remaining unmodified constraints,
--  * constraints that have been solved,
--  * constraints that are insoluble, and
--  * new work.
--
-- Note that new work generated by one plugin will not be seen by
-- other plugins on this pass (but the main constraint solver will be
-- re-invoked and they will see it later).  There is no check that new
-- work differs from the original constraints supplied to the plugin:
-- the plugin itself should perform this check if necessary.
325
326
327
runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPlugins plugins all_cts
  = foldM do_plugin initialProgress plugins
Adam Gundry's avatar
Adam Gundry committed
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
  where
    do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
    do_plugin p solver = do
        result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
        return $ progress p result

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

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

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

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

    eqCt :: Ct -> Ct -> Bool
    eqCt c c' = case (ctEvidence c, ctEvidence c') of
      (CtGiven   pred _ _, CtGiven   pred' _ _) -> pred `eqType` pred'
      (CtWanted  pred _ _, CtWanted  pred' _ _) -> pred `eqType` pred'
      (CtDerived pred _  , CtDerived pred' _  ) -> pred `eqType` pred'
      (_                 , _                  ) -> False

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

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


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

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

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

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

Austin Seipp's avatar
Austin Seipp committed
411
{-
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
Example 1:
  Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
  Reagent: a ~ [b] (given)

React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []

Example 2:
  Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
  Reagent: a ~w [b]

React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
etc.

Example 3:
  Inert:  {a ~ Int, F Int ~ b} (given)
  Reagent: F a ~ b (wanted)

React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
Austin Seipp's avatar
Austin Seipp committed
434
-}
435

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

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

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

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

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

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

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

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

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

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

494
495
496
497
498
data InteractResult
   = IRKeep      -- Keep the existing inert constraint in the inert set
   | IRReplace   -- Replace the existing inert constraint with the work item
   | IRDelete    -- Delete the existing inert constraint from the inert set

499
500
501
502
503
504
505
506
507
508
instance Outputable InteractResult where
  ppr IRKeep    = ptext (sLit "keep")
  ppr IRReplace = ptext (sLit "replace")
  ppr IRDelete  = ptext (sLit "delete")

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

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

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

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

527
528
529
530
531
532
  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
  = return (IRKeep, False)  -- Just discard the un-usable Given
                            -- This never actually happens because
                            -- Givens get processed first

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

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

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

552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
     different_level_strategy
       | isIPPred pred, lvl_w > lvl_i = IRReplace
       | lvl_w < lvl_i                = IRReplace
       | otherwise                    = IRKeep

     same_level_strategy binds        -- Both Given
       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
       = case ctLocOrigin loc_w of
            GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
                                     | otherwise -> IRKeep
            _                                    -> IRReplace

       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
       = IRKeep

       | has_binding binds ev_w
       , not (has_binding binds ev_i)
       = IRReplace

       | otherwise = IRKeep

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

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

581
  * Constraints come from different levels (different_level_strategy)
582

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

587
588
589
590
      - For everything else, we want to keep the outermost one.  Reason: that
        makes it more likely that the inner one will turn out to be unused,
        and can be reported as redundant.  See Note [Tracking redundant constraints]
        in TcSimplify.
591

592
593
594
595
        It transpires that using the outermost one is reponsible for an
        8% performance improvement in nofib cryptarithm2, compared to
        just rolling the dice.  I didn't investigate why.

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

       - Always get rid of InstSC ones if possible, since they are less
         useful for solving.  If both are InstSC, choose the one with
         the smallest TypeSize
         See Note [Solving superclass constraints] in TcInstDcls

       - Keep the one that has a non-trivial evidence binding.
            Example:  f :: (Eq a, Ord a) => blah
Simon Peyton Jones's avatar
Simon Peyton Jones committed
605
            then we may find [G] d3 :: Eq a
606
                             [G] d2 :: Eq a
Simon Peyton Jones's avatar
Simon Peyton Jones committed
607
              with bindings  d3 = sc_sel (d1::Ord a)
608
609
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
610
         Why? See Note [Tracking redundant constraints] in TcSimplify again.
611

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

Doing the depth-check for implicit parameters, rather than making the work item
always overrride, is important.  Consider

    data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }

    f :: (?x::a) => T a -> Int
    f T1 = ?x
    f T2 = 3

We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
two new givens in the work-list:  [G] (?x::Int)
                                  [G] (a ~ Int)
Now consider these steps
  - process a~Int, kicking out (?x::a)
  - process (?x::Int), the inner given, adding to inert set
  - process (?x::a), the outer given, overriding the inner given
Wrong!  The depth-check ensures that the inner implicit parameter wins.
(Actually I think that the order in which the work-list is processed means
that this chain of events won't happen, but that's very fragile.)

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

642
643
644
645
-- Two pieces of irreducible evidence: if their types are *exactly identical*
-- we can rewrite them. We can never improve using this:
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
646
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
647
648
649

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
650
651
652
        (matching_irreds, others)
          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
                         (inert_irreds inerts)
653
654
655
656
  , (ct_i : rest) <- bagToList matching_irreds
  , let ctev_i = ctEvidence ct_i
  = ASSERT( null rest )
    do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
657
658
659
660
661
662
663
664
665
666
       ; case inert_effect of
            IRKeep    -> return ()
            IRDelete  -> updInertIrreds (\_ -> others)
            IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
                         -- These const upd's assume that solveOneFromTheOther
                         -- has no side effects on InertCans
       ; if stop_now then
            return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
       ; else
            continueWith workItem }
667

668
  | otherwise
669
  = continueWith workItem
670

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

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

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

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

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

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

708
  | Just ctev_i <- lookupInertDict inerts cls tys
709
  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
710
711
712
713
714
715
       ; case inert_effect of
           IRKeep    -> return ()
           IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
           IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
       ; if stop_now then
            return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
Austin Seipp's avatar
Austin Seipp committed
716
         else
717
            continueWith workItem }
718

719
  | cls `hasKey` ipClassKey
720
721
722
723
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
724
725
726
727
728
729
730
731
732
  = do { addFunDepWork inerts ev_w cls
       ; continueWith workItem  }

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

addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
-- Add derived constraints from type-class functional dependencies.
addFunDepWork inerts work_ev cls
  = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
733
734
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
735
736
               -- Importantly we don't throw workitem back in the
               -- worklist because this can cause loops (see #5236)
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
  where
    work_pred = ctEvPred work_ev
    work_loc  = ctEvLoc work_ev
    add_fds inert_ct
      = emitFunDepDeriveds $
        improveFromAnother derived_loc inert_pred work_pred
               -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
               -- NB: We do create FDs for given to report insoluble equations that arise
               -- from pairs of Givens, and also because of floating when we approximate
               -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
      where
        inert_pred = ctPred inert_ct
        inert_loc  = ctLoc inert_ct
        derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
                                                            inert_pred inert_loc }
752

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

761
interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
762
763
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
764
765
766
767
interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
                                          , cc_tyargs = tys@(ip_str:_) })
  = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
       ; stopWith ev "Given IP" }
768
769
770
771
772
773
774
775
  where
    dicts           = inert_dicts inerts
    ip_dicts        = findDictsByClass dicts cls
    other_ip_dicts  = filterBag (not . is_this_ip) ip_dicts
    filtered_dicts  = addDictsByClass dicts cls other_ip_dicts

    -- Pick out any Given constraints for the same implicit parameter
    is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
776
       = isGiven ev && ip_str `tcEqType` ip_str'
777
778
779
780
    is_this_ip _ = False

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

781

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

787
788
f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x
789

790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
The "let ?x = ..." generates an implication constraint of the form:

?x :: Char => ?x :: Char

Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:

?x :: Char => (?x :: Char => ?x :: Char)

Note that the wanted (?x :: Char) constraint may be solved in
two incompatible ways:  either by using the parameter from the
signature, or by using the local definition.  Our intention is
that the local definition should "shadow" the parameter of the
signature, and we implement this as follows: when we add a new
*given* implicit parameter to the inert set, it replaces any existing
givens for the same implicit parameter.

This works for the normal cases but it has an odd side effect
in some pathological programs like this:

-- This is accepted, the second parameter shadows
f1 :: (?x :: Int, ?x :: Char) => Char
f1 = ?x

-- This is rejected, the second parameter shadows
f2 :: (?x :: Int, ?x :: Char) => Int
f2 = ?x

Both of these are actually wrong:  when we try to use either one,
we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
which would lead to an error.

I can think of two ways to fix this:

  1. Simply disallow multiple constratits for the same implicit
    parameter---this is never useful, and it can be detected completely
    syntactically.

  2. Move the shadowing machinery to the location where we nest
     implications, and add some code here that will produce an
     error if we get multiple givens for the same implicit parameter.


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

840
841
interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- Try interacting the work item with the inert set
842
interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
843
                                         , cc_tyargs = args, cc_fsk = fsk })
844
845
  | Just (CFunEqCan { cc_ev = ev_i
                    , cc_fsk = fsk_i }) <- matching_inerts
846
  = if ev_i `funEqCanDischarge` ev
847
848
849
850
851
852
    then  -- Rewrite work-item using inert
      do { traceTcS "reactFunEq (discharge work item):" $
           vcat [ text "workItem =" <+> ppr workItem
                , text "inertItem=" <+> ppr ev_i ]
         ; reactFunEq ev_i fsk_i ev fsk
         ; stopWith ev "Inert rewrites work item" }
853
    else  -- Rewrite inert using work-item
854
      ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
855
856
857
858
859
860
861
862
863
      do { traceTcS "reactFunEq (rewrite inert item):" $
           vcat [ text "workItem =" <+> ppr workItem
                , text "inertItem=" <+> ppr ev_i ]
         ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
               -- Do the updInertFunEqs before the reactFunEq, so that
               -- we don't kick out the inertItem as well as consuming it!
         ; reactFunEq ev fsk ev_i fsk_i
         ; stopWith ev "Work item rewrites inert" }

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

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

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

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

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

Jan Stolarek's avatar
Jan Stolarek committed
904
905
906
907
908
      | otherwise
      = []

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

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

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

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

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

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

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

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

Jan Stolarek's avatar
Jan Stolarek committed
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
Note [Type inference for type families with injectivity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a type family with an injectivity annotation:
    type family F a b = r | r -> b

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

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

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

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

See also Note [Injective type families] in TyCon


1002
1003
1004
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1005
solved cache (which is the default behaviour or xCtEvidence), because the interaction
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
may not be contributing towards a solution. Here is an example:

Initial inert set:
  [W] g1 : F a ~ beta1
Work item:
  [W] g2 : F a ~ beta2
The work item will react with the inert yielding the _same_ inert set plus:
    i)   Will set g2 := g1 `cast` g3
    ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
    iii) Will emit [W] g3 : beta1 ~ beta2
Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
will set
      g1 := g ; sym g3
and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
remember that we have this in our solved cache, and it is ... g2! In short we
created the evidence loop:

        g2 := g1 ; g3
        g3 := refl
        g1 := g2 ; sym g3

To avoid this situation we do not cache as solved any workitems (or inert)
which did not really made a 'step' towards proving some goal. Solved's are
just an optimization so we don't lose anything in terms of completeness of
solving.


1034
Note [Efficient Orientation]
1035
1036
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
1037
1038
          (inert)  ci :: (F ty ~ xi_i)
          (work)   cw :: (F ty ~ xi_w)
1039
1040
We prefer to keep the inert (else we pass the work item on down
the pipeline, which is a bit silly).  If we keep the inert, we
1041
will (a) discharge 'cw'
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
     (b) produce a new equality work-item (xi_w ~ xi_i)
Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
    new_work :: xi_w ~ xi_i
    cw := ci ; sym new_work
Why?  Consider the simplest case when xi1 is a type variable.  If
we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
If we generate xi2~xi1, there is less chance of that happening.
Of course it can and should still happen if xi1=a, xi1=Int, say.
But we want to avoid it happening needlessly.

Similarly, if we *can't* keep the inert item (because inert is Wanted,
and work is Given, say), we prefer to orient the new equality (xi_i ~
xi_w).

1056
1057
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1058
   ---- OLD COMMENT, NOW NOT NEEDED
Gabor Greif's avatar
Gabor Greif committed
1059
   ---- because we now allow multiple
1060
   ---- wanted FunEqs with the same head
1061
1062
1063
Consider the constraints
  c1 :: F Int ~ a      -- Arising from an application line 5
  c2 :: F Int ~ Bool   -- Arising from an application line 10
1064
Suppose that 'a' is a unification variable, arising only from
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
flattening.  So there is no error on line 5; it's just a flattening
variable.  But there is (or might be) an error on line 10.

Two ways to combine them, leaving either (Plan A)
  c1 :: F Int ~ a      -- Arising from an application line 5
  c3 :: a ~ Bool       -- Arising from an application line 10
or (Plan B)
  c2 :: F Int ~ Bool   -- Arising from an application line 10
  c4 :: a ~ Bool       -- Arising from an application line 5

Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
on the *totally innocent* line 5.  An example is test SimpleFail16
where the expected/actual message comes out backwards if we use
the wrong plan.

The second is the right thing to do.  Hence the isMetaTyVarTy
test when solving pairwise CFunEqCan.
1082
1083


1084
1085
**********************************************************************
*                                                                    *
1086
                   interactTyVarEq
1087
1088
*                                                                    *
**********************************************************************
Austin Seipp's avatar
Austin Seipp committed
1089
-}
1090

1091
1092
interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-- CTyEqCans are always consumed, so always returns Stop
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1093
1094
1095
1096
interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                          , cc_rhs = rhs
                                          , cc_ev = ev
                                          , cc_eq_rel = eq_rel })
1097
  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1098
                             <- findTyEqs inerts tv
1099
                         , ev_i `eqCanDischarge` ev
1100
                         , rhs_i `tcEqType` rhs ]
1101
1102
  =  -- Inert:     a ~ ty
     -- Work item: a ~ ty
1103
1104
1105
1106
1107
    do { setEvBindIfWanted ev $
          EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
                                      (ctEvRole ev_i)
                                      (ctEvCoercion ev_i))

1108
       ; stopWith ev "Solved from inert" }
1109
1110
1111

  | Just tv_rhs <- getTyVar_maybe rhs
  , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1112
                             <- findTyEqs inerts tv_rhs
1113
                         , ev_i `eqCanDischarge` ev
1114
                         , rhs_i `tcEqType` mkTyVarTy tv ]
1115
1116
  =  -- Inert:     a ~ b
     -- Work item: b ~ a
1117
1118
1119
1120
1121
1122
    do { setEvBindIfWanted ev $
           EvCoercion (mkTcSymCo $
                       tcDowngradeRole (eqRelRole eq_rel)
                                       (ctEvRole ev_i)
                                       (ctEvCoercion ev_i))

1123
       ; stopWith ev "Solved from inert (r)" }
1124

1125
  | otherwise
1126
  = do { tclvl <- getTcLevel
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1127
       ; if canSolveByUnification tclvl ev eq_rel tv rhs
1128
         then do { solveByUnification ev tv rhs