TcInteract.hs 108 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 13
import BasicTypes ( SwapFlag(..), isSwapped,
                    infinity, IntWithInf, intGtLimit )
14
import HsTypes ( HsIPName(..) )
15
import TcCanonical
16
import TcFlatten
17
import TcUnify( canSolveByUnification )
18 19
import VarSet
import Type
Ben Gamari's avatar
Ben Gamari committed
20
import Kind( isConstraintKind )
21
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
22
import CoAxiom( sfInteractTop, sfInteractInert )
23

24 25
import TcMType (newMetaTyVars)

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

48
import TcEvidence
49 50
import Outputable

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

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

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

68 69 70
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe

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

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

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

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

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

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

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

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

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

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

182 183
     | isEmptyBag (wc_simple wc)
     = return (n,wc)
184

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

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

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

199

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

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

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

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

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

-- | 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
270
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
271
-- main solver.
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
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
297 298 299
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv (ev,ct) = case ctEvidence ct of
300
      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
Adam Gundry's avatar
Adam Gundry committed
301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
      _ -> 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
    }

323 324 325
getTcPlugins :: TcS [TcPluginSolver]
getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }

Adam Gundry's avatar
Adam Gundry committed
326 327 328 329 330 331 332 333 334 335 336 337 338
-- | 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.
339 340 341
runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPlugins plugins all_cts
  = foldM do_plugin initialProgress plugins
Adam Gundry's avatar
Adam Gundry committed
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
  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
369 370
    eqCt c c' = ctFlavour c == ctFlavour c'
             && ctPred c `tcEqType` ctPred c'
Adam Gundry's avatar
Adam Gundry committed
371 372 373 374 375 376 377 378 379 380 381

    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)


382
type WorkItem = Ct
383
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
384

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

398
       ; bumpStepCountTcS    -- One step for each constraint processed
399
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
400

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

Austin Seipp's avatar
Austin Seipp committed
421
{-
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
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
444
-}
445

446
thePipeline :: [(String,SimplifierStage)]
447
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
448 449
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
450

Austin Seipp's avatar
Austin Seipp committed
451
{-
452
*********************************************************************************
453
*                                                                               *
454 455 456 457
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

458 459 460 461 462
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

463
   If the work-item is Given,
464 465
   then the inert item must Given

466
But this isn't quite true.  Suppose we have,
467 468 469 470
    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
471
solve c3, we must re-react it with the inert set.  So we can attempt a
472 473 474
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
475
   If the work-item is Given,
476 477 478
   AND there is a reaction
   then the inert item must Given
or, equivalently,
479
   If the work-item is Given,
480 481
   and the inert item is Wanted/Derived
   then there is no reaction
Austin Seipp's avatar
Austin Seipp committed
482
-}
483

484
-- Interaction result of  WorkItem <~> Ct
485

486
type StopNowFlag = Bool    -- True <=> stop after this interaction
487

488
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
489 490
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
491

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

504 505 506 507 508
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

509
instance Outputable InteractResult where
510 511 512
  ppr IRKeep    = text "keep"
  ppr IRReplace = text "replace"
  ppr IRDelete  = text "delete"
513 514 515 516 517 518

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

524 525 526
  | 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
527

528 529
  | CtWanted { ctev_loc = loc_w } <- ev_w
  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
530 531
  = do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
       ; return (IRDelete, False) }
532

533 534 535
  | CtWanted { ctev_dest = dest } <- ev_w
       -- Inert is Given or Wanted
  = do { setWantedEvTerm dest (ctEvTerm ev_i)
536 537
       ; return (IRKeep, True) }

538 539
  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
540 541 542 543
  = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
       ; return (IRKeep, False) } -- Just discard the un-usable Given
                                  -- This never actually happens because
                                  -- Givens get processed first
544

