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

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

#include "HsVersions.h"

10 11
import GhcPrelude

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

24 25
import TcMType (newMetaTyVars)

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

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

53 54
import TcRnTypes
import TcSMonad
55
import Bag
56
import MonadUtils ( concatMapM, foldlM )
57

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

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

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

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

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

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

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

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

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

108
 * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
Jan Stolarek's avatar
Jan Stolarek committed
109
   need to worry about them across successive passes over the constraint tree.
110 111 112 113 114 115 116 117 118 119 120 121 122 123
   (E.g. we don't need the old ic_fsk field of an implication.

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

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

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

   Obviously this is soluble with gamma := F c a b, and unflattening
124
   will do exactly that after solving the simple constraints and before
125 126 127 128 129 130 131 132 133
   attempting the implications.  Before, when we were not unflattening,
   we had to push Wanted funeqs in as new givens.  Yuk!

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

Note [Running plugins on unflattened wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137 138
There is an annoying mismatch between solveSimpleGivens and
solveSimpleWanteds, because the latter needs to fiddle with the inert
Jan Stolarek's avatar
Jan Stolarek committed
139
set, unflatten and zonk the wanteds.  It passes the zonked wanteds
140 141 142 143 144 145
to runTcPluginsWanteds, which produces a replacement set of wanteds,
some additional insolubles and a flag indicating whether to go round
the loop again.  If so, prepareInertsForImplications is used to remove
the previous wanteds (which will still be in the inert set).  Note
that prepareInertsForImplications will discard the insolubles, so we
must keep track of them separately.
Austin Seipp's avatar
Austin Seipp committed
146
-}
147

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

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

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

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

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

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

201

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

217 218
{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
219 220
Solving a bunch of simple constraints is done in a loop,
(the 'go' loop of 'solveSimpleWanteds'):
221 222 223 224 225 226 227 228 229
  1. Try to solve them; unflattening may lead to improvement that
     was not exploitable during solving
  2. Try the plugin
  3. If step 1 did improvement during unflattening; or if the plugin
     wants to run again, go back to step 1

Non-obviously, improvement can also take place during
the unflattening that takes place in step (1). See TcFlatten,
See Note [Unflattening can force the solver to iterate]
230
-}
231 232 233

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

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

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

-- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
-- them and produce an updated bag of wanteds (possibly with some new
-- work) and a bag of insolubles.  The boolean indicates whether
272
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
Adam Gundry's avatar
Adam Gundry committed
273
-- main solver.
274
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
275
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
276 277 278 279 280 281 282 283 284 285 286 287 288
  | isEmptyBag simples1
  = return (False, wc)
  | otherwise
  = do { plugins <- getTcPlugins
       ; if null plugins then return (False, wc) else

    do { given <- getInertGivens
       ; simples1 <- zonkSimples simples1    -- Plugin requires zonked inputs
       ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
       ; p <- runTcPlugins plugins (given, derived, wanted)
       ; let (_, _,                solved_wanted)   = pluginSolvedCts p
             (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
             new_wanted                             = pluginNewCts p
289
             insols                                 = pluginBadCts p
290 291 292 293 294 295

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

Austin Seipp's avatar
Austin Seipp committed
427
{-
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
Example 1:
  Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
  Reagent: a ~ [b] (given)

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

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

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

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

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

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

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

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

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

472
But this isn't quite true.  Suppose we have,
473 474 475
    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
     c1: [G] beta ~ [alpha], c2 : [W] blah
476
Now, c3 does not interact with the given c1, so when we spontaneously
477
solve c3, we must re-react it with the inert set.  So we can attempt a
478 479 480
reaction between inert c2 [W] and work-item c3 [G].

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

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

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

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

508
data InteractResult
509 510 511
   = KeepInert   -- Keep the inert item, and solve the work item from it
                 -- (if the latter is Wanted; just discard it if not)
   | KeepWork    -- Keep the work item, and solve the intert item from it
512

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

solveOneFromTheOther :: CtEvidence  -- Inert
                     -> CtEvidence  -- WorkItem
519 520 521 522 523 524 525 526
                     -> TcS InteractResult
-- Precondition:
-- * inert and work item represent evidence for the /same/ predicate
--
-- We can always solve one from the other: even if both are wanted,
-- although we don't rewrite wanteds with wanteds, we can combine
-- two wanteds into one by solving one from the other

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

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

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

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

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

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

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

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

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

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

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

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

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

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

596 597
       | otherwise
       = KeepInert
598

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

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

607
  * Constraints come from different levels (different_level_strategy)
608

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

613 614 615 616
      - For everything else, we want to keep the outermost one.  Reason: that
        makes it more likely that the inner one will turn out to be unused,
        and can be reported as redundant.  See Note [Tracking redundant constraints]
        in TcSimplify.
617

618 619 620 621
        It transpires that using the outermost one is reponsible for an
        8% performance improvement in nofib cryptarithm2, compared to
        just rolling the dice.  I didn't investigate why.

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

624 625 626 627
       (a) Always get rid of InstSC ones if possible, since they are less
           useful for solving.  If both are InstSC, choose the one with
           the smallest TypeSize
           See Note [Solving superclass constraints] in TcInstDcls
628

629 630 631 632 633
       (b) Keep the one that has a non-trivial evidence binding.
              Example:  f :: (Eq a, Ord a) => blah
              then we may find [G] d3 :: Eq a
                               [G] d2 :: Eq a
                with bindings  d3 = sc_sel (d1::Ord a)
634 635
            We want to discard d2 in favour of the superclass selection from
            the Ord dictionary.
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
            Why? See Note [Tracking redundant constraints] in TcSimplify again.

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

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

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

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

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

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

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

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

Austin Seipp's avatar
Austin Seipp committed
690
-}
691

692 693 694 695
-- Two pieces of irreducible evidence: if their types are *exactly identical*
-- we can rewrite them. We can never improve using this:
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
696
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
697

698 699 700 701 702
interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
  | insoluble  -- For insolubles, don't allow the constaint to be dropped
               -- which can happen with solveOneFromTheOther, so that
               -- we get distinct error messages with -fdefer-type-errors
               -- See Note [Do not add duplicate derived insolubles]
703
  , not (isDroppableCt workItem)
704 705 706
  = continueWith workItem

  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
707 708
  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
        -- See Note [Multiple matching irreds]
709
  , let ev_i = ctEvidence ct_i
710
  = do { what_next <- solveOneFromTheOther ev_i ev_w
711 712 713 714 715 716 717
       ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
       ; case what_next of
            KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
                            ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
            KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
                            ; updInertIrreds (\_ -> others)
                            ; continueWith workItem } }
718

719
  | otherwise
720
  = continueWith workItem
721

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

729
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
730

731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821
findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
findMatchingIrreds irreds ev
  | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
    -- See Note [Solving irreducible equalities]
  = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
  | otherwise
  = partitionBagWith match_non_eq irreds
  where
    pred = ctEvPred ev
    match_non_eq ct
      | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
      | otherwise                            = Right ct

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

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

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

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

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

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

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

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

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

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

Assume we have started with an implication:

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

which we have simplified to:

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

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

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

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

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

Austin Seipp's avatar
Austin Seipp committed
822
{-
823 824 825 826 827
*********************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************
828

829 830
Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853
When we interact a [W] constraint with a [G] constraint that solves it, there is
a possibility that we could produce better code if instead we solved from a
top-level instance declaration (See #12791, #5835). For example:

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

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

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

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

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

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

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

861 862 863 864 865 866 867 868 869 870
** NB: It is important to emphasize that all this is purely an optimization:
** exactly the same programs should typecheck with or without this
** procedure.

Solving fully
~~~~~~~~~~~~~
There is a reason why the solver does not simply try to solve such
constraints with top-level instances. If the solver finds a relevant
instance declaration in scope, that instance may require a context
that can't be solved for. A good example of this is:
871 872 873 874 875 876 877

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

If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
be left with the obligation to solve the constraint Eq a, which we cannot. So we
must be conservative in our attempt to use an instance declaration to solve the
878 879 880 881 882 883 884 885
[W] constraint we're interested in.

Our rule is that we try to solve all of the instance's subgoals
recursively all at once. Precisely: We only attempt to solve
constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci
are themselves class constraints of the form `C1', ... Cm' => C' t1'
... tn'` and we only succeed if the entire tree of constraints is
solvable from instances.
886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920

An example that succeeds:

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

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

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

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

An example that fails:

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

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

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

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

921 922
Note [Shortcut solving: type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
923 924 925 926 927 928 929 930 931 932 933
Suppose we have (Trac #13943)
  class Take (n :: Nat) where ...
  instance {-# OVERLAPPING #-}                    Take 0 where ..
  instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..

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

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

939 940 941 942 943 944 945 946 947 948 949 950 951 952
Note [Shortcut solving: overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
  instance {-# OVERLAPPABLE #-} C a where ...
and we are typechecking
  f :: C a => a -> a
  f = e  -- Gives rise to [W] C a

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

Note [Shortcut solving: incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
953 954
This optimization relies on coherence of dictionaries to be correct. When we
cannot assume coherence because of IncoherentInstances then this optimization
Gabor Greif's avatar
Gabor Greif committed
955
can change the behavior of the user's code.
956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010

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

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

    class A a where
      int :: a -> Int

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

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

    import A

    instance A a where
      int _ = 1

    instance C a [b] where
      m _ = id

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

    import A

    instance A Int where
      int _ = 2

    instance C Int [Int] where
      m _ = id

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

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

    import A
    import B
    import C

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

The output of `main` if we avoid the optimization under the effect of
IncoherentInstances is `1`. If we were to do the optimization, the output of
`main` would be `2`.
1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 10