545 546
  | CtWanted { ctev_dest = dest } <- ev_i
  = do { setWantedEvTerm dest (ctEvTerm ev_w)
547 548
       ; return (IRReplace, True) }

549 550 551 552
  -- So they are both Given
  -- See Note [Replacement vs keeping]
  | lvl_i == lvl_w
  = do { binds <- getTcEvBindsMap
553
       ; return (same_level_strategy binds, True) }
554

555 556 557
  | otherwise   -- Both are Given, levels differ
  = return (different_level_strategy, True)
  where
558 559 560 561 562
     pred  = ctEvPred ev_i
     loc_i = ctEvLoc ev_i
     loc_w = ctEvLoc ev_w
     lvl_i = ctLocLevel loc_i
     lvl_w = ctLocLevel loc_w
563

564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584
     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

585
     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
586

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

593
  * Constraints come from different levels (different_level_strategy)
594

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

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

604 605 606 607
        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
608
  * Constraints coming from the same level (i.e. same implication)
609 610 611 612 613 614 615 616

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

624
  * Finally, when there is still a choice, use IRKeep rather than
Gabor Greif's avatar
Gabor Greif committed
625
    IRReplace, to avoid unnecessary munging of the inert set.
626 627

Doing the depth-check for implicit parameters, rather than making the work item
Gabor Greif's avatar
Gabor Greif committed
628
always override, is important.  Consider
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646

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

647 648 649 650 651
*********************************************************************************
*                                                                               *
                   interactIrred
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
652
-}
653

654 655 656 657
-- 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)
658
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
659 660 661

interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
  | let pred = ctEvPred ev_w
662 663 664
        (matching_irreds, others)
          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
                         (inert_irreds inerts)
665 666 667 668
  , (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
669 670 671 672 673 674 675
       ; 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
676
            return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
677 678
       ; else
            continueWith workItem }
679

680
  | otherwise
681
  = continueWith workItem
682

683
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
684

Austin Seipp's avatar
Austin Seipp committed
685
{-
686 687 688 689 690
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776

Note [Solving from instances when interacting Dicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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

This is bad! We could do much better if we solved [W] `Num Int` directly from
the instance that we have in scope:

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

However, 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:

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

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)

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
777
can change the behavior of the user's code.
778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838

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

It is important to emphasize that failure means that we don't produce more
efficient code, NOT that we fail to typecheck at all! This is purely an
an optimization: exactly the same programs should typecheck with or without this
procedure.

Austin Seipp's avatar
Austin Seipp committed
839
-}
840

841
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
842
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
843
  | isWanted ev_w
Eric Seidel's avatar
Eric Seidel committed
844
  , Just ip_name      <- isCallStackPred (ctPred workItem)
845 846 847 848
  , 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.
849
  -- See Note [Overview of implicit CallStacks]
850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866
  = 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" }
867
  | Just ctev_i <- lookupInertDict inerts cls tys
868 869 870 871 872 873 874 875 876 877 878 879 880 881
  = do
  { dflags <- getDynFlags
  -- See Note [Solving from instances when interacting Dicts]
  ; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
  ; case try_inst_res of
      Just evs -> do
        { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
          { setWantedEvBind (ctEvId ct_ev) ev_t
          ; addSolvedDict ct_ev cls typ }
        ; stopWith ev_w "interactDict/solved from instance" }
      -- We were unable to solve the [W] constraint from in-scope instances so
      -- we solve it from the solution in the inerts we just retrieved.
      Nothing ->  do
        { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
882
        ; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
883 884 885 886 887 888 889 890
        ; 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 (text "Dict equal" <+> parens (ppr inert_effect))
          else
            continueWith workItem } }
891
  | cls `hasKey` ipClassKey
892 893 894 895
  , isGiven ev_w
  = interactGivenIP inerts workItem

  | otherwise
896 897 898 899 900
  = do { addFunDepWork inerts ev_w cls
       ; continueWith workItem  }

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

901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 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
-- See Note [Solving from instances when interacting Dicts]
trySolveFromInstance :: DynFlags
                     -> CtEvidence -- Work item
                     -> CtEvidence -- Inert we want to try to replace
                     -> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
                     -- Everything we need to bind a solution for the work item
                     -- and add the solved Dict to the cache in the main solver.
trySolveFromInstance dflags ev_w ctev_i
  | isWanted ev_w
 && isGiven ctev_i
 -- We are about to solve a [W] constraint from a [G] constraint. We take
 -- a moment to see if we can get a better solution using an instance.
 -- Note that we only do this for the sake of performance. Exactly the same
 -- programs should typecheck regardless of whether we take this step or
 -- not. See Note [Solving from instances when interacting Dicts]
 && not (xopt LangExt.IncoherentInstances dflags)
 -- If IncoherentInstances is on then we cannot rely on coherence of proofs
 -- in order to justify this optimization: The proof provided by the
 -- [G] constraint's superclass may be different from the top-level proof.
 && gopt Opt_SolveConstantDicts dflags
 -- Enabled by the -fsolve-constant-dicts flag
  = runMaybeT $ try_solve_from_instance emptyDictMap ev_w

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

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

    -- MaybeT manages early failure if we find a subgoal that cannot be solved
    -- from instances.
    -- Why do we need a local cache here?
    -- 1. We can't use the global cache because it contains givens that
    --    we specifically don't want to use to solve.
    -- 2. We need to be able to handle recursive super classes. The
    --    cache ensures that we remember what we have already tried to
    --    solve to avoid looping.
    try_solve_from_instance
      :: DictMap CtEvidence -> CtEvidence
      -> MaybeT TcS [(EvTerm, CtEvidence, Class, [TcPredType])]
    try_solve_from_instance cache ev
      | ClassPred cls tys <- classifyPredType (ctEvPred ev) = do
      -- It is important that we add our goal to the cache before we solve!
      -- Otherwise we may end up in a loop while solving recursive dictionaries.
      { let cache' = addDict cache cls tys ev
      ; inst_res <- lift $ match_class_inst dflags cls tys loc_w
      ; case inst_res of
          GenInst { lir_new_theta = preds
                  , lir_mk_ev = mk_ev
                  , lir_safe_over = safeOverlap }
            | safeOverlap -> do
              -- emit work for subgoals but use our local cache so that we can
              -- solve recursive dictionaries.
              { evc_vs <- mapM (new_wanted_cached cache') preds
              ; subgoalBinds <- mapM (try_solve_from_instance cache')
                                     (freshGoals evc_vs)
              ; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
                       : concat subgoalBinds }

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

976 977 978
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
-- Add derived constraints from type-class functional dependencies.
addFunDepWork inerts work_ev cls
979
  | isImprovable work_ev
980
  = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
981 982
               -- No need to check flavour; fundeps work between
               -- any pair of constraints, regardless of flavour
983 984
               -- Importantly we don't throw workitem back in the
               -- worklist because this can cause loops (see #5236)
985 986
  | otherwise
  = return ()
987 988 989
  where
    work_pred = ctEvPred work_ev
    work_loc  = ctEvLoc work_ev
990

991
    add_fds inert_ct
992
      | isImprovable inert_ev
993 994 995 996 997 998
      = 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
999 1000
      | otherwise
      = return ()
1001
      where
1002 1003 1004
        inert_ev   = ctEvidence inert_ct
        inert_pred = ctEvPred inert_ev
        inert_loc  = ctEvLoc inert_ev
1005 1006 1007
        derived_loc = work_loc { ctl_depth  = ctl_depth work_loc `maxSubGoalDepth`
                                              ctl_depth inert_loc
                               , ctl_origin = FunDepOrigin1 work_pred  work_loc
1008
                                                            inert_pred inert_loc }
1009

1010
{-
1011 1012
**********************************************************************
*                                                                    *